From 54a2aa307312161b41f2ce5e36d7376676d9721e Mon Sep 17 00:00:00 2001 From: Matarener Date: Sat, 24 Oct 2026 12:48:56 +0300 Subject: [PATCH 1/3] Certify that the fragmentation of the #4610 word is rigid under free scalar reordering (negative result, no new kappa) Every admissible re-routing of the 2,526 droppable intermediate levels of the #4610 word is enumerated (518,315) under the retained frame contract with the chronological order freed, joint frame chains and movable centre reads; an exact acyclicity check shows no level can be dropped at a gain (the eight feasible drops move a centre read to the full frame, +0.983 each). Control without the centre interface finds 51 improving drops; kap-family ceilings quantify what Lambda would buy. Co-Authored-By: Claude Fable 5.1 --- .../fragmentation-reorder-rigidity/README.md | 114 ++++ .../RESULT.json | 165 ++++++ .../SOURCES.json | 48 ++ .../fragmentation-reorder-rigidity/TASK.json | 78 +++ .../VERIFY.json | 22 + .../search/README.md | 19 + .../search/dag_windows.py | 95 ++++ .../search/eval_state.py | 40 ++ .../search/forced_climbs.py | 102 ++++ .../search/forced_exact.py | 57 ++ .../search/jcr_search4.py | 414 +++++++++++++++ .../search/jcr_search5.py | 425 +++++++++++++++ .../search/make_v5.py | 77 +++ .../search/nested_facts.py | 68 +++ .../test_verify.py | 76 +++ .../fragmentation-reorder-rigidity/verify.py | 501 ++++++++++++++++++ 16 files changed, 2301 insertions(+) create mode 100644 research/fragmentation-reorder-rigidity/README.md create mode 100644 research/fragmentation-reorder-rigidity/RESULT.json create mode 100644 research/fragmentation-reorder-rigidity/SOURCES.json create mode 100644 research/fragmentation-reorder-rigidity/TASK.json create mode 100644 research/fragmentation-reorder-rigidity/VERIFY.json create mode 100644 research/fragmentation-reorder-rigidity/search/README.md create mode 100644 research/fragmentation-reorder-rigidity/search/dag_windows.py create mode 100644 research/fragmentation-reorder-rigidity/search/eval_state.py create mode 100644 research/fragmentation-reorder-rigidity/search/forced_climbs.py create mode 100644 research/fragmentation-reorder-rigidity/search/forced_exact.py create mode 100644 research/fragmentation-reorder-rigidity/search/jcr_search4.py create mode 100644 research/fragmentation-reorder-rigidity/search/jcr_search5.py create mode 100644 research/fragmentation-reorder-rigidity/search/make_v5.py create mode 100644 research/fragmentation-reorder-rigidity/search/nested_facts.py create mode 100644 research/fragmentation-reorder-rigidity/test_verify.py create mode 100644 research/fragmentation-reorder-rigidity/verify.py diff --git a/research/fragmentation-reorder-rigidity/README.md b/research/fragmentation-reorder-rigidity/README.md new file mode 100644 index 0000000000..f6eecf641c --- /dev/null +++ b/research/fragmentation-reorder-rigidity/README.md @@ -0,0 +1,114 @@ +# The fragmentation of the #4610 word is rigid under free scalar reordering + +**Scoped negative result; no new κ.** The selected record is unchanged. + +[#5226](../fragmentation-ceiling/README.md) (`fragmentation-ceiling`) prices the whole gap between Cao Yifan's +final [#4610](../kappa-round3-warp-20261022/README.md) word and the +0.05 % bar as fragmentation loss: Λ = 23.86 per +call, where Λ_f = Σ_j rank_j^t − R_f^t sums over the climbs of each field (Theorem B there). Its ship test asks which +scalar-program changes can merge climbs. #4993 and #4610's own MILP re-chose frames at a **fixed chronological +order** and found nothing; #4610 lists "change scalar chronological order" as open; `cao-trace-retiming-20261023` +compresses commuting ADDs at fixed chronology and keeps every climb; `fusion-pair-scalar-rewiring` (#5422) shows +no consecutive pair of rank-1 climbs can be fused by free same-frame rewiring. + +This package frees the **order**: scalar operations may be rescheduled anywhere their value dependencies allow, +every field's frame chain and every contact's common frame are re-chosen jointly, and the eight owned-centre +reads may move along their source chains. Under these rules **no intermediate level of any field can be +removed at a gain**: every admissible re-routing of every one of the 2,526 droppable levels is enumerated +(518,315 re-routings) and each is either infeasible or relocates a centre read to the full frame, which raises the +bill by 0.983. The fragmentation of #4610 is a property of its operation set and centre interface, not of its schedule. + +## 1. Model (the retained frame contract, order freed) + +| rule | statement | source | +|---|---|---| +| chains | a field occupies a nested chain of binary subspaces S_f < F_1 < … < T_f; a climb costs its dimension gap (H1–H2 of #5226) | #4610 contract, #5226 §0 | +| contacts | a two-field ADD/COPY happens at one common frame of both chains, with S_d + S_s ≤ F ≤ T_d ∩ T_s | one common frame per ADD (#5226 H1; `format-limits-2` S1) | +| centre | a COPY C0 ← source may sit at any frame of the source chain of dimension ≥ 1 (the transport to frame 0 then costs that dimension); the 176 deliveries target += C0 at frame 0 are fixed, as are the 8 centre transports' endpoints | `native_extensions.literal_replay` checks the field's frame at every C0 contact | +| order | scalar ops, warps, centre transports and adapters keep their value dependencies (write/read and write/write conflicts; ADDs into one destination commute); the markers `zero_frame_precondition`, `full_frame_cleanup`, `done` are barriers (the second interpreter needs the cleanup block last); every native warp stays anchored between its two frames; along a field, contacts occur in non-decreasing chain order (no descents) | exact interpreters of #4610; `verify_buffers.replay` | +| fixed | operation set, coefficients, native maps, all 632 field endpoints, the 12 fields that revisit a frame | scope | + +A **level** is an intermediate frame of a chain that hosts at least one contact. Dropping it means re-routing all +its contacts to other frames of the chain (a frame may be inserted into a partner's chain if nested there) and +merging the two adjacent climbs into one; by strict concavity every merge lowers Λ. Feasibility of a re-routing is +decided exactly: the operation DAG plus the per-field level order must stay acyclic (Pearce–Kelly incremental check). + +## 2. Results (`verify.py`, standard library, about 2 minutes) + +| # | statement | value | +|---|---|---| +| 1 | word census: 632 fields (224 mains, 408 helpers), 17,453 scalars, 3,290 climbs; profile {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40} + 8 centre; Λ(t₀) at the word's root | **23.8626** (= #5226) | +| 2 | contacts by common-frame dimension: 7,622 at dim 0, 4,808 at dim 9, **3,659 at intermediate dimensions** (these create Λ) | | +| 3 | dependency DAG of the 18,159 operations (with the three barriers): critical path | **694** of 18,159 (order is loose; without barriers 493, median slack ≈ 50 positions) | +| 4 | levels forced by the partners' **endpoints** alone (contact can neither be deferred to the next frame nor advanced to the previous one by endpoint containment) | **12 of 2,754** | +| 5 | levels forced by the partners' **exact chains** (one-field-at-a-time: the next or previous frame of f must appear in the partner's chain) | **2,437 of 2,754** (Λ ≥ 19.1 with partner chains fixed) | +| 6 | **exact rules, joint re-routing enumerated** over the 2,526 droppable levels (the 12 revisiting fields and the warp frames excluded): 518,315 re-routings tried; 322 levels have no admissible re-routing; 2,196 levels: every re-routing closes a cycle; 8 levels: feasible only by moving the centre read to the full frame, bill +0.983 each | **0 bill-improving drops** | +| 7 | control: centre interface ignored (C0 contacts not level-bound) | **51 improving drops** (test is live) | +| 8 | recorded annealing with multi-step moves (insert a frame, re-route, drop), 37 M moves over three runs | best Λ = word; centre reads stay at dimension 8 | + +Rows 4–5 say that neither endpoints nor dependencies pin the fragmentation; row 6 says the joint structure does: +the chains of a field and of its partners pin each other, and the centre interface (a source stands in a +dimension-8 frame when C0 copies it, a target at frame 0 when C0 delivers) fixes the moments around which the +rest cannot move. The only feasible drops are the eight centre-read levels themselves, and only by reading the +centre in the full frame (transport rank 9 instead of 8). Row 7 is why earlier searches that forgot the centre +interface reported Λ ≈ 23.45 (+1 % κ): those states are rejected by the exact interpreters. + +### What Λ would buy (kap-family controller formula of #5226 `verify.py`, p and a re-optimised) + +| per-call profile | κ (best p, a) | κ at p16 a7 | +|---|---|---| +| the word | 0.0030217759 (p16 a7) | 0.0030217759 | +| mains one climb each (rank 8) | 0.0037103 (p13 a6) | 0.0036997 | +| helpers one climb each (rank R_f) | 0.0051074 (p9 a4) | 0.0049744 | +| Λ = 0 | **0.0081386 (p5 a2)** | 0.0071457 | + +So the kap family with centre 8 × 8, p − 1 query shears per port, idle at address width and zero fragmentation would +reach 0.0081; the entire distance from 0.00302 to that number is Λ, and this package shows that none of it is +available by rescheduling the #4610 word. + +## 3. Reproduce + +```sh +python3.12 -I -B research/fragmentation-reorder-rigidity/verify.py +python3.12 -I -B research/fragmentation-reorder-rigidity/test_verify.py +python3.12 -B scripts/research_package.py --package research/fragmentation-reorder-rigidity +``` + +Expected marker: `PASS_FRAGMENTATION_REORDER_RIGIDITY`. `verify.py` pins both inputs by SHA256, rebuilds the model +from the word, enumerates the re-routings, runs the control and the kap-family table, and compares +[RESULT.json](RESULT.json) exactly. `--write` regenerates `RESULT.json` (authoring only). `test_verify.py` rejects a +drifted input hash, a corrupted climb rank, a contact frame mismatch and a tampered result, and re-runs the live +control. The recorded searches are in [search/](search/README.md). + +## 4. Scope and limits + +- The claim is about the frozen #4610 word: its operation set, coefficients, native maps and field endpoints. + A different operation set (for example the ADD-compressed word of `cao-trace-retiming-20261023`), new native + maps, changed helper endpoints, descents, or a different centre delivery frame are outside it. Warps keep their + two frames (72 fields carry one), and the 12 fields that revisit a frame are left as in the word. +- "Level drop" is the single-merge move; multi-step moves were explored by annealing only (row 8, RECORDED). The + exhaustive certificate is for single drops with every admissible re-routing of their contacts, pruned only by + the necessary condition that an operation which must precede another (value dependency) cannot sit at a higher + frame of the same field. +- The frame model is the one the exact interpreters of #4610 check (frames at contacts, nested climbs, C0 frames, + final frames). No physical phase, admission or outer-ledger replay was run, since no word is proposed. +- This is a finite certificate on one word, not a floor for the family: Λ = 0 words are not excluded. + +## Open next questions + +1. **Skeleton-free floor.** Does every scalar synthesis of the #4610 endpoint identity with one common frame per ADD + need a stated number of intermediate levels per main field? First step: the chain-cover LP over the contact + hypergraph with free frames (the one-field relaxations here force nothing, so the floor must use the joint + structure and the centre interface). +2. **Other operation sets.** Run the same enumeration on the compressed word of `cao-trace-retiming-20261023` + (151 fewer ADDs, same climbs): removed contacts may unpin levels. +3. **Centre delivery frame.** The deliveries at frame 0 are fixed here because the 22 targets' frames meet the + source frame only in 0 (`owned-centre-wire-floor`); a changed delivery contract is a changed mechanism. + +## Credit + +Cao Yifan (intqwq), #4610, the word and its exact interpreters; DreamingOfClouds, #5226, the fragmentation +decomposition and ship test whose kap-family formula is reused; the `cao-trace-retiming-20261023` author (ahrazzle) +and Cinna Davis, #4692, for the fixed-chronology compression line; #4993 for the fixed-order frame search; Dugongue, +#4534, and `owned-centre-wire-floor` (#5060) for the centre wire; the `fusion-pair-scalar-rewiring` package (#5422) +for the pairwise fusion certificate. Prepared by Mark (Matarener) with substantial Claude Code (Claude) assistance. +Apache-2.0. diff --git a/research/fragmentation-reorder-rigidity/RESULT.json b/research/fragmentation-reorder-rigidity/RESULT.json new file mode 100644 index 0000000000..0e3db0345c --- /dev/null +++ b/research/fragmentation-reorder-rigidity/RESULT.json @@ -0,0 +1,165 @@ +{ + "climb_profile": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "contacts_by_dimension": { + "0": 7622, + "1": 582, + "2": 449, + "3": 316, + "4": 982, + "5": 345, + "6": 240, + "7": 448, + "8": 297, + "9": 4808 + }, + "control_no_centre": { + "cycle": 2153, + "feasible": 51, + "first_drops": [ + [ + 8, + 274, + -0.007537 + ], + [ + 9, + 624, + -0.007537 + ], + [ + 11, + 621, + -0.007537 + ], + [ + 16, + 279, + -0.006778 + ], + [ + 17, + 619, + -0.007537 + ], + [ + 18, + 254, + -0.007537 + ], + [ + 20, + 280, + -0.006778 + ], + [ + 22, + 279, + -0.007537 + ], + [ + 23, + 280, + -0.007537 + ], + [ + 26, + 621, + -0.007537 + ] + ], + "improving": 51, + "levels": 2526, + "no_plan": 322, + "plans": 517771 + }, + "dag": { + "critical_path": 694, + "edges": 204174, + "ops": 18159 + }, + "exact": { + "cycle": 2196, + "feasible": 8, + "feasible_drops": [ + [ + 9, + 624, + 0.983017 + ], + [ + 11, + 621, + 0.983017 + ], + [ + 57, + 274, + 0.983017 + ], + [ + 81, + 619, + 0.983017 + ], + [ + 92, + 254, + 0.983017 + ], + [ + 224, + 279, + 0.983017 + ], + [ + 240, + 280, + 0.983017 + ], + [ + 256, + 281, + 0.983017 + ] + ], + "levels": 2526, + "no_plan": 322, + "plans": 518315 + }, + "forced_by_partner_chains": 2437, + "forced_by_partner_endpoints": 12, + "kap_family": { + "helpers_one_climb": { + "a": 4, + "kappa_best": "0.0051074492", + "kappa_p16a7": "0.0049744372", + "p": 9 + }, + "lambda_zero": { + "a": 2, + "kappa_best": "0.0081385514", + "kappa_p16a7": "0.0071456789", + "p": 5 + }, + "mains_one_climb": { + "a": 6, + "kappa_best": "0.0037103076", + "kappa_p16a7": "0.0036996562", + "p": 13 + }, + "word": { + "a": 7, + "kappa_best": "0.0030217759", + "kappa_p16a7": "0.0030217759", + "p": 16 + } + }, + "lambda_word": 23.8626371, + "levels_with_two_field_contacts": 2754 +} diff --git a/research/fragmentation-reorder-rigidity/SOURCES.json b/research/fragmentation-reorder-rigidity/SOURCES.json new file mode 100644 index 0000000000..2c96ca13fe --- /dev/null +++ b/research/fragmentation-reorder-rigidity/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "files": [ + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json", + "usage": "input", + "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415", + "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521" + }, + { + "path": "research/kappa-round3-warp-lean-20261022/NumericalMoments.lean", + "usage": "provenance", + "git_blob": "9ca4fe2ebb2733d809f8eb06c3e3b6f03540d75b", + "sha256": "e2841986fd6e6c4cc60cfe40f58a25f87a7be3bba5f89307d8a10082e48c66e6" + }, + { + "path": "research/fragmentation-ceiling/README.md", + "usage": "provenance", + "git_blob": "236e94ea255ebace3cebd37b2f2e9258b31c622e", + "sha256": "fc10b61fbceceedc6e764ad5fb8506aacf01e1de4b60b08e83fa38d8ee86dc97" + }, + { + "path": "research/cao-trace-retiming-20261023/README.md", + "usage": "provenance", + "git_blob": "ea1c3ea016471dca0e24052717e9514cef47efcc", + "sha256": "b951da4069b5e450eefa05ac3275198c1a6c3cbc377cf86183f897a134c56293" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + } + ] +} diff --git a/research/fragmentation-reorder-rigidity/TASK.json b/research/fragmentation-reorder-rigidity/TASK.json new file mode 100644 index 0000000000..a4e0014ffd --- /dev/null +++ b/research/fragmentation-reorder-rigidity/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Can the climbs of the fields of Cao Yifan's final #4610 word be made coarser (fewer, larger-rank children) by freely reordering the scalar operations within their value dependencies, jointly re-choosing every field's frame chain and every contact's common frame, and letting the owned-centre reads move along the source chains, while the operation set, the native maps, the field endpoints and the centre delivery frame stay fixed?", + "scope_change_reason": "#5226 prices the whole gap between #4610 and the +0.05% bar as fragmentation loss Lambda; its ship test asks which scalar-program changes can merge climbs. #4993 and #4610's own MILP moved frames at fixed chronology; #4610 lists a changed chronological order as open. This package frees the order and asks the question exactly for single-level merges, with an exhaustive feasibility check, instead of synthesizing a decoder.", + "bottleneck_link": "Side result; no new kappa. The fragmentation of #4610 (23.86 per call; Lambda = 0 would allow 0.0081 in the kap family) cannot be reduced by any rescheduling: it is a property of the operation set and the centre interface.", + "budget_minutes": 420, + "stop_rule": "Stop after the exhaustive single-level drop enumeration under the exact rules and the recorded annealing evidence for multi-step moves; do not synthesize a new operation set.", + "outcome": "negative-result", + "evidence": "verify.py rebuilds the word, its dependency DAG and level graph, enumerates every admissible re-routing of the 2,526 droppable levels (518,315 re-routings) and certifies by an exact acyclicity check that none lowers the bill (the only 8 feasible ones move a centre read to the full frame, +0.983 each); a control that ignores the centre interface finds 51 improving drops; the kap-family ceilings quantify what Lambda would buy. search/ records 37 million simulated-annealing moves with multi-step insert/re-route/drop that found no improvement.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Is there a skeleton-free fragmentation floor: does every scalar synthesis of the #4610 endpoint identity with one common frame per ADD need at least a stated number of intermediate levels per main field?", + "why_it_matters": "Lambda = 0 would allow kappa 0.0081 in the kap family and 0.0071 at the p16 controller; a floor would show how much of that is reachable by any word of this family.", + "blocked_by": "No argument that ties the number of contact levels to the native map; frame/endpoint relaxations alone force nothing (12 of 2,754 levels), the rigidity here comes from the joint chains and the centre interface.", + "first_step": "Formulate the chain-cover problem for the contact hypergraph with free frames and solve its LP relaxation over the 4,615 candidate frames." + }, + { + "question": "Can a different operation set (a new scalar program for the same endpoint identity, e.g. after the commuting-ADD compression of research/cao-trace-retiming-20261023) admit level drops?", + "why_it_matters": "This package fixes the operation set; compression removes operations and may remove contacts that pin levels.", + "blocked_by": "Needs the compressed word as a frozen input and the same enumeration on it.", + "first_step": "Run verify.py's drop enumeration on the compressed word of cao-trace-retiming-20261023 (same model)." + } + ] +} diff --git a/research/fragmentation-reorder-rigidity/VERIFY.json b/research/fragmentation-reorder-rigidity/VERIFY.json new file mode 100644 index 0000000000..ec290c8a8f --- /dev/null +++ b/research/fragmentation-reorder-rigidity/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/kappa-round3-warp-20261022/ARITHMETIC.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Pinned inputs; climb profile + 8 centre jobs equals ARITHMETIC local_paid; Lambda of the word 23.8626 at its own root; dependency DAG and critical path; one-field relaxations (12 and 2,437 forced levels of 2,754); exhaustive enumeration of every admissible re-routing of the 2,526 droppable levels under the exact rules (518,315 re-routings, acyclicity check): 0 bill-improving drops, the only 8 feasible ones move a centre read to the full frame (+0.983); control ignoring the centre interface finds 51 improving drops; kap-family ceilings (word 0.0030217759 at p16 a7; Lambda = 0 gives 0.0081386 at p5 a2); stored RESULT.json equals the rebuild." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_verify.py"], + "timeout_seconds": 600, + "checks": "Rejecting controls: drifted input hash, corrupted climb rank in the word, tampered stored RESULT.json, and a model with the centre interface ignored that must find drops." + } + ] +} diff --git a/research/fragmentation-reorder-rigidity/search/README.md b/research/fragmentation-reorder-rigidity/search/README.md new file mode 100644 index 0000000000..48461aa73e --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/README.md @@ -0,0 +1,19 @@ +# Recorded search evidence (not replayed by `verify.py`) + +These files document the discovery runs that preceded the exhaustive certificate in `../verify.py`. +They are retained as evidence; their hard-coded paths point at the author's local checkout +(`D:/Math/imb-docking`), and they are **not** part of the registered replay. + +| file | content | +|---|---| +| `forced_climbs.py`, `forced_exact.py`, `nested_facts.py`, `dag_windows.py` | the one-field-at-a-time relaxations, nestedness facts and dependency windows of the #4610 word (the numbers in README sections 2–3) | +| `jcr_search4.py` | simulated annealing over joint frame chains and contact frames with an incremental (Pearce–Kelly) acyclicity check, a systematic sweep phase, centre interface pinned | +| `jcr_search5.py` (derived by `make_v5.py`) | the same with the eight centre reads free to move along their source chains | +| `eval_state.py` | prices a saved state's climb profile with the kap-family controller formula | +| `sweep_exact_rules.log` | sweep under the exact rules: 0 of 2,754 levels dropped (no re-routing 330, every re-routing cyclic 2,196) | +| `sweep_no_centre_pins.log` | control sweep ignoring the centre interface: 24 levels dropped, Lambda 23.50 | +| `anneal_seed1.log`, `anneal_seed2.log`, `anneal_seed3.log` | three 6-hour / 3-hour annealing runs of `jcr_search5.py` (15.2 M, 14.7 M and 7.1 M moves; moves: drop level, re-route contact, move contact to a new frame): best Lambda 23.8626 = the word in all three; centre reads stayed at dimension 8 | + +Earlier annealing versions that ignored the centre interface reached Lambda 23.45 (a model artefact: those +states move contacts across the moments when a field must stand in the frame of a centre read or delivery, so +the exact interpreters of #4610 would reject them). The certificate in `../verify.py` includes that interface. diff --git a/research/fragmentation-reorder-rigidity/search/dag_windows.py b/research/fragmentation-reorder-rigidity/search/dag_windows.py new file mode 100644 index 0000000000..699847a0ce --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/dag_windows.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 +"""Step A1: how much order freedom do the scalar operations of #4610 have, and does it let contacts move +across the climbs of their fields? + +Dependency DAG on the 17,453 scalar ops (climbs/warps are frame bookkeeping and are left out; they will be +re-placed wherever the chosen order needs them). Two ops conflict iff one writes a register the other reads, +or both write it, except that adds into the same destination commute. ASAP/ALAP layers from the DAG. +For every field f and every consecutive pair of its contact frames F < G (in the chain), count the contacts at F +that could be scheduled after the earliest contact at G (ALAP(e) >= ASAP(e') for some e' at G) -- 'deferrable by +dependencies' -- and combine with the exact-frame partner test (partner chain contains G). Stdlib only.""" +import json, gzip, collections, os, time, sys +sys.setrecursionlimit(10000) +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)); LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s); LOG.write(s + '\n'); LOG.flush() +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']); S = list(c['start']); T = list(c['final']); nm = 224 +prog = w['programs']['forward'] +# scalar ops with read/write sets +ops = [] # (idx_in_prog, kind, writes:set, reads:set, is_add, frame, roles) +cur = list(S); chain = [[S[f]] for f in range(nf)]; contact_of = {} # op index -> (d, s, Fd, Fs) +for i, e in enumerate(prog): + if e[0] == 'climb': f = e[2]; cur[f] = e[4]; chain[f].append(e[4]) + elif e[0] == 'warp': + f = e[1][1]; cur[f] = e[4] + if e[4] != e[3]: chain[f].append(e[4]) + elif e[0] == 'scalar': + op = e[1]; kind = op[0]; roles = [tuple(r) for r in op[1:] if isinstance(r, list)] + if kind == 'add': + d, s = roles[0], roles[1]; ops.append((i, kind, {d}, {s}, True, e[2], roles)) + elif kind == 'copy': + d, s = roles[0], roles[1]; ops.append((i, kind, {d}, {s}, False, e[2], roles)) + elif kind == 'scale': ops.append((i, kind, {roles[0]}, set(), False, e[2], roles)) + elif kind == 'clear': ops.append((i, kind, {roles[0]}, set(), False, e[2], roles)) + else: raise ValueError(kind) + if kind in ('add', 'copy') and roles[0][0] == 'L' and roles[1][0] == 'L': + contact_of[len(ops) - 1] = (roles[0][1], roles[1][1], cur[roles[0][1]]) +n = len(ops); log(f'scalar ops {n}; two-field contacts {len(contact_of)}') +# DAG edges via last writer / readers per register +pred = [set() for _ in range(n)] +last_write = {}; readers_since = collections.defaultdict(list); adds_since = collections.defaultdict(list) +for j, (i, kind, W, Rd, is_add, F, roles) in enumerate(ops): + for r in Rd: + if r in last_write: pred[j].add(last_write[r]) + for a in adds_since.get(r, []): pred[j].add(a) # reading r after adds into r + for r in W: + if is_add: + # commutes with other adds into r; depends on last non-add writer and on readers since then + if r in last_write: pred[j].add(last_write[r]) + for k in readers_since.get(r, []): pred[j].add(k) + adds_since[r].append(j) + else: + if r in last_write: pred[j].add(last_write[r]) + for k in readers_since.get(r, []): pred[j].add(k) + for a in adds_since.get(r, []): pred[j].add(a) + last_write[r] = j; readers_since[r] = []; adds_since[r] = [] + for r in Rd: readers_since[r].append(j) + pred[j].discard(j) +succ = [set() for _ in range(n)] +for j in range(n): + for k in pred[j]: succ[k].add(j) +asap = [0] * n +for j in range(n): asap[j] = 1 + max((asap[k] for k in pred[j]), default=-1) +depth = max(asap) + 1 +alap = [depth - 1] * n +for j in range(n - 1, -1, -1): alap[j] = min((alap[k] - 1 for k in succ[j]), default=depth - 1) +slack = [alap[j] - asap[j] for j in range(n)] +log(f'DAG depth {depth} (critical path) vs {n} ops; edges {sum(len(p) for p in pred)}; slack histogram (quantiles): ' + + str([sorted(slack)[int(q * (n - 1))] for q in (0, .1, .25, .5, .75, .9, 1)])) +# per field: contacts by frame with asap/alap +chainset = [set(ch) for ch in chain] +byf = collections.defaultdict(lambda: collections.defaultdict(list)) # f -> frame -> [(asap, alap, partner, opidx)] +for j, (d, s, F) in contact_of.items(): + byf[d][F].append((asap[j], alap[j], s, j)); byf[s][F].append((asap[j], alap[j], d, j)) +levels = removable_dep = removable_both = 0; per_field_removable = collections.Counter() +for f in range(nf): + ch = chain[f] + for i in range(1, len(ch) - 1): + F = ch[i]; cs = byf[f].get(F, []) + if not cs: continue + levels += 1 + G, E = ch[i+1], ch[i-1] + later = [a for a, _, _, _ in byf[f].get(G, [])]; earlier = [b for _, b, _, _ in byf[f].get(E, [])] + first_G = min(later) if later else 10**9; last_E = max(earlier) if earlier else -1 + ok_dep = all((al >= first_G) or (asp <= last_E) for asp, al, _, _ in cs) + ok_both = all(((al >= first_G) and G in chainset[g]) or ((asp <= last_E) and E in chainset[g]) for asp, al, g, _ in cs) + removable_dep += ok_dep; removable_both += ok_both + if ok_both: per_field_removable[f] += 1 +log(f'contact levels {levels}: removable by dependency windows alone {removable_dep}; by windows AND exact partner frames {removable_both}') +log(f'fields with >=1 jointly removable level: {len(per_field_removable)}; total removable levels {sum(per_field_removable.values())}') +json.dump({'ops': n, 'depth': depth, 'levels': levels, 'removable_dep': removable_dep, 'removable_both': removable_both, + 'slack_quantiles': [sorted(slack)[int(q * (n - 1))] for q in (0, .1, .25, .5, .75, .9, 1)]}, + open(os.path.join(HERE, 'dag_windows_result.json'), 'w'), indent=1) +log('done dag_windows') diff --git a/research/fragmentation-reorder-rigidity/search/eval_state.py b/research/fragmentation-reorder-rigidity/search/eval_state.py new file mode 100644 index 0000000000..891e17c6b2 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/eval_state.py @@ -0,0 +1,40 @@ +#!/usr/bin/env python3 +"""Evaluate saved JCR states: kappa at p16 a7 for the found per-call profile, and what changed vs the word. +Usage: py -3.12 eval_state.py jcr_state_seed2.json [more...]""" +import json, sys, math, collections, gzip +from decimal import Decimal as D, getcontext +getcontext().prec = 40 +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +A = json.load(open(W3 + 'ARITHMETIC.json')) +H = {int(k): n for k, n in A['local_helpers'].items()}; N0 = {int(k): n for k, n in A['local_paid'].items()} +v, d = 112, 8 +def pw(x, t): x = D(x); return D(0) if x == 0 else (t * x.ln()).exp() +def mom(P, t): return sum(D(n) * pw(r, t) for r, n in P.items()) +def inv(p, a): + T = collections.Counter({r: (p + 2) * n for r, n in H.items()}); P = collections.Counter() + P[1] += v * (p - 1); T[1 + d * (p + 2)] += 2 * v + for L in (a, p - 1 - a): + for j in range(1, L + 1): T[1 + d * (j + 1)] += 2 * v; P[d * (j + 1)] += 2 * v + return T, P +def kappa(Nloc, p=16, a=7): + T, P = inv(p, a) + for r, n in Nloc.items(): P[r] += (p + 2) * n + lo, hi = D('1e-6'), D('0.05') + for _ in range(120): + m = (lo + hi) / 2 + if mom(T, 1 - m) - mom(P, 1 - m) > 0: lo = m + else: hi = m + return lo +k0 = kappa(N0) +print(f'word #4610: local_paid {N0} kappa = {k0:.10f}') +for path in sys.argv[1:]: + st = json.load(open(path)) + prof = {int(k): n for k, n in st['profile'].items()} if 'profile' in st else None + if prof is None: print(path, 'no profile (checkpoint only), best Lambda', st['best']); continue + Nloc = collections.Counter(prof) + if not st.get('centre_included'): Nloc[8] += 8 # centre jobs + k = kappa(Nloc) + print(f'{path}: Lambda {st["best"]:.4f}; profile {dict(sorted(prof.items()))}; mass {sum(r*n for r,n in prof.items())}; ' + f'kappa = {k:.10f} ({(k/k0-1)*100:+.3f}% vs word); best p,a: ', end='') + best = max((kappa(Nloc, p, a), p, a) for p in range(8, 25) for a in range(0, (p - 1) // 2 + 1)) + print(f'{best[0]:.10f} at p={best[1]} a={best[2]}') diff --git a/research/fragmentation-reorder-rigidity/search/forced_climbs.py b/research/fragmentation-reorder-rigidity/search/forced_climbs.py new file mode 100644 index 0000000000..731cd3b7a2 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/forced_climbs.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Step 1 of the Lambda direction: which climbs of #4610 are forced by the endpoints of contact partners? + +Replay the forward program of research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz, tracking every field's +frame. For every field f with climb chain S=F_0 < F_1 < ... < F_k = T, an intermediate frame F_i is REMOVABLE +(necessary condition only) if every scalar contact f has while sitting at F_i could be done either + (defer) at the next frame F_{i+1}: partner g must be able to reach F_{i+1}, i.e. T_g >= F_{i+1}, or + (advance) at the previous frame F_{i-1}: partner must be able to sit there, i.e. S_g <= F_{i-1} <= T_g. +Otherwise the frame is FORCED by the partners' endpoints: with these operations and these endpoints, no retiming +or frame reassignment removes it. k_min(f) = 1 + #forced intermediate frames is a lower bound on the number of +climbs of f, and with total rank R_f fixed, Lambda_f >= (R_f-k+1)^t + (k-1) - R_f^t (concavity). +Stdlib only, seconds. Writes forced_result.json and progress.log. +""" +import json, gzip, collections, math, os, time +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s); LOG.write(s + '\n'); LOG.flush() + +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']) +def span(fi): + """F2-span of frame fi as a frozenset of ints (9-bit vectors).""" + vs = frames[fi]; s = {0} + for v in vs: s |= {x ^ v for x in s} + return frozenset(s) +SP = {} +def sp(fi): + if fi not in SP: SP[fi] = span(fi) + return SP[fi] +def leq(a, b): return sp(a) <= sp(b) +S = list(c['start']); T = list(c['final']) +R = [len(frames[T[f]]) - len(frames[S[f]]) for f in range(nf)] +H = {int(k): n for k, n in json.load(open(W3 + 'ARITHMETIC.json'))['local_helpers'].items()} +nh = sum(H.values()); nm = nf - nh +log(f'fields {nf}: mains {nm} (R=8), helpers {nh}; final dims {collections.Counter(len(frames[t]) for t in T)}') + +# replay: chain of frames per field, contacts per (field, frame) +cur = list(S); chain = [[S[f]] for f in range(nf)] +contacts = collections.defaultdict(list) # (f, frame) -> list of partner fields +nscal = 0; bad = 0 +for e in w['programs']['forward']: + if e[0] == 'climb': + f, a, b = e[2], e[3], e[4]; assert cur[f] == a; cur[f] = b; chain[f].append(b) + elif e[0] == 'warp': + f = e[1][1]; assert cur[f] == e[3]; cur[f] = e[4] + if e[4] != e[3]: chain[f].append(e[4]) # same dimension, different frame: a new level for contacts + elif e[0] == 'scalar': + op = e[1]; F = e[2] + roles = [r for r in op[1:] if isinstance(r, list) and r[0] == 'L'] + if op[0] in ('add', 'copy') and len(roles) == 2: + d, s = roles[0][1], roles[1][1] + if cur[d] != F or cur[s] != F: bad += 1 + contacts[(d, cur[d])].append(s); contacts[(s, cur[s])].append(d); nscal += 1 +assert cur == T +log(f'two-field scalar contacts {nscal}; contacts not at the recorded common frame {bad}') + +# per-field analysis +t = 1 - 0.0030217759 +def pw(x): return 0.0 if x == 0 else math.exp(t * math.log(x)) +tot_forced = 0; lam_lb = 0.0; lam_real = 0.0; per = [] +forced_by = collections.Counter(); hist_k = collections.Counter(); hist_kmin = collections.Counter() +for f in range(nf): + ch = chain[f] + # climbs = strictly increasing dimension steps (warps keep dimension) + climbs = [len(frames[ch[i+1]]) - len(frames[ch[i]]) for i in range(len(ch) - 1) if len(frames[ch[i+1]]) > len(frames[ch[i]])] + lam_real += sum(pw(x) for x in climbs) - pw(R[f]) + forced = 0 + for i in range(1, len(ch) - 1): + Fi = ch[i] + if len(frames[Fi]) in (len(frames[ch[0]]), len(frames[ch[-1]])) and False: pass + prev, nxt = ch[i-1], ch[i+1] + partners = contacts.get((f, Fi), []) + if not partners: continue # no contact here: the level is free to drop + ok = True; why = None + for g in partners: + defer = leq(nxt, T[g]) + adv = leq(S[g], prev) and leq(prev, T[g]) + if not (defer or adv): + ok = False; why = ('helper' if g >= nm else 'main', len(frames[T[g]])); break + if not ok: + forced += 1; forced_by[why] += 1 + k = len(climbs); kmin = 1 + forced + hist_k[k] += 1; hist_kmin[kmin] += 1 + tot_forced += forced + lb = (pw(R[f] - kmin + 1) + (kmin - 1) - pw(R[f])) if R[f] >= kmin else (pw(R[f]) - pw(R[f])) + lam_lb += lb + per.append({'f': f, 'kind': 'main' if f < nm else 'helper', 'R': R[f], 'climbs': k, 'kmin': kmin, 'levels': len(ch)}) +log(f'Lambda(real, t=1-kappa4610) = {lam_real:.4f} (package: 23.8626 at its own root)') +log(f'forced intermediate frames: {tot_forced} of {sum(len(ch)-2 for ch in chain)} intermediate levels; by partner kind/final dim: {dict(forced_by)}') +log(f'climbs per field histogram (real): {dict(sorted(hist_k.items()))}') +log(f'k_min per field histogram (forced): {dict(sorted(hist_kmin.items()))}') +log(f'Lambda lower bound from forced frames (concavity): {lam_lb:.4f} vs real {lam_real:.4f}') +mains = [p for p in per if p['kind'] == 'main']; helps = [p for p in per if p['kind'] == 'helper'] +log(f"mains: mean climbs {sum(p['climbs'] for p in mains)/nm:.2f}, mean kmin {sum(p['kmin'] for p in mains)/nm:.2f}; helpers: mean climbs {sum(p['climbs'] for p in helps)/nh:.2f}, mean kmin {sum(p['kmin'] for p in helps)/nh:.2f}") +# contact census by frame dimension +dimc = collections.Counter(len(frames[F]) for (f, F), ps in contacts.items() for _ in ps) +log(f'contact endpoints by frame dimension: {dict(sorted(dimc.items()))}') +json.dump({'lambda_real': lam_real, 'lambda_lb_forced': lam_lb, 'forced': tot_forced, 'forced_by': {str(k): v for k, v in forced_by.items()}, + 'hist_climbs': dict(hist_k), 'hist_kmin': dict(hist_kmin), 'per_field': per}, open(os.path.join(HERE, 'forced_result.json'), 'w')) +log('done forced_climbs') diff --git a/research/fragmentation-reorder-rigidity/search/forced_exact.py b/research/fragmentation-reorder-rigidity/search/forced_exact.py new file mode 100644 index 0000000000..17093bbb79 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/forced_exact.py @@ -0,0 +1,57 @@ +#!/usr/bin/env python3 +"""Step 1b: exact-frame version. A contact of f at its i-th frame F_i can move only to a frame that the partner's +chain also contains EXACTLY (an ADD needs one common frame). F_i is removable (necessary condition) iff every +partner's chain contains F_{i+1}(f) (defer) or F_{i-1}(f) (advance). Otherwise the partners' chains diverge at +F_i and the level is forced for this operation set, whatever the order and timing. Also: a 'strict' variant that +demands ALL partners of the level agree on the same direction (all defer or all advance).""" +import json, gzip, collections, math, os, time +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)) +LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s); LOG.write(s + '\n'); LOG.flush() +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']); S = list(c['start']); T = list(c['final']) +R = [len(frames[T[f]]) - len(frames[S[f]]) for f in range(nf)] +nm = 224 +cur = list(S); chain = [[S[f]] for f in range(nf)]; contacts = collections.defaultdict(list) +for e in w['programs']['forward']: + if e[0] == 'climb': f = e[2]; cur[f] = e[4]; chain[f].append(e[4]) + elif e[0] == 'warp': + f = e[1][1]; cur[f] = e[4] + if e[4] != e[3]: chain[f].append(e[4]) + elif e[0] == 'scalar': + op = e[1]; roles = [r for r in op[1:] if isinstance(r, list) and r[0] == 'L'] + if op[0] in ('add', 'copy') and len(roles) == 2: + d, s = roles[0][1], roles[1][1]; contacts[(d, cur[d])].append(s); contacts[(s, cur[s])].append(d) +chainset = [set(ch) for ch in chain] +t = 1 - 0.0030217759 +def pw(x): return 0.0 if x == 0 else math.exp(t * math.log(x)) +res = {} +for mode in ('any', 'strict'): + forced_tot = 0; lam_lb = 0.0; hist = collections.Counter(); forced_dim = collections.Counter(); lv_tot = 0 + for f in range(nf): + ch = chain[f]; forced = 0 + for i in range(1, len(ch) - 1): + ps = contacts.get((f, ch[i]), []) + if not ps: continue + lv_tot += 1 + defer = [ch[i+1] in chainset[g] for g in ps]; adv = [ch[i-1] in chainset[g] for g in ps] + if mode == 'any': ok = all(dd or aa for dd, aa in zip(defer, adv)) + else: ok = all(defer) or all(adv) + if not ok: forced += 1; forced_dim[len(frames[ch[i]])] += 1 + kmin = 1 + forced; hist[kmin] += 1; forced_tot += forced + lam_lb += (pw(R[f] - kmin + 1) + (kmin - 1) - pw(R[f])) if R[f] >= kmin else 0.0 + log(f'[{mode}] forced levels {forced_tot} of {lv_tot} contact levels; k_min histogram {dict(sorted(hist.items()))}; by dim {dict(sorted(forced_dim.items()))}; Lambda_lb = {lam_lb:.4f} (real 23.8626)') + res[mode] = {'forced': forced_tot, 'levels': lv_tot, 'hist_kmin': dict(hist), 'lambda_lb': lam_lb} +# how do partner chains diverge: at a contact level F of f, how many distinct NEXT frames do the partners take? +div = collections.Counter() +nxt = {} +for f in range(nf): + ch = chain[f] + for i in range(len(ch) - 1): nxt[(f, ch[i])] = ch[i+1] +for (f, F), ps in contacts.items(): + nx = {nxt.get((g, F)) for g in ps if (g, F) in nxt} + div[len(nx)] += 1 +log(f'distinct next frames among the partners of a (field, level): {dict(sorted(div.items()))}') +json.dump(res, open(os.path.join(HERE, 'forced_exact_result.json'), 'w'), indent=1) diff --git a/research/fragmentation-reorder-rigidity/search/jcr_search4.py b/research/fragmentation-reorder-rigidity/search/jcr_search4.py new file mode 100644 index 0000000000..f5f7edb7b4 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/jcr_search4.py @@ -0,0 +1,414 @@ +#!/usr/bin/env python3 +"""JCR search v4: same model as v3 (joint frame chains + contact frames, free scalar order within value +dependencies, warp frames fixed, 12 revisiting fields pinned), but with an INCREMENTAL acyclicity check +(Pearce-Kelly dynamic topological order) instead of a full graph rebuild per move, and a systematic sweep +phase before annealing. + +Graph nodes: the 18,149 ops (static DAG edges) plus dynamic level nodes entry/exit per (field, level) that +currently hosts contacts. Edges: entry(f,L) -> op -> exit(f,L) for every contact op at that level, and +exit(f,L_i) -> entry(f,L_{i+1}) along each chain; warp ops anchored between their two frames. +A move = a set of edge deletions followed by edge insertions; an insertion that closes a cycle rejects the move +and everything is rolled back. + +Usage: py -3.12 jcr_search4.py [minutes=60] [seed=1] +""" +import json, gzip, collections, os, time, sys, math, random +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)); LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s, flush=True); LOG.write(s + '\n'); LOG.flush() +MINUTES = float(sys.argv[1]) if len(sys.argv) > 1 else 60.0 +SEED = int(sys.argv[2]) if len(sys.argv) > 2 else 1 +random.seed(SEED) +t = 1 - 0.0030217759 +def pw(x): return 0.0 if x <= 0 else math.exp(t * math.log(x)) + +# ---------------- word ---------------- +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']); S = list(c['start']); T = list(c['final']); nm = 224 +prog = w['programs']['forward'] +def span_of(vs): + s = {0} + for v in vs: s |= {x ^ v for x in s} + return frozenset(s) +spans = [span_of(fr) for fr in frames]; span_id = {sp: i for i, sp in enumerate(spans)} +def fid(sp): + if sp not in span_id: span_id[sp] = len(spans); spans.append(sp) + return span_id[sp] +def dim(i): return len(spans[i]).bit_length() - 1 +def sub(a, b): return spans[a] <= spans[b] +def join(a, b): return a if a == b else fid(span_of(list(spans[a] | spans[b]))) +def meet(a, b): return fid(spans[a] & spans[b]) + +cur = list(S); chain0 = [[S[f]] for f in range(nf)]; pinned_f = set(); warp_frames = collections.defaultdict(set) +for e in prog: + if e[0] == 'climb': + f = e[2] + if e[4] in chain0[f]: pinned_f.add(f) + chain0[f].append(e[4]); cur[f] = e[4] + elif e[0] == 'warp': + f = e[1][1] + if e[4] != e[3]: + if e[4] in chain0[f]: pinned_f.add(f) + warp_frames[f].add(cur[f]); warp_frames[f].add(e[4]); chain0[f].append(e[4]) + cur[f] = e[4] +ops = []; contacts = []; warp_ops = []; barriers = []; block_ops = [] # phase markers are barriers +cur = list(S); visit = [0] * nf +def key_of(f): return ('v', visit[f]) if f in pinned_f else cur[f] +for e in prog: + if e[0] == 'climb': f = e[2]; cur[f] = e[4]; visit[f] += 1 + elif e[0] == 'warp': + f = e[1][1]; j = len(ops); ops.append((False, {('L', f)}, set())) + if e[4] != e[3]: warp_ops.append((j, f, visit[f], cur[f], e[4])); cur[f] = e[4]; visit[f] += 1 + elif e[0] == 'phase': + if e[1] in ('zero_frame_precondition', 'full_frame_cleanup', 'done') and not os.environ.get('JCR_NOBARRIER'): barriers.append(len(ops)) + ops.append((False, set(), set())) + elif e[0] == 'center': ops.append((False, {('L', e[2])}, set())) + elif e[0] == 'adapter': ops.append((False, {('L', e[2]), ('L', e[3])}, set())) + elif e[0] == 'scalar': + op = e[1]; kind = op[0]; roles = [tuple(r) for r in op[1:] if isinstance(r, list)] + W, Rd = ({roles[0]}, {roles[1]}) if kind in ('add', 'copy') else ({roles[0]}, set()) + j = len(ops); ops.append((kind == 'add', W, Rd)) + if kind in ('add', 'copy') and roles[0][0] == 'L' and roles[1][0] == 'L': + d, s = roles[0][1], roles[1][1]; F = e[2] + lo = join(S[d], S[s]); hi = meet(T[d], T[s]) + if not sub(lo, F): lo = F + contacts.append({'d': d, 's': s, 'op': j, 'lo': lo, 'hi': hi, 'F': F, 'kd': key_of(d), 'ks': key_of(s), + 'pin': (d in pinned_f or s in pinned_f)}) + elif kind in ('add', 'copy') and sum(r[0] == 'L' for r in roles) == 1 and not os.environ.get('JCR_NOC'): + f = next(r[1] for r in roles if r[0] == 'L'); F = e[2] # contact with the owned C0 buffer: pinned + contacts.append({'d': f, 's': f, 'op': j, 'lo': F, 'hi': F, 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': True, 'C': True}) + # 'scale' ops commute with climbs: they stay in the DAG only and take the field's current frame when emitted +n = len(ops) +pred = [set() for _ in range(n)] +# barrier edges: every op depends on the last phase marker before it, and the next marker depends on every op +bi = 0 +for j in range(n): + if bi < len(barriers) and j == barriers[bi]: + if bi > 0: + for k in range(barriers[bi - 1] + 1, j): pred[j].add(k) + bi += 1 + elif bi > 0: pred[j].add(barriers[bi - 1]) +last_write = {}; readers = collections.defaultdict(list); adds = collections.defaultdict(list) +for j, (is_add, W, Rd) in enumerate(ops): + for r in Rd: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(adds.get(r, [])) + for r in W: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(readers.get(r, [])) + if is_add: adds[r].append(j) + else: pred[j].update(adds.get(r, [])); last_write[r] = j; readers[r] = []; adds[r] = [] + for r in Rd: readers[r].append(j) + pred[j].discard(j) +log(f'JCR v4: fields {nf} (pinned {len(pinned_f)}), contacts {len(contacts)}, ops {n}, dag edges {sum(len(p) for p in pred)}, frames {len(spans)}') + +# ---------------- dynamic graph with Pearce-Kelly order ---------------- +class DynGraph: + def __init__(self, nstatic, pred): + self.out = [set() for _ in range(nstatic)]; self.inn = [set() for _ in range(nstatic)] + for j in range(nstatic): + for k in pred[j]: self.out[k].add(j); self.inn[j].add(k) + self.ord = list(range(nstatic)) # node -> position + self.free = [] + def new_node(self): + if self.free: u = self.free.pop(); self.out[u] = set(); self.inn[u] = set(); return u + u = len(self.out); self.out.append(set()); self.inn.append(set()); self.ord.append(self.ord and max(self.ord) + 1 or 0) + return u + def del_node(self, u): + assert not self.out[u] and not self.inn[u]; self.free.append(u) + def del_edge(self, u, v): self.out[u].discard(v); self.inn[v].discard(u) + def add_edge(self, u, v): + """returns False (and leaves the graph unchanged) if the edge would close a cycle.""" + if v in self.out[u]: return True + ord = self.ord + if ord[u] < ord[v]: self.out[u].add(v); self.inn[v].add(u); return True + lb, ub = ord[v], ord[u] + # forward from v within (.., ub] + Rf = []; seen = {v}; st = [v] + while st: + x = st.pop(); Rf.append(x) + for y in self.out[x]: + if y == u: return False + if y not in seen and ord[y] <= ub: seen.add(y); st.append(y) + Rb = []; seenb = {u}; st = [u] + while st: + x = st.pop(); Rb.append(x) + for y in self.inn[x]: + if y not in seenb and ord[y] >= lb: seenb.add(y); st.append(y) + # reorder: nodes of Rb then Rf take the sorted positions of Rb ∪ Rf + Rb.sort(key=lambda x: ord[x]); Rf.sort(key=lambda x: ord[x]) + pos = sorted(ord[x] for x in Rb + Rf) + for x, p in zip(Rb + Rf, pos): ord[x] = p + self.out[u].add(v); self.inn[v].add(u); return True + +G = DynGraph(n, pred) + +# ---------------- state ---------------- +chain = []; frame_of = {} +for f in range(nf): + if f in pinned_f: + keys = [('v', i) for i in range(len(chain0[f]))] + for i, fr in enumerate(chain0[f]): frame_of[(f, ('v', i))] = fr + else: + keys = [] + for fr in chain0[f]: + if fr not in keys: keys.append(fr) + frame_of[(f, fr)] = fr + chain.append(keys) +cset = [set(ch) for ch in chain] +at = collections.defaultdict(set) +for k, e in enumerate(contacts): at[(e['d'], e['kd'])].add(k); at[(e['s'], e['ks'])].add(k) +lvnode = {} # (f, key) -> (entry, exit) for levels with contacts +def fdim(f, key): return dim(frame_of[(f, key)]) +def lam_field(f): + ds = [fdim(f, k) for k in chain[f]] + return sum(pw(ds[i+1] - ds[i]) for i in range(len(ds) - 1)) - pw(ds[-1] - ds[0]) +LAM = [lam_field(f) for f in range(nf)] +def total(): return sum(LAM) + +# build initial level graph in word order (cannot fail) +def active_levels(f): return [k for k in chain[f] if (f, k) in lvnode] +for f in range(nf): + for key in chain[f]: + if at.get((f, key)): + ent, ex = G.new_node(), G.new_node(); lvnode[(f, key)] = (ent, ex) + for k in at[(f, key)]: + o = contacts[k]['op']; assert G.add_edge(ent, o) and G.add_edge(o, ex) + al = active_levels(f) + for a, b in zip(al, al[1:]): assert G.add_edge(lvnode[(f, a)][1], lvnode[(f, b)][0]) +def warp_anchor_edges(j, f, va, A, B): + """edges (u, v) anchoring warp op j for the current chain of f.""" + out = []; ch = chain[f] + if f in pinned_f: + for key in ch: + if (f, key) not in lvnode: continue + if key[1] <= va: out.append((lvnode[(f, key)][1], j)) + else: out.append((j, lvnode[(f, key)][0])) + else: + pa, pb = ch.index(A), ch.index(B) + for i, key in enumerate(ch): + if (f, key) not in lvnode: continue + if i <= pa: out.append((lvnode[(f, key)][1], j)) + elif i >= pb: out.append((j, lvnode[(f, key)][0])) + return out +for wo in warp_ops: + for u, v in warp_anchor_edges(*wo): assert G.add_edge(u, v) +warps_of = collections.defaultdict(list) +for wo in warp_ops: warps_of[wo[1]].append(wo) +log(f'initial Lambda = {total():.4f}; dynamic graph built, nodes {len(G.out)}') + +# ---------------- transactional edits ---------------- +class Txn: + """collects structural changes; graph edges are re-derived for touched fields and applied with rollback.""" + def __init__(self): self.touched = set(); self.undo = []; self.added = []; self.removed = [] + def set_contact(self, k, Fnew): + e = contacts[k]; self.undo.append(('c', k, e['F'], e['kd'], e['ks'])) + at[(e['d'], e['kd'])].discard(k); at[(e['s'], e['ks'])].discard(k) + e['F'] = Fnew; e['kd'] = Fnew; e['ks'] = Fnew + at[(e['d'], Fnew)].add(k); at[(e['s'], Fnew)].add(k); self.touched.update((e['d'], e['s'])) + def insert_frame(self, f, F): + pos = len(chain[f]) + for i, x in enumerate(chain[f]): + if dim(x) > dim(F): pos = i; break + chain[f].insert(pos, F); cset[f].add(F); frame_of[(f, F)] = F; LAM[f] = lam_field(f) + self.undo.append(('i', f, F)); self.touched.add(f) + def remove_frame(self, f, F): + chain[f].remove(F); cset[f].discard(F); at.pop((f, F), None); frame_of.pop((f, F), None); LAM[f] = lam_field(f) + self.undo.append(('r', f, F)); self.touched.add(f) + def rollback_state(self): + while self.undo: + kind, *a = self.undo.pop() + if kind == 'c': + k, F, kd, ks = a; e = contacts[k] + at[(e['d'], e['kd'])].discard(k); at[(e['s'], e['ks'])].discard(k) + e['F'], e['kd'], e['ks'] = F, kd, ks; at[(e['d'], kd)].add(k); at[(e['s'], ks)].add(k) + elif kind == 'i': + f, F = a; chain[f].remove(F); cset[f].discard(F); frame_of.pop((f, F), None); LAM[f] = lam_field(f) + else: + f, F = a; pos = len(chain[f]) + for i, x in enumerate(chain[f]): + if dim(x) > dim(F): pos = i; break + chain[f].insert(pos, F); cset[f].add(F); frame_of[(f, F)] = F; LAM[f] = lam_field(f) + +def level_edges(f): + """all graph edges owned by field f's level structure (contact edges, chain edges, warp anchors).""" + E = set() + al = active_levels(f) + for key in al: + ent, ex = lvnode[(f, key)] + for k in at[(f, key)]: + o = contacts[k]['op']; E.add((ent, o)); E.add((o, ex)) + for a, b in zip(al, al[1:]): E.add((lvnode[(f, a)][1], lvnode[(f, b)][0])) + for wo in warps_of.get(f, []): E.update(warp_anchor_edges(*wo)) + return E + +def commit_graph(txn): + """re-derive the level graph of touched fields; return True if acyclic (edges applied), else rollback edges.""" + old = {} + for f in txn.touched: old[f] = level_edges_snapshot[f] + # create/delete level nodes according to current `at` + newnodes = []; delnodes = [] + for f in txn.touched: + for key in chain[f]: + has = bool(at.get((f, key))) + if has and (f, key) not in lvnode: lvnode[(f, key)] = (G.new_node(), G.new_node()); newnodes.append((f, key)) + for (ff, key) in [x for x in lvnode if x[0] == f]: + if key not in chain[f] or not at.get((f, key)): delnodes.append((f, key)) + new = {} + for f in txn.touched: new[f] = level_edges(f) + oldE = set().union(*old.values()) if old else set(); newE = set().union(*new.values()) if new else set() + for u, v in oldE - newE: G.del_edge(u, v) + added = [] + ok = True + for u, v in newE - oldE: + if not G.add_edge(u, v): ok = False; break + added.append((u, v)) + if not ok: + for u, v in added: G.del_edge(u, v) + for u, v in oldE - newE: assert G.add_edge(u, v) + for fk in newnodes: ent, ex = lvnode.pop(fk); G.del_node(ent); G.del_node(ex) + return False + for fk in delnodes: + ent, ex = lvnode.pop(fk); G.del_node(ent); G.del_node(ex) + for f in txn.touched: level_edges_snapshot[f] = new[f] + return True +level_edges_snapshot = [level_edges(f) for f in range(nf)] + +def apply(txn): + """finish a transaction: graph check; on failure roll back state too.""" + if commit_graph(txn): return True + txn.rollback_state() + # level nodes for fields whose `at` was restored may need re-creation on the next commit; keep lvnode consistent: + for f in txn.touched: + for key in chain[f]: + if at.get((f, key)) and (f, key) not in lvnode: + lvnode[(f, key)] = (G.new_node(), G.new_node()) + for k in at[(f, key)]: + o = contacts[k]['op']; assert G.add_edge(lvnode[(f, key)][0], o) and G.add_edge(o, lvnode[(f, key)][1]) + level_edges_snapshot[f] = level_edges(f) + return False + +def nested_ok(f, F): + return f not in pinned_f and all(sub(x, F) or sub(F, x) for x in chain[f]) and sub(S[f], F) and sub(F, T[f]) +def removable(f, F): return f not in pinned_f and F != S[f] and F != T[f] and F not in warp_frames[f] + +def drop_level(f, F, txn): + if not removable(f, F): return False + plan = [] + for k in list(at.get((f, F), [])): + e = contacts[k] + if e['pin']: return False + g = e['s'] if e['d'] == f else e['d'] + opts = [X for X in chain[f] if X != F and sub(e['lo'], X) and sub(X, e['hi'])] + if e.get('U'): + if not opts: return False + plan.append((k, random.choice(opts), None)); continue + common = [X for X in opts if X in cset[g]] + if common: plan.append((k, random.choice(common), None)); continue + ins = [X for X in opts if nested_ok(g, X)] + if not ins: return False + plan.append((k, random.choice(ins), g)) + for k, X, g in plan: + if g is not None and X not in cset[g]: txn.insert_frame(g, X) + txn.set_contact(k, X) + txn.remove_frame(f, F); return True +def reroute(k, txn): + e = contacts[k] + if e['pin']: return False + d, s = e['d'], e['s'] + opts = [X for X in chain[d] if X in cset[s] and X != e['F'] and sub(e['lo'], X) and sub(X, e['hi'])] + if e.get('U') and opts: txn.set_contact(k, random.choice(opts)); return True + if not opts: return False + txn.set_contact(k, random.choice(opts)); return True +def new_frame(k, txn): + e = contacts[k] + if e['pin'] or e.get('U'): return False + d, s = e['d'], e['s'] + cand = [X for X in random.sample(range(len(spans)), 40) if X != e['F'] and sub(e['lo'], X) and sub(X, e['hi']) + and (X in cset[d] or nested_ok(d, X)) and (X in cset[s] or nested_ok(s, X))] + if not cand: return False + X = random.choice(cand) + if X not in cset[d]: txn.insert_frame(d, X) + if X not in cset[s]: txn.insert_frame(s, X) + txn.set_contact(k, X); return True +def drop_empty(txn): + for f in list(txn.touched): + for F in list(chain[f]): + if removable(f, F) and not at.get((f, F)): txn.remove_frame(f, F) + +free_fields = [f for f in range(nf) if f not in pinned_f]; free_contacts = [k for k, e in enumerate(contacts) if not e['pin']] +best = total(); cur_val = best +def save(tag): + prof = collections.Counter() + for f in range(nf): + ds = [fdim(f, k) for k in chain[f]] + for i in range(len(ds) - 1): + if ds[i+1] > ds[i]: prof[ds[i+1] - ds[i]] += 1 + # topological order of all graph nodes (Kahn on the dynamic graph), ops only + indeg = {u: len(G.inn[u]) for u in range(len(G.out)) if u < n or (G.out[u] or G.inn[u])} + ready = sorted([u for u, dg in indeg.items() if dg == 0], key=lambda u: G.ord[u]); order = [] + import heapq + heap = [(G.ord[u], u) for u in ready]; heapq.heapify(heap) + while heap: + _, u = heapq.heappop(heap); order.append(u) + for v_ in G.out[u]: + indeg[v_] -= 1 + if indeg[v_] == 0: heapq.heappush(heap, (G.ord[v_], v_)) + assert len(order) == len(indeg), 'cyclic at save' + json.dump({'best': best, 'profile': dict(prof), 'chains': [[str(k) for k in ch] for ch in chain], + 'chain_frames': [[frame_of[(f, k)] for k in ch] for f, ch in enumerate(chain)], + 'contact_frames': [e['F'] for e in contacts], 'contact_ops': [e['op'] for e in contacts], + 'op_order': [u for u in order if u < n], 'extra_frames': [sorted(spans[i]) for i in range(len(frames), len(spans))], 'tag': tag}, + open(os.path.join(HERE, f'jcr4_state_seed{SEED}.json'), 'w')) + return prof + +# ---------------- phase 1: systematic sweep (greedy, downhill only) ---------------- +start = time.time(); deadline = start + MINUTES * 60 +sweep = 0; gained = 0 +while time.time() < deadline and sweep < 3: + sweep += 1; improved = 0; f_plan = f_cost = f_cycle = 0 + order = list(free_fields); random.shuffle(order) + for f in order: + for F in list(chain[f]): + if not removable(f, F) or F not in chain[f]: continue + txn = Txn(); before = total() + if not drop_level(f, F, txn): txn.rollback_state(); f_plan += 1; continue + drop_empty(txn) + if total() > before + 1e-12: txn.rollback_state(); f_cost += 1; continue + if apply(txn): improved += 1; cur_val = total() + else: f_cycle += 1 + gained += improved + log(f'sweep {sweep}: {improved} levels dropped, Lambda {total():.4f}; failed: no plan {f_plan}, cost {f_cost}, cycle {f_cycle}') + if improved == 0: break +best = total(); save('sweep') + +# ---------------- phase 2: annealing ---------------- +Temp = 0.02; it = acc = rej = 0; last_ck = time.time() +log(f'annealing until {MINUTES} min, seed {SEED}') +while time.time() < deadline: + it += 1 + txn = Txn(); before = cur_val + r = random.random() + if r < 0.5: + f = random.choice(free_fields); inner = [F for F in chain[f] if removable(f, F)] + if not inner: continue + ok = drop_level(f, random.choice(inner), txn) + elif r < 0.8: ok = reroute(random.choice(free_contacts), txn) + else: ok = new_frame(random.choice(free_contacts), txn) + if not ok: txn.rollback_state(); continue + drop_empty(txn) + after = total(); delta = after - before + if delta <= 0 or random.random() < math.exp(-delta / Temp): + if apply(txn): cur_val = after; acc += 1 + else: rej += 1 + else: txn.rollback_state() + if cur_val < best - 1e-12: best = cur_val; save('anneal') + Temp = max(0.002, Temp * 0.99998) + if time.time() - last_ck > 180: + last_ck = time.time() + log(f'it {it} acc {acc} cyc-rejected {rej} T {Temp:.4f} cur {cur_val:.4f} best {best:.4f}') +prof = save('final') +hist = collections.Counter(sum(1 for i in range(len(ch) - 1) if fdim(f, ch[i+1]) > fdim(f, ch[i])) for f, ch in enumerate(chain)) +log(f'FINAL best Lambda = {best:.4f} (word 23.8626); climbs/field hist {dict(sorted(hist.items()))}; climb profile {dict(sorted(prof.items()))}') +log('done jcr_search4') diff --git a/research/fragmentation-reorder-rigidity/search/jcr_search5.py b/research/fragmentation-reorder-rigidity/search/jcr_search5.py new file mode 100644 index 0000000000..3d40e15e60 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/jcr_search5.py @@ -0,0 +1,425 @@ +#!/usr/bin/env python3 +"""JCR search v4: same model as v3 (joint frame chains + contact frames, free scalar order within value +dependencies, warp frames fixed, 12 revisiting fields pinned), but with an INCREMENTAL acyclicity check +(Pearce-Kelly dynamic topological order) instead of a full graph rebuild per move, and a systematic sweep +phase before annealing. + +Graph nodes: the 18,149 ops (static DAG edges) plus dynamic level nodes entry/exit per (field, level) that +currently hosts contacts. Edges: entry(f,L) -> op -> exit(f,L) for every contact op at that level, and +exit(f,L_i) -> entry(f,L_{i+1}) along each chain; warp ops anchored between their two frames. +A move = a set of edge deletions followed by edge insertions; an insertion that closes a cycle rejects the move +and everything is rolled back. + +v5: free owned-centre read frames. +Usage: py -3.12 jcr_search5.py [minutes=60] [seed=1] +""" +import json, gzip, collections, os, time, sys, math, random +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)); LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s, flush=True); LOG.write(s + '\n'); LOG.flush() +MINUTES = float(sys.argv[1]) if len(sys.argv) > 1 else 60.0 +SEED = int(sys.argv[2]) if len(sys.argv) > 2 else 1 +random.seed(SEED) +t = 1 - 0.0030217759 +def pw(x): return 0.0 if x <= 0 else math.exp(t * math.log(x)) + +# ---------------- word ---------------- +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']); S = list(c['start']); T = list(c['final']); nm = 224 +prog = w['programs']['forward'] +def span_of(vs): + s = {0} + for v in vs: s |= {x ^ v for x in s} + return frozenset(s) +spans = [span_of(fr) for fr in frames]; span_id = {sp: i for i, sp in enumerate(spans)} +def fid(sp): + if sp not in span_id: span_id[sp] = len(spans); spans.append(sp) + return span_id[sp] +def dim(i): return len(spans[i]).bit_length() - 1 +def sub(a, b): return spans[a] <= spans[b] +def join(a, b): return a if a == b else fid(span_of(list(spans[a] | spans[b]))) +def meet(a, b): return fid(spans[a] & spans[b]) + +cur = list(S); chain0 = [[S[f]] for f in range(nf)]; pinned_f = set(); warp_frames = collections.defaultdict(set) +for e in prog: + if e[0] == 'climb': + f = e[2] + if e[4] in chain0[f]: pinned_f.add(f) + chain0[f].append(e[4]); cur[f] = e[4] + elif e[0] == 'warp': + f = e[1][1] + if e[4] != e[3]: + if e[4] in chain0[f]: pinned_f.add(f) + warp_frames[f].add(cur[f]); warp_frames[f].add(e[4]); chain0[f].append(e[4]) + cur[f] = e[4] +ops = []; contacts = []; warp_ops = []; barriers = []; block_ops = [] # phase markers are barriers +cur = list(S); visit = [0] * nf +def key_of(f): return ('v', visit[f]) if f in pinned_f else cur[f] +for e in prog: + if e[0] == 'climb': f = e[2]; cur[f] = e[4]; visit[f] += 1 + elif e[0] == 'warp': + f = e[1][1]; j = len(ops); ops.append((False, {('L', f)}, set())) + if e[4] != e[3]: warp_ops.append((j, f, visit[f], cur[f], e[4])); cur[f] = e[4]; visit[f] += 1 + elif e[0] == 'phase': + if e[1] in ('zero_frame_precondition', 'full_frame_cleanup', 'done') and not os.environ.get('JCR_NOBARRIER'): barriers.append(len(ops)) + ops.append((False, set(), set())) + elif e[0] == 'center': ops.append((False, {('L', e[2])}, set())) + elif e[0] == 'adapter': ops.append((False, {('L', e[2]), ('L', e[3])}, set())) + elif e[0] == 'scalar': + op = e[1]; kind = op[0]; roles = [tuple(r) for r in op[1:] if isinstance(r, list)] + W, Rd = ({roles[0]}, {roles[1]}) if kind in ('add', 'copy') else ({roles[0]}, set()) + j = len(ops); ops.append((kind == 'add', W, Rd)) + if kind in ('add', 'copy') and roles[0][0] == 'L' and roles[1][0] == 'L': + d, s = roles[0][1], roles[1][1]; F = e[2] + lo = join(S[d], S[s]); hi = meet(T[d], T[s]) + if not sub(lo, F): lo = F + contacts.append({'d': d, 's': s, 'op': j, 'lo': lo, 'hi': hi, 'F': F, 'kd': key_of(d), 'ks': key_of(s), + 'pin': (d in pinned_f or s in pinned_f)}) + elif kind in ('add', 'copy') and sum(r[0] == 'L' for r in roles) == 1 and not os.environ.get('JCR_NOC'): + f = next(r[1] for r in roles if r[0] == 'L'); F = e[2] + if kind == 'copy': # centre read: its frame may move along the source's chain (dim >= 1) + contacts.append({'d': f, 's': f, 'op': j, 'lo': S[f], 'hi': T[f], 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': f in pinned_f, 'K': True}) + else: # centre delivery at frame 0: pinned + contacts.append({'d': f, 's': f, 'op': j, 'lo': F, 'hi': F, 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': True, 'C': True}) + # 'scale' ops commute with climbs: they stay in the DAG only and take the field's current frame when emitted +n = len(ops) +pred = [set() for _ in range(n)] +# barrier edges: every op depends on the last phase marker before it, and the next marker depends on every op +bi = 0 +for j in range(n): + if bi < len(barriers) and j == barriers[bi]: + if bi > 0: + for k in range(barriers[bi - 1] + 1, j): pred[j].add(k) + bi += 1 + elif bi > 0: pred[j].add(barriers[bi - 1]) +last_write = {}; readers = collections.defaultdict(list); adds = collections.defaultdict(list) +for j, (is_add, W, Rd) in enumerate(ops): + for r in Rd: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(adds.get(r, [])) + for r in W: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(readers.get(r, [])) + if is_add: adds[r].append(j) + else: pred[j].update(adds.get(r, [])); last_write[r] = j; readers[r] = []; adds[r] = [] + for r in Rd: readers[r].append(j) + pred[j].discard(j) +log(f'JCR v4: fields {nf} (pinned {len(pinned_f)}), contacts {len(contacts)}, ops {n}, dag edges {sum(len(p) for p in pred)}, frames {len(spans)}') + +# ---------------- dynamic graph with Pearce-Kelly order ---------------- +class DynGraph: + def __init__(self, nstatic, pred): + self.out = [set() for _ in range(nstatic)]; self.inn = [set() for _ in range(nstatic)] + for j in range(nstatic): + for k in pred[j]: self.out[k].add(j); self.inn[j].add(k) + self.ord = list(range(nstatic)) # node -> position + self.free = [] + def new_node(self): + if self.free: u = self.free.pop(); self.out[u] = set(); self.inn[u] = set(); return u + u = len(self.out); self.out.append(set()); self.inn.append(set()); self.ord.append(self.ord and max(self.ord) + 1 or 0) + return u + def del_node(self, u): + for v in list(self.out[u]): self.del_edge(u, v) + for v in list(self.inn[u]): self.del_edge(v, u) + self.free.append(u) + def del_edge(self, u, v): self.out[u].discard(v); self.inn[v].discard(u) + def add_edge(self, u, v): + """returns False (and leaves the graph unchanged) if the edge would close a cycle.""" + if v in self.out[u]: return True + ord = self.ord + if ord[u] < ord[v]: self.out[u].add(v); self.inn[v].add(u); return True + lb, ub = ord[v], ord[u] + # forward from v within (.., ub] + Rf = []; seen = {v}; st = [v] + while st: + x = st.pop(); Rf.append(x) + for y in self.out[x]: + if y == u: return False + if y not in seen and ord[y] <= ub: seen.add(y); st.append(y) + Rb = []; seenb = {u}; st = [u] + while st: + x = st.pop(); Rb.append(x) + for y in self.inn[x]: + if y not in seenb and ord[y] >= lb: seenb.add(y); st.append(y) + # reorder: nodes of Rb then Rf take the sorted positions of Rb ∪ Rf + Rb.sort(key=lambda x: ord[x]); Rf.sort(key=lambda x: ord[x]) + pos = sorted(ord[x] for x in Rb + Rf) + for x, p in zip(Rb + Rf, pos): ord[x] = p + self.out[u].add(v); self.inn[v].add(u); return True + +G = DynGraph(n, pred) + +# ---------------- state ---------------- +chain = []; frame_of = {} +for f in range(nf): + if f in pinned_f: + keys = [('v', i) for i in range(len(chain0[f]))] + for i, fr in enumerate(chain0[f]): frame_of[(f, ('v', i))] = fr + else: + keys = [] + for fr in chain0[f]: + if fr not in keys: keys.append(fr) + frame_of[(f, fr)] = fr + chain.append(keys) +cset = [set(ch) for ch in chain] +at = collections.defaultdict(set) +for k, e in enumerate(contacts): at[(e['d'], e['kd'])].add(k); at[(e['s'], e['ks'])].add(k) +lvnode = {} # (f, key) -> (entry, exit) for levels with contacts +def fdim(f, key): return dim(frame_of[(f, key)]) +def lam_field(f): + ds = [fdim(f, k) for k in chain[f]] + return sum(pw(ds[i+1] - ds[i]) for i in range(len(ds) - 1)) - pw(ds[-1] - ds[0]) +LAM = [lam_field(f) for f in range(nf)] +KC = [k for k, e in enumerate(contacts) if e.get('K')] +def centre_term(): return sum(pw(dim(contacts[k]['F'])) for k in KC) - 8 * pw(8) +def total(): return sum(LAM) + centre_term() + +# build initial level graph in word order (cannot fail) +def active_levels(f): return [k for k in chain[f] if (f, k) in lvnode] +for f in range(nf): + for key in chain[f]: + if at.get((f, key)): + ent, ex = G.new_node(), G.new_node(); lvnode[(f, key)] = (ent, ex) + for k in at[(f, key)]: + o = contacts[k]['op']; assert G.add_edge(ent, o) and G.add_edge(o, ex) + al = active_levels(f) + for a, b in zip(al, al[1:]): assert G.add_edge(lvnode[(f, a)][1], lvnode[(f, b)][0]) +def warp_anchor_edges(j, f, va, A, B): + """edges (u, v) anchoring warp op j for the current chain of f.""" + out = []; ch = chain[f] + if f in pinned_f: + for key in ch: + if (f, key) not in lvnode: continue + if key[1] <= va: out.append((lvnode[(f, key)][1], j)) + else: out.append((j, lvnode[(f, key)][0])) + else: + pa, pb = ch.index(A), ch.index(B) + for i, key in enumerate(ch): + if (f, key) not in lvnode: continue + if i <= pa: out.append((lvnode[(f, key)][1], j)) + elif i >= pb: out.append((j, lvnode[(f, key)][0])) + return out +for wo in warp_ops: + for u, v in warp_anchor_edges(*wo): assert G.add_edge(u, v) +warps_of = collections.defaultdict(list) +for wo in warp_ops: warps_of[wo[1]].append(wo) +log(f'initial Lambda = {total():.4f}; dynamic graph built, nodes {len(G.out)}') + +# ---------------- transactional edits ---------------- +class Txn: + """collects structural changes; graph edges are re-derived for touched fields and applied with rollback.""" + def __init__(self): self.touched = set(); self.undo = []; self.added = []; self.removed = [] + def set_contact(self, k, Fnew): + e = contacts[k]; self.undo.append(('c', k, e['F'], e['kd'], e['ks'])) + at[(e['d'], e['kd'])].discard(k); at[(e['s'], e['ks'])].discard(k) + e['F'] = Fnew; e['kd'] = Fnew; e['ks'] = Fnew + at[(e['d'], Fnew)].add(k); at[(e['s'], Fnew)].add(k); self.touched.update((e['d'], e['s'])) + def insert_frame(self, f, F): + pos = len(chain[f]) + for i, x in enumerate(chain[f]): + if dim(x) > dim(F): pos = i; break + chain[f].insert(pos, F); cset[f].add(F); frame_of[(f, F)] = F; LAM[f] = lam_field(f) + self.undo.append(('i', f, F)); self.touched.add(f) + def remove_frame(self, f, F): + chain[f].remove(F); cset[f].discard(F); at.pop((f, F), None); frame_of.pop((f, F), None); LAM[f] = lam_field(f) + self.undo.append(('r', f, F)); self.touched.add(f) + def rollback_state(self): + while self.undo: + kind, *a = self.undo.pop() + if kind == 'c': + k, F, kd, ks = a; e = contacts[k] + at[(e['d'], e['kd'])].discard(k); at[(e['s'], e['ks'])].discard(k) + e['F'], e['kd'], e['ks'] = F, kd, ks; at[(e['d'], kd)].add(k); at[(e['s'], ks)].add(k) + elif kind == 'i': + f, F = a; chain[f].remove(F); cset[f].discard(F); frame_of.pop((f, F), None); LAM[f] = lam_field(f) + else: + f, F = a; pos = len(chain[f]) + for i, x in enumerate(chain[f]): + if dim(x) > dim(F): pos = i; break + chain[f].insert(pos, F); cset[f].add(F); frame_of[(f, F)] = F; LAM[f] = lam_field(f) + +def level_edges(f): + """all graph edges owned by field f's level structure (contact edges, chain edges, warp anchors).""" + E = set() + al = active_levels(f) + for key in al: + ent, ex = lvnode[(f, key)] + for k in at[(f, key)]: + o = contacts[k]['op']; E.add((ent, o)); E.add((o, ex)) + for a, b in zip(al, al[1:]): E.add((lvnode[(f, a)][1], lvnode[(f, b)][0])) + for wo in warps_of.get(f, []): E.update(warp_anchor_edges(*wo)) + return E + +def commit_graph(txn): + """re-derive the level graph of touched fields; return True if acyclic (edges applied), else rollback edges.""" + old = {} + for f in txn.touched: old[f] = level_edges_snapshot[f] + # create/delete level nodes according to current `at` + newnodes = []; delnodes = [] + for f in txn.touched: + for key in chain[f]: + has = bool(at.get((f, key))) + if has and (f, key) not in lvnode: lvnode[(f, key)] = (G.new_node(), G.new_node()); newnodes.append((f, key)) + for (ff, key) in [x for x in lvnode if x[0] == f]: + if key not in chain[f] or not at.get((f, key)): delnodes.append((f, key)) + new = {} + for f in txn.touched: new[f] = level_edges(f) + oldE = set().union(*old.values()) if old else set(); newE = set().union(*new.values()) if new else set() + for u, v in oldE - newE: G.del_edge(u, v) + added = [] + ok = True + for u, v in newE - oldE: + if not G.add_edge(u, v): ok = False; break + added.append((u, v)) + if not ok: + for u, v in added: G.del_edge(u, v) + for u, v in oldE - newE: assert G.add_edge(u, v) + for fk in newnodes: ent, ex = lvnode.pop(fk); G.del_node(ent); G.del_node(ex) + return False + for fk in delnodes: + ent, ex = lvnode.pop(fk); G.del_node(ent); G.del_node(ex) + for f in txn.touched: level_edges_snapshot[f] = new[f] + return True +level_edges_snapshot = [level_edges(f) for f in range(nf)] + +def apply(txn): + """finish a transaction: graph check; on failure roll back state too.""" + if commit_graph(txn): return True + txn.rollback_state() + # level nodes for fields whose `at` was restored may need re-creation on the next commit; keep lvnode consistent: + for f in txn.touched: + for key in chain[f]: + if at.get((f, key)) and (f, key) not in lvnode: + lvnode[(f, key)] = (G.new_node(), G.new_node()) + for k in at[(f, key)]: + o = contacts[k]['op']; assert G.add_edge(lvnode[(f, key)][0], o) and G.add_edge(o, lvnode[(f, key)][1]) + level_edges_snapshot[f] = level_edges(f) + return False + +def nested_ok(f, F): + return f not in pinned_f and all(sub(x, F) or sub(F, x) for x in chain[f]) and sub(S[f], F) and sub(F, T[f]) +def removable(f, F): return f not in pinned_f and F != S[f] and F != T[f] and F not in warp_frames[f] + +def drop_level(f, F, txn): + if not removable(f, F): return False + plan = [] + for k in list(at.get((f, F), [])): + e = contacts[k] + if e['pin']: return False + g = e['s'] if e['d'] == f else e['d'] + opts = [X for X in chain[f] if X != F and sub(e['lo'], X) and sub(X, e['hi'])] + if e.get('U') or e.get('K'): + if e.get('K'): opts = [X for X in opts if dim(X) >= 1] + if not opts: return False + plan.append((k, random.choice(opts), None)); continue + common = [X for X in opts if X in cset[g]] + if common: plan.append((k, random.choice(common), None)); continue + ins = [X for X in opts if nested_ok(g, X)] + if not ins: return False + plan.append((k, random.choice(ins), g)) + for k, X, g in plan: + if g is not None and X not in cset[g]: txn.insert_frame(g, X) + txn.set_contact(k, X) + txn.remove_frame(f, F); return True +def reroute(k, txn): + e = contacts[k] + if e['pin']: return False + d, s = e['d'], e['s'] + opts = [X for X in chain[d] if X in cset[s] and X != e['F'] and sub(e['lo'], X) and sub(X, e['hi'])] + if e.get('K'): opts = [X for X in opts if dim(X) >= 1] + if e.get('U') and opts: txn.set_contact(k, random.choice(opts)); return True + if not opts: return False + txn.set_contact(k, random.choice(opts)); return True +def new_frame(k, txn): + e = contacts[k] + if e['pin'] or e.get('U') or e.get('K'): return False + d, s = e['d'], e['s'] + cand = [X for X in random.sample(range(len(spans)), 40) if X != e['F'] and sub(e['lo'], X) and sub(X, e['hi']) + and (X in cset[d] or nested_ok(d, X)) and (X in cset[s] or nested_ok(s, X))] + if not cand: return False + X = random.choice(cand) + if X not in cset[d]: txn.insert_frame(d, X) + if X not in cset[s]: txn.insert_frame(s, X) + txn.set_contact(k, X); return True +def drop_empty(txn): + for f in list(txn.touched): + for F in list(chain[f]): + if removable(f, F) and not at.get((f, F)): txn.remove_frame(f, F) + +free_fields = [f for f in range(nf) if f not in pinned_f]; free_contacts = [k for k, e in enumerate(contacts) if not e['pin']] +best = total(); cur_val = best +def save(tag): + prof = collections.Counter() + for f in range(nf): + ds = [fdim(f, k) for k in chain[f]] + for i in range(len(ds) - 1): + if ds[i+1] > ds[i]: prof[ds[i+1] - ds[i]] += 1 + # topological order of all graph nodes (Kahn on the dynamic graph), ops only + indeg = {u: len(G.inn[u]) for u in range(len(G.out)) if u < n or (G.out[u] or G.inn[u])} + ready = sorted([u for u, dg in indeg.items() if dg == 0], key=lambda u: G.ord[u]); order = [] + import heapq + heap = [(G.ord[u], u) for u in ready]; heapq.heapify(heap) + while heap: + _, u = heapq.heappop(heap); order.append(u) + for v_ in G.out[u]: + indeg[v_] -= 1 + if indeg[v_] == 0: heapq.heappush(heap, (G.ord[v_], v_)) + assert len(order) == len(indeg), 'cyclic at save' + for k in KC: prof[dim(contacts[k]['F'])] += 1 # centre transports at their actual rank (profile then includes the centre) + json.dump({'best': best, 'profile': dict(prof), 'centre_included': True, 'centre_read_dims': [dim(contacts[k]['F']) for k in KC], 'chains': [[str(k) for k in ch] for ch in chain], + 'chain_frames': [[frame_of[(f, k)] for k in ch] for f, ch in enumerate(chain)], + 'contact_frames': [e['F'] for e in contacts], 'contact_ops': [e['op'] for e in contacts], + 'op_order': [u for u in order if u < n], 'extra_frames': [sorted(spans[i]) for i in range(len(frames), len(spans))], 'tag': tag}, + open(os.path.join(HERE, f'jcr4_state_seed{SEED}.json'), 'w')) + return prof + +# ---------------- phase 1: systematic sweep (greedy, downhill only) ---------------- +start = time.time(); deadline = start + MINUTES * 60 +sweep = 0; gained = 0 +while time.time() < deadline and sweep < 3: + sweep += 1; improved = 0; f_plan = f_cost = f_cycle = 0 + order = list(free_fields); random.shuffle(order) + for f in order: + for F in list(chain[f]): + if not removable(f, F) or F not in chain[f]: continue + txn = Txn(); before = total() + if not drop_level(f, F, txn): txn.rollback_state(); f_plan += 1; continue + drop_empty(txn) + if total() > before + 1e-12: txn.rollback_state(); f_cost += 1; continue + if apply(txn): improved += 1; cur_val = total() + else: f_cycle += 1 + gained += improved + log(f'sweep {sweep}: {improved} levels dropped, Lambda {total():.4f}; failed: no plan {f_plan}, cost {f_cost}, cycle {f_cycle}') + if improved == 0: break +best = total(); save('sweep') + +# ---------------- phase 2: annealing ---------------- +Temp = 0.02; it = acc = rej = 0; last_ck = time.time() +log(f'annealing until {MINUTES} min, seed {SEED}') +while time.time() < deadline: + it += 1 + txn = Txn(); before = cur_val + r = random.random() + if r < 0.5: + f = random.choice(free_fields); inner = [F for F in chain[f] if removable(f, F)] + if not inner: continue + ok = drop_level(f, random.choice(inner), txn) + elif r < 0.8: ok = reroute(random.choice(free_contacts), txn) + else: ok = new_frame(random.choice(free_contacts), txn) + if not ok: txn.rollback_state(); continue + drop_empty(txn) + after = total(); delta = after - before + if delta <= 0 or random.random() < math.exp(-delta / Temp): + if apply(txn): cur_val = after; acc += 1 + else: rej += 1 + else: txn.rollback_state() + if cur_val < best - 1e-12: best = cur_val; save('anneal') + Temp = max(0.002, Temp * 0.99998) + if time.time() - last_ck > 180: + last_ck = time.time() + log(f'it {it} acc {acc} cyc-rejected {rej} T {Temp:.4f} cur {cur_val:.4f} best {best:.4f}') +prof = save('final') +hist = collections.Counter(sum(1 for i in range(len(ch) - 1) if fdim(f, ch[i+1]) > fdim(f, ch[i])) for f, ch in enumerate(chain)) +log(f'FINAL best Lambda+centre = {best:.4f} (word 23.8626); climbs/field hist {dict(sorted(hist.items()))}; profile incl. centre {dict(sorted(prof.items()))}; centre read dims {[dim(contacts[k]["F"]) for k in KC]}') +log('done jcr_search4') diff --git a/research/fragmentation-reorder-rigidity/search/make_v5.py b/research/fragmentation-reorder-rigidity/search/make_v5.py new file mode 100644 index 0000000000..054edf643d --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/make_v5.py @@ -0,0 +1,77 @@ +"""Derive jcr_search5.py from jcr_search4.py: the owned-centre walk is free. +Each of the 8 centre blocks reads one source field by `copy C0 = X` at a frame R_b (dim 8 in the word), transports +C0 from R_b to frame 0 (rank dim R_b) and delivers to 22 targets at frame 0. v5 lets R_b be any frame of the source's +chain (dim >= 1); the centre bill in the objective becomes sum_b (dim R_b)^t instead of 8 * 8^t. Delivery contacts +(target += C0 at frame 0) stay pinned. Also patches build_word.py -> build_word5.py to emit the matching clear/center events.""" +s = open('jcr_search4.py', encoding='utf-8').read() +def rep(old, new): + global s + assert old in s, old[:70] + s = s.replace(old, new) +rep('Usage: py -3.12 jcr_search4.py [minutes=60] [seed=1]', 'v5: free owned-centre read frames.\nUsage: py -3.12 jcr_search5.py [minutes=60] [seed=1]') +rep(""" f = next(r[1] for r in roles if r[0] == 'L'); F = e[2] # contact with the owned C0 buffer: pinned + contacts.append({'d': f, 's': f, 'op': j, 'lo': F, 'hi': F, 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': True, 'C': True})""", +""" f = next(r[1] for r in roles if r[0] == 'L'); F = e[2] + if kind == 'copy': # centre read: its frame may move along the source's chain (dim >= 1) + contacts.append({'d': f, 's': f, 'op': j, 'lo': S[f], 'hi': T[f], 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': f in pinned_f, 'K': True}) + else: # centre delivery at frame 0: pinned + contacts.append({'d': f, 's': f, 'op': j, 'lo': F, 'hi': F, 'F': F, 'kd': key_of(f), 'ks': key_of(f), 'pin': True, 'C': True})""") +rep("""LAM = [lam_field(f) for f in range(nf)] +def total(): return sum(LAM)""", +"""LAM = [lam_field(f) for f in range(nf)] +KC = [k for k, e in enumerate(contacts) if e.get('K')] +def centre_term(): return sum(pw(dim(contacts[k]['F'])) for k in KC) - 8 * pw(8) +def total(): return sum(LAM) + centre_term()""") +rep(""" if e.get('U'): + if not opts: return False + plan.append((k, random.choice(opts), None)); continue + common = [X for X in opts if X in cset[g]]""", +""" if e.get('U') or e.get('K'): + if e.get('K'): opts = [X for X in opts if dim(X) >= 1] + if not opts: return False + plan.append((k, random.choice(opts), None)); continue + common = [X for X in opts if X in cset[g]]""") +rep(""" if e.get('U') and opts: txn.set_contact(k, random.choice(opts)); return True + if not opts: return False""", +""" if e.get('K'): opts = [X for X in opts if dim(X) >= 1] + if e.get('U') and opts: txn.set_contact(k, random.choice(opts)); return True + if not opts: return False""") +rep(""" if e['pin'] or e.get('U'): return False""", """ if e['pin'] or e.get('U') or e.get('K'): return False""") +rep(""" json.dump({'best': best, 'profile': dict(prof), 'chains': [[str(k) for k in ch] for ch in chain],""", +""" for k in KC: prof[dim(contacts[k]['F'])] += 1 # centre transports at their actual rank (profile then includes the centre) + json.dump({'best': best, 'profile': dict(prof), 'centre_included': True, 'centre_read_dims': [dim(contacts[k]['F']) for k in KC], 'chains': [[str(k) for k in ch] for ch in chain],""") + +rep("""log(f'FINAL best Lambda = {best:.4f} (word 23.8626); climbs/field hist {dict(sorted(hist.items()))}; climb profile {dict(sorted(prof.items()))}')""", + """log(f'FINAL best Lambda+centre = {best:.4f} (word 23.8626); climbs/field hist {dict(sorted(hist.items()))}; profile incl. centre {dict(sorted(prof.items()))}; centre read dims {[dim(contacts[k]["F"]) for k in KC]}')""") +open('jcr_search5.py', 'w', encoding='utf-8').write(s) +open('run_jcr5.bat', 'w').write(open('run_jcr4.bat').read().replace('jcr_search4.py', 'jcr_search5.py').replace('jcr4_seed', 'jcr5_seed')) +# builder: centre clear / center events follow the copy frame +b = open('build_word.py', encoding='utf-8').read() +old = """ elif e[0] == 'phase' and e[1] == 'done':""" +assert old in b +b = b.replace("""def build(prog): + out = []""", """# centre blocks: the clear before a copy and the center transport after it take the copy's frame +copy_frame_after = {} # original event index of a C0 clear (dim 8) or center -> op index of the block's copy +for i, e in enumerate(fw): + if e[0] == 'scalar' and e[1][0] == 'copy' and e[1][1] == ['C', 0]: + u = op_events.index(i) + for j in range(i - 1, -1, -1): + if fw[j][0] == 'scalar' and fw[j][1][0] == 'clear': copy_frame_after[j] = u; break + for j in range(i + 1, len(fw)): + if fw[j][0] == 'center': copy_frame_after[j] = u; break +def build(prog): + out = []""") +b = b.replace(""" else: Fr = e[2] # ops that only touch C0 keep their frame + for f in Lf: out.extend(climb_events(f, Fr)) + out.append(['scalar', g, Fr])""", """ elif i in copy_frame_after: Fr = contact_frame_of_op[copy_frame_after[i]] # clear C0 before the centre read + else: Fr = e[2] # ops that only touch C0 keep their frame + for f in Lf: out.extend(climb_events(f, Fr)) + out.append(['scalar', g, Fr])""") +b = b.replace(""" else: + out.append(e) # center / adapter / phase""", """ elif e[0] == 'center' and i in copy_frame_after: + R = contact_frame_of_op[copy_frame_after[i]] + out.append(['center', e[1], R, e[3], abs(dim(R) - dim(e[3]))]) + else: + out.append(e) # adapter / phase""") +open('build_word5.py', 'w', encoding='utf-8').write(b) +print('v5 written') diff --git a/research/fragmentation-reorder-rigidity/search/nested_facts.py b/research/fragmentation-reorder-rigidity/search/nested_facts.py new file mode 100644 index 0000000000..c6307d75fd --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/nested_facts.py @@ -0,0 +1,68 @@ +#!/usr/bin/env python3 +"""Facts needed for an order-free, frame-exact chain relaxation of #4610: + (1) is every frame of a field's chain a superspace of its start frame (nestedness through warps)? + (2) at every contact, do both start frames lie in the common frame, and does the common frame lie in both final frames? + (3) interval per contact: lower = S_d + S_s, upper = T_d & T_s; dims of lower/current/upper. + (4) per main field: number of distinct other ports it contacts directly (main-main) and via helpers.""" +import json, gzip, collections, os, time +W3 = 'D:/Math/imb-docking/research/kappa-round3-warp-20261022/' +HERE = os.path.dirname(os.path.abspath(__file__)); LOG = open(os.path.join(HERE, 'progress.log'), 'a') +def log(*a): + s = time.strftime('%H:%M:%S ') + ' '.join(str(x) for x in a); print(s); LOG.write(s + '\n'); LOG.flush() +w = json.loads(gzip.decompress(open(W3 + 'ACTUAL-WORD.json.gz', 'rb').read())) +c = w['canonical']; frames = c['frames']; nf = len(c['start']); S = list(c['start']); T = list(c['final']); nm = 224 +SP = {} +def sp(fi): + if fi not in SP: + s = {0} + for v in frames[fi]: s |= {x ^ v for x in s} + SP[fi] = frozenset(s) + return SP[fi] +def dim(s): return len(s).bit_length() - 1 +cur = list(S); chain = [[S[f]] for f in range(nf)]; cont = [] +for e in w['programs']['forward']: + if e[0] == 'climb': f = e[2]; cur[f] = e[4]; chain[f].append(e[4]) + elif e[0] == 'warp': + f = e[1][1]; cur[f] = e[4] + if e[4] != e[3]: chain[f].append(e[4]) + elif e[0] == 'scalar': + op = e[1]; roles = [r for r in op[1:] if isinstance(r, list) and r[0] == 'L'] + if op[0] in ('add', 'copy') and len(roles) == 2: cont.append((roles[0][1], roles[1][1], e[2])) +# (1) nestedness +viol = 0; warpviol = 0 +for f in range(nf): + s0 = sp(S[f]) + for i, fr in enumerate(chain[f]): + if not s0 <= sp(fr): viol += 1 + if i and not sp(chain[f][i-1]) <= sp(fr): warpviol += 1 +log(f'(1) chain frames not containing the start frame: {viol}; non-nested consecutive chain steps (warps): {warpviol} of {sum(len(ch)-1 for ch in chain)}') +# (2),(3) +lo_ok = up_ok = 0; room = collections.Counter(); exact_lower = exact_upper = 0 +for d, s, F in cont: + lower = sp(S[d]) | sp(S[s]); lowspan = set(lower) + for v in list(lower): + lowspan |= {x ^ v for x in lowspan} + lowspan = frozenset(lowspan); upper = sp(T[d]) & sp(T[s]); cf = sp(F) + if lowspan <= cf: lo_ok += 1 + if cf <= upper: up_ok += 1 + room[(dim(lowspan), dim(cf), dim(upper))] += 1 + if dim(lowspan) == dim(cf): exact_lower += 1 + if dim(upper) == dim(cf): exact_upper += 1 +log(f'(2) contacts {len(cont)}: start frames inside common frame {lo_ok}; common frame inside both finals {up_ok}') +log(f'(3) contacts at the interval bottom (dim F = dim(S_d+S_s)): {exact_lower}; at the top (dim F = dim(T_d & T_s)): {exact_upper}; strictly inside: {len(cont)-exact_lower-exact_upper + sum(1 for (a,b,c_),n in room.items() if a==b==c_ for _ in range(n))}') +log('(3) (dim lower, dim F, dim upper) histogram, top 25: ' + str(sorted(room.items(), key=lambda kv: -kv[1])[:25])) +# (4) ports per main +port_of = {} +for p, line in enumerate(c['ports']): + for f in range(nm): + if frames[S[f]] == [line] or (len(frames[S[f]]) == 0 and False): port_of.setdefault(f, p) +# mains: X_p starts at q_p (dim 1); Y_p starts at 0 -> identify by final frame = q_p^perp? use pairing: assume field index f<112 -> X, 112<=f<224 -> Y with same port order +mm = collections.defaultdict(set); mh = collections.defaultdict(set); hm = collections.defaultdict(set) +for d, s, F in cont: + for a, b in ((d, s), (s, d)): + if a < nm and b < nm: mm[a].add(b % 112) + elif a < nm: mh[a].add(b) + else: hm[a].add(b % 112) +pm = collections.Counter(len(v - {f % 112}) for f, v in mm.items()); ph = collections.Counter(len(v) for v in hm.values()) +log(f'(4) distinct other ports contacted main-main per main: {dict(sorted(pm.items()))}; distinct ports contacted per helper: {dict(sorted(ph.items()))}') +log(f' mains with no main-main contact: {nm - len(mm)}; mean helpers per main {sum(len(v) for v in mh.values())/nm:.1f}') diff --git a/research/fragmentation-reorder-rigidity/test_verify.py b/research/fragmentation-reorder-rigidity/test_verify.py new file mode 100644 index 0000000000..ab96d42c92 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/test_verify.py @@ -0,0 +1,76 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit('FAIL...').""" +import collections +import copy +import gzip +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +word = json.loads(gzip.decompress((V.W3 / 'ACTUAL-WORD.json.gz').read_bytes())) +arith = json.loads((V.W3 / 'ARITHMETIC.json').read_text(encoding='utf-8')) + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith('FAIL'): + raise + print('rejected:', name) + return + raise AssertionError('control accepted: ' + name) + + +def drift(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + rows['files'][0]['sha256'] = '0' * 64 + orig = V.pinned_inputs + def patched(): + for row in rows['files']: + if row['usage'] == 'input': + data = (V.ROOT / row['path']).read_bytes() + V.require(V.hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + patched() + + +def bad_rank(): + bad = copy.deepcopy(word) + e = next(ev for ev in bad['programs']['forward'] if ev[0] == 'climb') + e[5] += 1 + w = V.Word(bad, arith) + prof = collections.Counter(w.climb_profile()); prof[8] += 8 + V.require(dict(prof) == w.N, 'climb profile + 8 centre jobs equals ARITHMETIC local_paid') + + +def frame_mismatch(): + bad = copy.deepcopy(word) + e = next(ev for ev in bad['programs']['forward'] if ev[0] == 'scalar' and ev[1][0] == 'add' and ev[1][1][0] == 'L' and ev[1][2][0] == 'L' and ev[2] != 0) + e[2] = 0 + V.Word(bad, arith) + + +def tampered_result(): + stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + stored['exact']['improving'] = 1 + V.require(stored['exact']['improving'] == 0, 'stored RESULT.json equals the rebuilt result') + + +def live_test(): + """ignoring the centre interface must produce feasible drops (otherwise the enumeration would be vacuous).""" + w = V.Word(word, arith, pin_centre=False) + LG = V.LevelGraph(w); LG.index_owners() + res, feas, capped = V.drop_test(w, LG) + V.require(res['improving'] >= 5, 'drop test finds improving drops without the centre interface') + print('live: improving drops without the centre interface', res['improving']) + + +rejects('drifted input hash', drift) +rejects('corrupted climb rank', bad_rank) +rejects('contact frame mismatch', frame_mismatch) +rejects('tampered stored result', tampered_result) +live_test() +print('PASS_FRAGMENTATION_REORDER_RIGIDITY_CONTROLS') diff --git a/research/fragmentation-reorder-rigidity/verify.py b/research/fragmentation-reorder-rigidity/verify.py new file mode 100644 index 0000000000..6f113adcb9 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/verify.py @@ -0,0 +1,501 @@ +#!/usr/bin/env python3 +"""The fragmentation of the #4610 word is rigid under free scalar reordering. + +Standard library only; about 2-4 minutes. Reads Cao Yifan's final PR4610 word +(research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz) and its ARITHMETIC.json, +both pinned by SHA256 in SOURCES.json. + +Model (the retained frame contract of #4610 / #5226, with the chronological order freed): + * every persistent field f occupies a nested chain of frames S_f = F_0 < ... < F_k = T_f + (binary subspaces); a climb F_i < F_{i+1} is a paid job of rank dim F_{i+1} - dim F_i and the + fragmentation loss of the field is Lambda_f(t) = sum_j rank_j^t - R_f^t (#5226, Theorem B); + * a two-field scalar contact (ADD/COPY) happens at ONE common frame that both chains contain, + inside the interval S_d + S_s <= F <= T_d & T_s; + * a scalar contact with the owned centre buffer C0 needs the field at the frame the centre walk + uses: the eight centre reads (COPY C0 <- source) may move to any frame of the source's chain of + dimension >= 1 (the transport C0 -> frame 0 then costs that dimension), the 176 deliveries + (target += C0 at frame 0) are fixed; + * scalar operations, warps, centre transports and adapters keep their value dependencies + (write/read and write/write conflicts; ADDs into one destination commute), the three + interpreter-visible phase markers (zero_frame_precondition, full_frame_cleanup, done) are + barriers, every native warp is anchored between its two frames, and along each field the + contacts occur in non-decreasing chain order (no descents). +A "level" of a field is an intermediate frame of its chain that hosts at least one contact. +Dropping a level means re-routing all its contacts to other frames of the chain (possibly adding +a frame to a partner's chain) and merging the two adjacent climbs into one; every such re-routing +is enumerated and tested for feasibility by an exact acyclicity check of the operation/level graph. + +Result: no level of any field can be dropped. Controls show the test is live. +Usage: python3 -I -B verify.py [--write] +""" +import argparse, collections, gzip, hashlib, itertools, json, math, sys, time +from pathlib import Path +from decimal import Decimal as D, getcontext + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +W3 = ROOT / 'research' / 'kappa-round3-warp-20261022' +getcontext().prec = 40 + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +# ---------------------------------------------------------------------------------------------- +# word model +# ---------------------------------------------------------------------------------------------- +class Word: + def __init__(self, word, arithmetic, centre_free=True, pin_centre=True, barriers=True): + c = word['canonical']; self.c = c + self.frames = list(c['frames']); self.nf = len(c['start']); self.S = list(c['start']); self.T = list(c['final']) + self.H = {int(k): n for k, n in arithmetic['local_helpers'].items()} + self.N = {int(k): n for k, n in arithmetic['local_paid'].items()} + self.nm = self.nf - sum(self.H.values()) + self.spans = [self.span_of(fr) for fr in self.frames] + self.span_id = {sp: i for i, sp in enumerate(self.spans)} + prog = word['programs']['forward']; self.prog = prog + S, T, nf = self.S, self.T, self.nf + # pass 1: visit sequences, pinned (revisiting) fields, warp frames + cur = list(S); chain0 = [[S[f]] for f in range(nf)]; pinned = set(); warp_frames = collections.defaultdict(set) + for e in prog: + if e[0] == 'climb': + f = e[2] + require(cur[f] == e[3] and self.spans[e[3]] < self.spans[e[4]] and e[5] == self.dim(e[4]) - self.dim(e[3]), 'nested climb with its paid rank') + if e[4] in chain0[f]: pinned.add(f) + chain0[f].append(e[4]); cur[f] = e[4] + elif e[0] == 'warp': + f = e[1][1] + if e[4] != e[3]: + if e[4] in chain0[f]: pinned.add(f) + warp_frames[f].update((cur[f], e[4])); chain0[f].append(e[4]) + cur[f] = e[4] + self.chain0, self.pinned, self.warp_frames = chain0, pinned, warp_frames + # pass 2: ops (DAG nodes), contacts with level keys + ops = []; contacts = []; warp_ops = []; barrier_ops = [] + cur = list(S); visit = [0] * nf + key_of = lambda f: ('v', visit[f]) if f in pinned else cur[f] + for e in prog: + kind = e[0] + if kind == 'climb': + f = e[2]; cur[f] = e[4]; visit[f] += 1 + elif kind == 'warp': + f = e[1][1]; j = len(ops); ops.append((False, {('L', f)}, set())) + if e[4] != e[3]: + warp_ops.append((j, f, visit[f], cur[f], e[4])); cur[f] = e[4]; visit[f] += 1 + elif kind == 'phase': + if barriers and e[1] in ('zero_frame_precondition', 'full_frame_cleanup', 'done'): barrier_ops.append(len(ops)) + ops.append((False, set(), set())) + elif kind == 'center': ops.append((False, {('L', e[2])}, set())) + elif kind == 'adapter': ops.append((False, {('L', e[2]), ('L', e[3])}, set())) + elif kind == 'scalar': + op = e[1]; k = op[0]; roles = [tuple(r) for r in op[1:] if isinstance(r, list)] + W, Rd = ({roles[0]}, {roles[1]}) if k in ('add', 'copy') else ({roles[0]}, set()) + j = len(ops); ops.append((k == 'add', W, Rd)) + L = [r[1] for r in roles if r[0] == 'L'] + if k in ('add', 'copy') and len(L) == 2: + d, s = L; F = e[2] + require(cur[d] == F and cur[s] == F, 'contact frame mismatch in the word') + lo = self.join(S[d], S[s]); hi = self.meet(T[d], T[s]) + if not self.sub(lo, F): lo = F # 135 contacts of the word sit below S_d+S_s (warped fields) + contacts.append(dict(d=d, s=s, op=j, lo=lo, hi=hi, F=F, kd=key_of(d), ks=key_of(s), + pin=(d in pinned or s in pinned), kind='LL')) + elif k in ('add', 'copy') and len(L) == 1 and pin_centre: + f = L[0]; F = e[2] + if k == 'copy' and centre_free: + contacts.append(dict(d=f, s=f, op=j, lo=S[f], hi=T[f], F=F, kd=key_of(f), ks=key_of(f), pin=f in pinned, kind='Cread')) + else: + contacts.append(dict(d=f, s=f, op=j, lo=F, hi=F, F=F, kd=key_of(f), ks=key_of(f), pin=True, kind='Cdeliver' if k == 'add' else 'Cread')) + else: + raise SystemExit('FAIL: unknown event ' + kind) + self.ops, self.contacts, self.warp_ops = ops, contacts, warp_ops + n = len(ops); self.n = n + pred = [set() for _ in range(n)] + last_write = {}; readers = collections.defaultdict(list); adds = collections.defaultdict(list) + for j, (is_add, W, Rd) in enumerate(ops): + for r in Rd: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(adds.get(r, [])) + for r in W: + if r in last_write: pred[j].add(last_write[r]) + pred[j].update(readers.get(r, [])) + if is_add: adds[r].append(j) + else: + pred[j].update(adds.get(r, [])); last_write[r] = j; readers[r] = []; adds[r] = [] + for r in Rd: readers[r].append(j) + pred[j].discard(j) + bi = 0 + for j in range(n): + if bi < len(barrier_ops) and j == barrier_ops[bi]: + if bi > 0: pred[j].update(range(barrier_ops[bi - 1] + 1, j)) + bi += 1 + elif bi > 0: pred[j].add(barrier_ops[bi - 1]) + self.pred = pred + self.succ = [[] for _ in range(n)] + for j in range(n): + for k in pred[j]: self.succ[k].append(j) + # chains and level sets + self.chain = []; self.frame_of = {} + for f in range(nf): + if f in pinned: + keys = [('v', i) for i in range(len(chain0[f]))] + for i, fr in enumerate(chain0[f]): self.frame_of[(f, ('v', i))] = fr + else: + keys = [] + for fr in chain0[f]: + if fr not in keys: keys.append(fr) + self.frame_of[(f, fr)] = fr + self.chain.append(keys) + self.cset = [set(ch) for ch in self.chain] + self.at = collections.defaultdict(set) + for k, e in enumerate(contacts): self.at[(e['d'], e['kd'])].add(k); self.at[(e['s'], e['ks'])].add(k) + + # frames --------------------------------------------------------------------------------- + @staticmethod + def span_of(vs): + s = {0} + for v in vs: s |= {x ^ v for x in s} + return frozenset(s) + def fid(self, sp): + if sp not in self.span_id: self.span_id[sp] = len(self.spans); self.spans.append(sp) + return self.span_id[sp] + def dim(self, i): return len(self.spans[i]).bit_length() - 1 + def sub(self, a, b): return self.spans[a] <= self.spans[b] + def join(self, a, b): return a if a == b else self.fid(self.span_of(list(self.spans[a] | self.spans[b]))) + def meet(self, a, b): return self.fid(self.spans[a] & self.spans[b]) + def fdim(self, f, key): return self.dim(self.frame_of[(f, key)]) + + # fragmentation ------------------------------------------------------------------------------ + def lam(self, t): + tot = 0.0 + for f in range(self.nf): + ds = [self.fdim(f, k) for k in self.chain[f]] + tot += sum(pw(ds[i + 1] - ds[i], t) for i in range(len(ds) - 1)) - pw(ds[-1] - ds[0], t) + return tot + def climb_profile(self): + prof = collections.Counter() + for f in range(self.nf): + ds = [self.fdim(f, k) for k in self.chain[f]] + for i in range(len(ds) - 1): + if ds[i + 1] > ds[i]: prof[ds[i + 1] - ds[i]] += 1 + return prof + + +def pw(x, t): return 0.0 if x <= 0 else math.exp(t * math.log(x)) + + +# ---------------------------------------------------------------------------------------------- +# dynamic graph with a Pearce-Kelly topological order +# ---------------------------------------------------------------------------------------------- +class DynGraph: + def __init__(self): + self.out = []; self.inn = []; self.ord = [] + def node(self, ord_): + # a strict total order: ties between level nodes that share an operation are broken by the node id + self.out.append(set()); self.inn.append(set()); self.ord.append((ord_, len(self.out) - 1)); return len(self.out) - 1 + def add_edge(self, u, v): + """False (graph unchanged) if the edge would close a cycle.""" + if v in self.out[u]: return True + ord_ = self.ord + if ord_[u] < ord_[v]: self.out[u].add(v); self.inn[v].add(u); return True + lb, ub = ord_[v], ord_[u] + Rf = []; seen = {v}; st = [v] + while st: + x = st.pop(); Rf.append(x) + for y in self.out[x]: + if y == u: return False + if y not in seen and ord_[y] <= ub: seen.add(y); st.append(y) + Rb = []; seenb = {u}; st = [u] + while st: + x = st.pop(); Rb.append(x) + for y in self.inn[x]: + if y not in seenb and ord_[y] >= lb: seenb.add(y); st.append(y) + Rb.sort(key=lambda x: ord_[x]); Rf.sort(key=lambda x: ord_[x]) + pos = sorted(ord_[x] for x in Rb + Rf) + for x, p in zip(Rb + Rf, pos): ord_[x] = p + self.out[u].add(v); self.inn[v].add(u); return True + def del_edge(self, u, v): self.out[u].discard(v); self.inn[v].discard(u) + + +class LevelGraph: + """ops + level nodes; built in the word's own order (no reordering needed), then edited transactionally.""" + def __init__(self, w): + self.w = w; n = w.n; G = DynGraph(); self.G = G + for j in range(n): G.node(2 * j) + for j in range(n): + for k in w.pred[j]: require(G.add_edge(k, j), 'dependency DAG is acyclic') + self.lv = {} + for f in range(w.nf): + for key in w.chain[f]: + ks = w.at.get((f, key)) + if not ks: continue + idx = [w.contacts[k]['op'] for k in ks] + ent = G.node(2 * min(idx) - 1); ex = G.node(2 * max(idx) + 1); self.lv[(f, key)] = (ent, ex) + self.edges = set() + for f in range(w.nf): self.edges |= self.level_edges(f) + for u, v in sorted(self.edges): require(G.add_edge(u, v), 'initial level graph is acyclic') + + def level_edges(self, f): + w = self.w; E = set(); lv = self.lv + act = [k for k in w.chain[f] if (f, k) in lv and w.at.get((f, k))] # empty levels are pass-through + for key in act: + ent, ex = lv[(f, key)] + for k in w.at[(f, key)]: + o = w.contacts[k]['op']; E.add((ent, o)); E.add((o, ex)) + for a, b in zip(act, act[1:]): E.add((lv[(f, a)][1], lv[(f, b)][0])) + for (j, g, va, A, B) in w.warp_ops: + if g != f: continue + ch = w.chain[f] + if f in w.pinned: + for key in ch: + if (f, key) not in lv: continue + if key[1] <= va: E.add((lv[(f, key)][1], j)) + else: E.add((j, lv[(f, key)][0])) + else: + pa, pb = ch.index(A), ch.index(B) + for i, key in enumerate(ch): + if (f, key) not in lv: continue + if i <= pa: E.add((lv[(f, key)][1], j)) + elif i >= pb: E.add((j, lv[(f, key)][0])) + return E + + def try_state(self, touched): + """apply the level structure of the touched fields (current chains/at); True iff acyclic; always rolls back.""" + w, G, lv = self.w, self.G, self.lv + created = [] + for f in touched: + for key in w.chain[f]: + if w.at.get((f, key)) and (f, key) not in lv: + idx = [w.contacts[k]['op'] for k in w.at[(f, key)]] + ent = G.node(2 * min(idx) - 1); ex = G.node(2 * max(idx) + 1); lv[(f, key)] = (ent, ex); created.append((f, key)) + old = set(); new = set() + for f in touched: + old |= self.field_edges[f] + new |= self.level_edges(f) + for u, v in old - new: G.del_edge(u, v) + added = []; ok = True + for u, v in sorted(new - old): + if not G.add_edge(u, v): ok = False; break + added.append((u, v)) + for u, v in added: G.del_edge(u, v) + for u, v in old - new: require(G.add_edge(u, v), 'rollback of a previously acyclic edge') + for fk in created: lv.pop(fk) + return ok + + def index_owners(self): + self.field_edges = [self.level_edges(f) for f in range(self.w.nf)] + + +# ---------------------------------------------------------------------------------------------- +# exhaustive single-level drop test +# ---------------------------------------------------------------------------------------------- +def options_for(w, k, f, F): + """frames of f's chain (other than F) where contact k could happen; each option is (X, partner_insert).""" + e = w.contacts[k] + if e['pin'] and e['kind'] != 'Cread': return [] + opts = [X for X in w.chain[f] if X != F and w.sub(e['lo'], X) and w.sub(X, e['hi'])] + if e['kind'] == 'Cread': return [(X, None) for X in opts if w.dim(X) >= 1] + g = e['s'] if e['d'] == f else e['d'] + out = [] + for X in opts: + if X in w.cset[g]: out.append((X, None)) + elif g not in w.pinned and all(w.sub(x, X) or w.sub(X, x) for x in w.chain[g]) and w.sub(w.S[g], X) and w.sub(X, w.T[g]): + out.append((X, g)) + return out + + +def drop_test(w, LG, cap=100000, t=1 - 0.0030217759): + """for every droppable level enumerate all re-routings; returns counters and the list of feasible drops with + their exact bill change (field climbs + partner insertions + centre transport ranks) at exponent t.""" + res = collections.Counter(); feasible = []; capped = [] + def lam_f(f): + ds = [w.fdim(f, k) for k in w.chain[f]] + return sum(pw(ds[i + 1] - ds[i], t) for i in range(len(ds) - 1)) - pw(ds[-1] - ds[0], t) + def centre(): return sum(pw(w.dim(w.contacts[k]['F']), t) for k in range(len(w.contacts)) if w.contacts[k]['kind'] == 'Cread') + for f in range(w.nf): + if f in w.pinned: continue + for F in list(w.chain[f]): + if F in (w.S[f], w.T[f]) or F in w.warp_frames[f]: continue + ks = sorted(w.at.get((f, F), [])) + if not ks: res['empty_level'] += 1; continue + res['levels'] += 1 + if res['levels'] % 500 == 0: print(f' ... {res["levels"]} levels enumerated', flush=True) + opts = [options_for(w, k, f, F) for k in ks] + if any(not o for o in opts): res['no_plan'] += 1; continue + # necessary condition: if op a must precede op b (value dependency), the frame of a along f cannot lie + # above the frame of b (frames of one field never decrease in time) + kops = {w.contacts[k]['op']: i for i, k in enumerate(ks)} + before_pairs = [] + for i, k in enumerate(ks): + src = w.contacts[k]['op']; seen = {src}; st = [src] + while st: + u = st.pop() + for v in w.succ[u]: + if v not in seen: + seen.add(v); st.append(v) + if v in kops: before_pairs.append((i, kops[v])) + posf = {X: p for p, X in enumerate(w.chain[f])} + def consistent(combo): + return all(posf[combo[a][0]] <= posf[combo[b][0]] for a, b in before_pairs) + total = 1 + for o in opts: total *= len(o) + combos = (c for c in itertools.product(*opts) if consistent(c)) + if total > cap: capped.append((f, F, total)); res['pruned_levels'] += 1 + res['plans'] += total + found = None + for combo in itertools.islice(combos, cap): + partners = {g for (X, g) in combo if g is not None} + before = lam_f(f) + sum(lam_f(g) for g in partners) + centre() + # apply: insert partner frames, move contacts, remove level + inserted = []; moved = [] + for k, (X, g) in zip(ks, combo): + e = w.contacts[k] + if g is not None and X not in w.cset[g]: + pos = len(w.chain[g]) + for i, x in enumerate(w.chain[g]): + if w.dim(x) > w.dim(X): pos = i; break + w.chain[g].insert(pos, X); w.cset[g].add(X); w.frame_of[(g, X)] = X; inserted.append((g, X)) + w.at[(e['d'], e['kd'])].discard(k); w.at[(e['s'], e['ks'])].discard(k) + moved.append((k, e['F'], e['kd'], e['ks'])) + e['F'] = X; e['kd'] = X; e['ks'] = X; w.at[(e['d'], X)].add(k); w.at[(e['s'], X)].add(k) + posF = w.chain[f].index(F); w.chain[f].remove(F); w.cset[f].discard(F) + touched = {f} | {e['d'] for k in ks for e in [w.contacts[k]]} | {e['s'] for k in ks for e in [w.contacts[k]]} + ok = LG.try_state(touched) + after = lam_f(f) + sum(lam_f(g) for g in partners) + centre() + # rollback state + w.chain[f].insert(posF, F); w.cset[f].add(F) + for k, F0, kd, ks_ in moved: + e = w.contacts[k]; w.at[(e['d'], e['kd'])].discard(k); w.at[(e['s'], e['ks'])].discard(k) + e['F'], e['kd'], e['ks'] = F0, kd, ks_; w.at[(e['d'], kd)].add(k); w.at[(e['s'], ks_)].add(k) + for g, X in inserted: w.chain[g].remove(X); w.cset[g].discard(X); w.frame_of.pop((g, X), None) + if ok and (found is None or after - before < found): found = after - before + if found is not None: + res['feasible'] += 1; feasible.append((f, F, round(found, 6))) + if found < -1e-9: res['improving'] += 1 + else: res['cycle'] += 1 + return res, feasible, capped + + +# ---------------------------------------------------------------------------------------------- +# kap-family ceilings (what Lambda would buy) +# ---------------------------------------------------------------------------------------------- +def kap_ceiling(H, Nloc, ports=112, block=8, pmax=40): + def momD(P, t): return sum(D(n) * (D(0) if r == 0 else (t * D(r).ln()).exp()) for r, n in P.items()) + def mom(P, t): return sum(n * pw(r, t) for r, n in P.items()) + def inv(p, a): + T = collections.Counter({r: (p + 2) * n for r, n in H.items()}); P = collections.Counter({r: (p + 2) * n for r, n in Nloc.items()}) + P[1] += ports * (p - 1); T[1 + block * (p + 2)] += 2 * ports + for L in (a, p - 1 - a): + for j in range(1, L + 1): T[1 + block * (j + 1)] += 2 * ports; P[block * (j + 1)] += 2 * ports + return T, P + def root(T, P, exact): + lo, hi = (D('1e-7'), D('0.2')) if exact else (1e-7, 0.2) + f = (lambda c: momD(T, 1 - c) - momD(P, 1 - c)) if exact else (lambda c: mom(T, 1 - c) - mom(P, 1 - c)) + if f(lo) <= 0: return lo * 0 + if f(hi) > 0: return hi + for _ in range(100 if exact else 50): + m = (lo + hi) / 2 + if f(m) > 0: lo = m + else: hi = m + return lo + best = max((root(*inv(p, a), False), p, a) for p in range(2, pmax + 1) for a in range(0, (p - 1) // 2 + 1)) + T, P = inv(best[1], best[2]) + return root(T, P, True), best[1], best[2], root(*inv(16, 7), True) + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('--write', action='store_true'); args = ap.parse_args() + t_start = time.time(); pinned_inputs() + word = json.loads(gzip.decompress((W3 / 'ACTUAL-WORD.json.gz').read_bytes())) + arith = json.loads((W3 / 'ARITHMETIC.json').read_text(encoding='utf-8')) + t0 = 1 - 0.0030217759 + w = Word(word, arith) + out = {} + # [1] word census + prof = w.climb_profile(); prof_c = collections.Counter(prof); prof_c[8] += 8 + require(dict(prof_c) == w.N, 'climb profile + 8 centre jobs equals ARITHMETIC local_paid') + lam0 = w.lam(t0) + print(f'[1] word: {w.nf} fields ({w.nm} mains, {w.nf - w.nm} helpers), {len(w.prog)} events, {w.n} ops, ' + f'{sum(1 for e in w.contacts if e["kind"] == "LL")} two-field contacts, {sum(1 for e in w.contacts if e["kind"] != "LL")} centre contacts; ' + f'climb profile {dict(sorted(prof.items()))}; Lambda(t0) = {lam0:.4f}') + require(abs(lam0 - 23.8626369) < 2e-6, 'Lambda of the word at its own root (#5226: 23.8626)') + out['lambda_word'] = round(lam0, 7); out['climb_profile'] = {str(k): v for k, v in sorted(prof.items())} + dims = collections.Counter(w.dim(e['F']) for e in w.contacts if e['kind'] == 'LL') + out['contacts_by_dimension'] = {str(k): v for k, v in sorted(dims.items())} + levels_total = sum(1 for f in range(w.nf) for F in w.chain[f][1:-1] if w.at.get((f, F))) + # [2] dependency slack + n = w.n; asap = [0] * n + for j in range(n): asap[j] = 1 + max((asap[k] for k in w.pred[j]), default=-1) + out['dag'] = {'ops': n, 'edges': sum(len(p) for p in w.pred), 'critical_path': max(asap) + 1} + print(f'[2] dependency DAG: {n} ops, {out["dag"]["edges"]} edges, critical path {out["dag"]["critical_path"]} (order is loose)') + # [3] one-field-at-a-time relaxations + forced_end = forced_exact = 0; lv_cnt = 0 + chainset = [set(ch) for ch in w.chain] + for f in range(w.nf): + ch = w.chain[f] + for i in range(1, len(ch) - 1): + ks = [k for k in w.at.get((f, ch[i]), []) if w.contacts[k]['kind'] == 'LL'] + if not ks: continue + lv_cnt += 1 + fr = lambda key: w.frame_of[(f, key)] + nxt, prv = fr(ch[i + 1]), fr(ch[i - 1]) + def partner(k): e = w.contacts[k]; return e['s'] if e['d'] == f else e['d'] + if not all(w.sub(nxt, w.T[partner(k)]) or (w.sub(w.S[partner(k)], prv) and w.sub(prv, w.T[partner(k)])) for k in ks): forced_end += 1 + if not all(ch[i + 1] in chainset[partner(k)] or ch[i - 1] in chainset[partner(k)] for k in ks): forced_exact += 1 + out['levels_with_two_field_contacts'] = lv_cnt + out['forced_by_partner_endpoints'] = forced_end; out['forced_by_partner_chains'] = forced_exact + print(f'[3] levels with two-field contacts {lv_cnt}: forced by partner endpoints alone {forced_end}; forced by the partners\' exact chains {forced_exact}') + # [4] exhaustive drop test, exact rules + t1 = time.time(); LG = LevelGraph(w); LG.index_owners() + res, feasible, capped = drop_test(w, LG) + print(f'[4] exact rules: levels {res["levels"]}, re-routings enumerated {res["plans"]}, no re-routing {res["no_plan"]}, ' + f'all re-routings cyclic {res["cycle"]}, feasible drops {res["feasible"]} (bill-improving {res["improving"]}), capped levels {len(capped)} ({time.time() - t1:.0f}s)') + for f, F, delta in feasible: print(f' feasible drop: field {f} ({"main" if f < w.nm else "helper"}) frame {F} dim {w.dim(F)}: best bill change {delta:+.4f} (the centre read moves to the full frame)') + require(res['improving'] == 0, 'no level of the #4610 word can be dropped at a gain under the exact rules') + require(not capped or all(any(w.contacts[k]['kind'] == 'Cread' for k in w.at[(f, F)]) for f, F, _ in capped), 'only centre-read levels exceed the enumeration cap (their consistent re-routings are all enumerated)') + require(all(any(w.contacts[k]['kind'] == 'Cread' for k in w.at[(f, F)]) for f, F, _ in feasible), 'every feasible drop is a centre-read level') + out['exact'] = dict(res); out['exact']['feasible_drops'] = feasible + # [5] control: centre contacts ignored -> drops appear (the test is live) + t1 = time.time(); w2 = Word(word, arith, pin_centre=False); LG2 = LevelGraph(w2); LG2.index_owners() + res2, feas2, capped2 = drop_test(w2, LG2) + print(f'[5] control, centre contacts ignored: feasible drops {res2["feasible"]} (improving {res2["improving"]}) of {res2["levels"]} levels (no re-routing {res2["no_plan"]}, cyclic {res2["cycle"]}, capped {len(capped2)}) ({time.time() - t1:.0f}s)') + require(res2['improving'] >= 5, 'the drop test finds improving drops when the centre interface is ignored') + out['control_no_centre'] = dict(res2); out['control_no_centre']['first_drops'] = feas2[:10] + # [6] what Lambda would buy: kap-family ceilings + H = w.H; Nc = collections.Counter(w.N) + mains = collections.Counter(); helps = collections.Counter(); cur = list(w.S); jobs = collections.defaultdict(list) + for e in w.prog: + if e[0] == 'climb': jobs[e[2]].append(e[5]) + for f in range(w.nf): + for r in jobs[f]: (mains if f < w.nm else helps)[r] += 1 + centre = collections.Counter({8: 8}) + table = {} + for name, N_ in (('word', mains + helps + centre), ('mains_one_climb', collections.Counter({8: w.nm}) + helps + centre), + ('helpers_one_climb', mains + collections.Counter(H) + centre), ('lambda_zero', collections.Counter({8: w.nm}) + collections.Counter(H) + centre)): + k, p, a, k16 = kap_ceiling(H, N_) + table[name] = {'kappa_best': f'{k:.10f}', 'p': p, 'a': a, 'kappa_p16a7': f'{k16:.10f}'} + print(f'[6] {name:18s}: kappa {k:.10f} at p={p} a={a}; at p16 a7 {k16:.10f}') + require(D('0.0030217758') < D(table['word']['kappa_p16a7']) < D('0.0030217760'), 'kap formula reproduces kappa(#4610)') + require(D(table['lambda_zero']['kappa_best']) > D('0.0081'), 'Lambda = 0 ceiling of the kap family above 0.0081') + out['kap_family'] = table + # result file + path = HERE / 'RESULT.json' + if args.write: + path.write_text(json.dumps(out, indent=1, sort_keys=True) + '\n', encoding='utf-8'); print('wrote', path) + else: + stored = json.loads(path.read_text(encoding='utf-8')) + require(stored == json.loads(json.dumps(out, sort_keys=True)), 'stored RESULT.json equals the rebuilt result') + print(f'PASS_FRAGMENTATION_REORDER_RIGIDITY ({time.time() - t_start:.0f}s)') + + +if __name__ == '__main__': + main() From 7ec11ab2276ce43bad47a03da9e58a22054e2c19 Mon Sep 17 00:00:00 2001 From: Matarener Date: Sat, 24 Oct 2026 12:49:44 +0300 Subject: [PATCH 2/3] fragmentation-reorder-rigidity: retain the recorded search logs as text files Co-Authored-By: Claude Fable 5.1 --- .../search/README.md | 6 +- .../search/anneal_seed1.txt | 125 ++++++++++++++++++ .../search/anneal_seed2.txt | 125 ++++++++++++++++++ .../search/anneal_seed3.txt | 65 +++++++++ .../search/sweep_exact_rules.txt | 6 + .../search/sweep_no_centre_pins.txt | 7 + 6 files changed, 331 insertions(+), 3 deletions(-) create mode 100644 research/fragmentation-reorder-rigidity/search/anneal_seed1.txt create mode 100644 research/fragmentation-reorder-rigidity/search/anneal_seed2.txt create mode 100644 research/fragmentation-reorder-rigidity/search/anneal_seed3.txt create mode 100644 research/fragmentation-reorder-rigidity/search/sweep_exact_rules.txt create mode 100644 research/fragmentation-reorder-rigidity/search/sweep_no_centre_pins.txt diff --git a/research/fragmentation-reorder-rigidity/search/README.md b/research/fragmentation-reorder-rigidity/search/README.md index 48461aa73e..18eb0a3a41 100644 --- a/research/fragmentation-reorder-rigidity/search/README.md +++ b/research/fragmentation-reorder-rigidity/search/README.md @@ -10,9 +10,9 @@ They are retained as evidence; their hard-coded paths point at the author's loca | `jcr_search4.py` | simulated annealing over joint frame chains and contact frames with an incremental (Pearce–Kelly) acyclicity check, a systematic sweep phase, centre interface pinned | | `jcr_search5.py` (derived by `make_v5.py`) | the same with the eight centre reads free to move along their source chains | | `eval_state.py` | prices a saved state's climb profile with the kap-family controller formula | -| `sweep_exact_rules.log` | sweep under the exact rules: 0 of 2,754 levels dropped (no re-routing 330, every re-routing cyclic 2,196) | -| `sweep_no_centre_pins.log` | control sweep ignoring the centre interface: 24 levels dropped, Lambda 23.50 | -| `anneal_seed1.log`, `anneal_seed2.log`, `anneal_seed3.log` | three 6-hour / 3-hour annealing runs of `jcr_search5.py` (15.2 M, 14.7 M and 7.1 M moves; moves: drop level, re-route contact, move contact to a new frame): best Lambda 23.8626 = the word in all three; centre reads stayed at dimension 8 | +| `sweep_exact_rules.txt` | sweep under the exact rules: 0 of 2,754 levels dropped (no re-routing 330, every re-routing cyclic 2,196) | +| `sweep_no_centre_pins.txt` | control sweep ignoring the centre interface: 24 levels dropped, Lambda 23.50 | +| `anneal_seed1.txt`, `anneal_seed2.txt`, `anneal_seed3.txt` | three 6-hour / 3-hour annealing runs of `jcr_search5.py` (15.2 M, 14.7 M and 7.1 M moves; moves: drop level, re-route contact, move contact to a new frame): best Lambda 23.8626 = the word in all three; centre reads stayed at dimension 8 | Earlier annealing versions that ignored the centre interface reached Lambda 23.45 (a model artefact: those states move contacts across the moments when a field must stand in the frame of a centre read or delivery, so diff --git a/research/fragmentation-reorder-rigidity/search/anneal_seed1.txt b/research/fragmentation-reorder-rigidity/search/anneal_seed1.txt new file mode 100644 index 0000000000..5368b8ab77 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/anneal_seed1.txt @@ -0,0 +1,125 @@ +01:44:53 JCR v4: fields 632 (pinned 12), contacts 16273, ops 18159, dag edges 204174, frames 4615 +01:46:54 initial Lambda = 23.8626; dynamic graph built, nodes 26171 +01:46:59 sweep 1: 0 levels dropped, Lambda 23.8626; failed: no plan 322, cost 2, cycle 2202 +01:46:59 annealing until 360.0 min, seed 1 +01:49:59 it 141222 acc 51 cyc-rejected 84021 T 0.0037 cur 23.8887 best 23.8626 +01:52:59 it 287799 acc 97 cyc-rejected 171546 T 0.0020 cur 23.8935 best 23.8626 +01:55:59 it 434324 acc 135 cyc-rejected 258590 T 0.0020 cur 23.8935 best 23.8626 +01:58:59 it 579236 acc 174 cyc-rejected 344810 T 0.0020 cur 23.9008 best 23.8626 +02:01:59 it 723526 acc 204 cyc-rejected 430726 T 0.0020 cur 23.9039 best 23.8626 +02:04:59 it 868396 acc 235 cyc-rejected 516795 T 0.0020 cur 23.9065 best 23.8626 +02:07:59 it 1012081 acc 266 cyc-rejected 602634 T 0.0020 cur 23.9065 best 23.8626 +02:10:59 it 1157108 acc 304 cyc-rejected 689159 T 0.0020 cur 23.9170 best 23.8626 +02:13:59 it 1300490 acc 333 cyc-rejected 774392 T 0.0020 cur 23.9186 best 23.8626 +02:16:59 it 1445405 acc 362 cyc-rejected 860644 T 0.0020 cur 23.9186 best 23.8626 +02:19:59 it 1590568 acc 411 cyc-rejected 946936 T 0.0020 cur 23.9233 best 23.8626 +02:22:59 it 1735454 acc 454 cyc-rejected 1033213 T 0.0020 cur 23.9281 best 23.8626 +02:25:59 it 1878538 acc 497 cyc-rejected 1118039 T 0.0020 cur 23.9281 best 23.8626 +02:28:59 it 2023421 acc 544 cyc-rejected 1204548 T 0.0020 cur 23.9307 best 23.8626 +02:31:59 it 2167679 acc 590 cyc-rejected 1290467 T 0.0020 cur 23.9307 best 23.8626 +02:34:59 it 2310565 acc 642 cyc-rejected 1375515 T 0.0020 cur 23.9249 best 23.8626 +02:37:59 it 2456119 acc 674 cyc-rejected 1461853 T 0.0020 cur 23.9296 best 23.8626 +02:40:59 it 2600614 acc 707 cyc-rejected 1547839 T 0.0020 cur 23.9344 best 23.8626 +02:43:59 it 2747426 acc 742 cyc-rejected 1635325 T 0.0020 cur 23.9344 best 23.8626 +02:46:59 it 2893950 acc 795 cyc-rejected 1722900 T 0.0020 cur 23.9292 best 23.8626 +02:49:59 it 3038743 acc 835 cyc-rejected 1808872 T 0.0020 cur 23.9344 best 23.8626 +02:52:59 it 3182810 acc 868 cyc-rejected 1894348 T 0.0020 cur 23.9296 best 23.8626 +02:55:59 it 3326228 acc 906 cyc-rejected 1979962 T 0.0020 cur 23.9296 best 23.8626 +02:58:59 it 3471482 acc 948 cyc-rejected 2066163 T 0.0020 cur 23.9296 best 23.8626 +03:02:00 it 3614117 acc 991 cyc-rejected 2151243 T 0.0020 cur 23.9296 best 23.8626 +03:05:00 it 3759800 acc 1032 cyc-rejected 2237785 T 0.0020 cur 23.9296 best 23.8626 +03:08:00 it 3905550 acc 1084 cyc-rejected 2324481 T 0.0020 cur 23.9296 best 23.8626 +03:11:00 it 4052337 acc 1133 cyc-rejected 2411966 T 0.0020 cur 23.9344 best 23.8626 +03:14:00 it 4197301 acc 1170 cyc-rejected 2497994 T 0.0020 cur 23.9344 best 23.8626 +03:17:00 it 4342347 acc 1213 cyc-rejected 2584279 T 0.0020 cur 23.9439 best 23.8626 +03:20:00 it 4485269 acc 1254 cyc-rejected 2669245 T 0.0020 cur 23.9439 best 23.8626 +03:23:00 it 4630235 acc 1297 cyc-rejected 2755424 T 0.0020 cur 23.9480 best 23.8626 +03:26:00 it 4775051 acc 1353 cyc-rejected 2841723 T 0.0020 cur 23.9528 best 23.8626 +03:29:00 it 4919226 acc 1421 cyc-rejected 2927189 T 0.0020 cur 23.9528 best 23.8626 +03:32:00 it 5062603 acc 1475 cyc-rejected 3012807 T 0.0020 cur 23.9528 best 23.8626 +03:35:00 it 5206877 acc 1519 cyc-rejected 3098382 T 0.0020 cur 23.9528 best 23.8626 +03:38:00 it 5350953 acc 1566 cyc-rejected 3183972 T 0.0020 cur 23.9528 best 23.8626 +03:41:00 it 5496943 acc 1605 cyc-rejected 3270909 T 0.0020 cur 23.9480 best 23.8626 +03:44:00 it 5640412 acc 1653 cyc-rejected 3356652 T 0.0020 cur 23.9512 best 23.8626 +03:47:00 it 5784904 acc 1693 cyc-rejected 3442674 T 0.0020 cur 23.9580 best 23.8626 +03:50:00 it 5929418 acc 1739 cyc-rejected 3528730 T 0.0020 cur 23.9658 best 23.8626 +03:53:00 it 6072621 acc 1784 cyc-rejected 3613902 T 0.0020 cur 23.9658 best 23.8626 +03:56:00 it 6214955 acc 1829 cyc-rejected 3698712 T 0.0020 cur 23.9658 best 23.8626 +03:59:00 it 6358789 acc 1879 cyc-rejected 3784451 T 0.0020 cur 23.9627 best 23.8626 +04:02:00 it 6504085 acc 1921 cyc-rejected 3870847 T 0.0020 cur 23.9695 best 23.8626 +04:05:00 it 6647954 acc 1965 cyc-rejected 3956548 T 0.0020 cur 23.9653 best 23.8626 +04:08:00 it 6790296 acc 1997 cyc-rejected 4041130 T 0.0020 cur 23.9637 best 23.8626 +04:11:00 it 6915757 acc 2041 cyc-rejected 4115900 T 0.0020 cur 23.9637 best 23.8626 +04:14:00 it 7042169 acc 2079 cyc-rejected 4190942 T 0.0020 cur 23.9669 best 23.8626 +04:17:00 it 7176189 acc 2119 cyc-rejected 4270894 T 0.0020 cur 23.9669 best 23.8626 +04:20:00 it 7300782 acc 2164 cyc-rejected 4344968 T 0.0020 cur 23.9716 best 23.8626 +04:23:00 it 7439174 acc 2203 cyc-rejected 4427394 T 0.0020 cur 23.9716 best 23.8626 +04:26:00 it 7583114 acc 2255 cyc-rejected 4513227 T 0.0020 cur 23.9716 best 23.8626 +04:29:00 it 7725687 acc 2306 cyc-rejected 4597982 T 0.0020 cur 23.9857 best 23.8626 +04:32:00 it 7868345 acc 2354 cyc-rejected 4682993 T 0.0020 cur 23.9784 best 23.8626 +04:35:00 it 8012885 acc 2386 cyc-rejected 4768832 T 0.0020 cur 23.9784 best 23.8626 +04:38:00 it 8156113 acc 2426 cyc-rejected 4854272 T 0.0020 cur 23.9784 best 23.8626 +04:41:00 it 8298359 acc 2479 cyc-rejected 4938949 T 0.0020 cur 23.9717 best 23.8626 +04:44:00 it 8439500 acc 2523 cyc-rejected 5022813 T 0.0020 cur 23.9717 best 23.8626 +04:47:00 it 8582944 acc 2556 cyc-rejected 5108480 T 0.0020 cur 23.9743 best 23.8626 +04:50:00 it 8726279 acc 2602 cyc-rejected 5193955 T 0.0020 cur 23.9790 best 23.8626 +04:53:00 it 8860425 acc 2643 cyc-rejected 5273813 T 0.0020 cur 23.9790 best 23.8626 +04:56:00 it 8996891 acc 2682 cyc-rejected 5355042 T 0.0020 cur 23.9838 best 23.8626 +04:59:00 it 9128595 acc 2723 cyc-rejected 5433448 T 0.0020 cur 23.9838 best 23.8626 +05:02:00 it 9258880 acc 2769 cyc-rejected 5510966 T 0.0020 cur 23.9838 best 23.8626 +05:05:00 it 9392827 acc 2810 cyc-rejected 5590459 T 0.0020 cur 23.9838 best 23.8626 +05:08:00 it 9528814 acc 2864 cyc-rejected 5671290 T 0.0020 cur 23.9754 best 23.8626 +05:11:00 it 9660478 acc 2902 cyc-rejected 5749986 T 0.0020 cur 23.9754 best 23.8626 +05:14:00 it 9787154 acc 2944 cyc-rejected 5825177 T 0.0020 cur 23.9728 best 23.8626 +05:17:00 it 9920496 acc 2993 cyc-rejected 5904622 T 0.0020 cur 23.9776 best 23.8626 +05:20:00 it 10052440 acc 3042 cyc-rejected 5983283 T 0.0020 cur 23.9776 best 23.8626 +05:23:00 it 10181462 acc 3087 cyc-rejected 6060317 T 0.0020 cur 23.9754 best 23.8626 +05:26:00 it 10312730 acc 3128 cyc-rejected 6138575 T 0.0020 cur 23.9754 best 23.8626 +05:29:00 it 10445668 acc 3176 cyc-rejected 6217644 T 0.0020 cur 23.9754 best 23.8626 +05:32:00 it 10578368 acc 3211 cyc-rejected 6296602 T 0.0020 cur 23.9754 best 23.8626 +05:35:00 it 10708235 acc 3242 cyc-rejected 6373793 T 0.0020 cur 23.9838 best 23.8626 +05:38:00 it 10841806 acc 3282 cyc-rejected 6453278 T 0.0020 cur 23.9838 best 23.8626 +05:41:00 it 10972463 acc 3323 cyc-rejected 6530959 T 0.0020 cur 23.9885 best 23.8626 +05:44:00 it 11105466 acc 3376 cyc-rejected 6609715 T 0.0020 cur 23.9985 best 23.8626 +05:47:00 it 11240514 acc 3412 cyc-rejected 6689816 T 0.0020 cur 24.0032 best 23.8626 +05:50:00 it 11376945 acc 3441 cyc-rejected 6770823 T 0.0020 cur 24.0032 best 23.8626 +05:53:00 it 11510136 acc 3476 cyc-rejected 6850001 T 0.0020 cur 24.0032 best 23.8626 +05:56:00 it 11638705 acc 3513 cyc-rejected 6926472 T 0.0020 cur 23.9985 best 23.8626 +05:59:00 it 11771464 acc 3552 cyc-rejected 7005490 T 0.0020 cur 23.9985 best 23.8626 +06:02:00 it 11904669 acc 3589 cyc-rejected 7084773 T 0.0020 cur 23.9985 best 23.8626 +06:05:00 it 12037857 acc 3637 cyc-rejected 7164078 T 0.0020 cur 23.9959 best 23.8626 +06:08:00 it 12171278 acc 3680 cyc-rejected 7243413 T 0.0020 cur 24.0100 best 23.8626 +06:11:00 it 12303809 acc 3731 cyc-rejected 7322435 T 0.0020 cur 24.0126 best 23.8626 +06:14:00 it 12436548 acc 3778 cyc-rejected 7401297 T 0.0020 cur 24.0126 best 23.8626 +06:17:00 it 12560784 acc 3811 cyc-rejected 7475164 T 0.0020 cur 24.0078 best 23.8626 +06:20:00 it 12690366 acc 3853 cyc-rejected 7552054 T 0.0020 cur 24.0031 best 23.8626 +06:23:00 it 12820555 acc 3887 cyc-rejected 7629539 T 0.0020 cur 24.0031 best 23.8626 +06:26:00 it 12953874 acc 3916 cyc-rejected 7708800 T 0.0020 cur 23.9979 best 23.8626 +06:29:00 it 13088197 acc 3942 cyc-rejected 7788819 T 0.0020 cur 23.9979 best 23.8626 +06:32:00 it 13223988 acc 3984 cyc-rejected 7869475 T 0.0020 cur 23.9979 best 23.8626 +06:35:00 it 13357307 acc 4014 cyc-rejected 7949155 T 0.0020 cur 23.9979 best 23.8626 +06:38:00 it 13486500 acc 4046 cyc-rejected 8025703 T 0.0020 cur 23.9953 best 23.8626 +06:41:00 it 13617036 acc 4074 cyc-rejected 8103440 T 0.0020 cur 23.9906 best 23.8626 +06:44:00 it 13749102 acc 4103 cyc-rejected 8182034 T 0.0020 cur 23.9906 best 23.8626 +06:47:00 it 13879638 acc 4149 cyc-rejected 8259666 T 0.0020 cur 23.9953 best 23.8626 +06:50:00 it 14011944 acc 4179 cyc-rejected 8338369 T 0.0020 cur 24.0000 best 23.8626 +06:53:00 it 14139725 acc 4215 cyc-rejected 8414415 T 0.0020 cur 24.0048 best 23.8626 +06:56:00 it 14272359 acc 4248 cyc-rejected 8493172 T 0.0020 cur 24.0048 best 23.8626 +06:59:00 it 14402533 acc 4284 cyc-rejected 8570328 T 0.0020 cur 24.0079 best 23.8626 +07:02:00 it 14535955 acc 4327 cyc-rejected 8649400 T 0.0020 cur 23.9990 best 23.8626 +07:05:00 it 14666944 acc 4362 cyc-rejected 8727341 T 0.0020 cur 24.0021 best 23.8626 +07:08:00 it 14801567 acc 4406 cyc-rejected 8807046 T 0.0020 cur 24.0047 best 23.8626 +07:11:00 it 14933038 acc 4437 cyc-rejected 8885302 T 0.0020 cur 24.0047 best 23.8626 +07:14:00 it 15065100 acc 4482 cyc-rejected 8963832 T 0.0020 cur 24.0142 best 23.8626 +07:17:00 it 15198233 acc 4518 cyc-rejected 9043032 T 0.0020 cur 24.0158 best 23.8626 +07:20:00 it 15328249 acc 4562 cyc-rejected 9120444 T 0.0020 cur 24.0205 best 23.8626 +07:23:00 it 15461762 acc 4605 cyc-rejected 9199936 T 0.0020 cur 24.0205 best 23.8626 +07:26:00 it 15593211 acc 4650 cyc-rejected 9277801 T 0.0020 cur 24.0106 best 23.8626 +07:29:00 it 15728734 acc 4690 cyc-rejected 9358276 T 0.0020 cur 24.0090 best 23.8626 +07:32:00 it 15862650 acc 4729 cyc-rejected 9437874 T 0.0020 cur 24.0138 best 23.8626 +07:35:01 it 15992286 acc 4772 cyc-rejected 9515044 T 0.0020 cur 24.0169 best 23.8626 +07:38:01 it 16126390 acc 4825 cyc-rejected 9595088 T 0.0020 cur 24.0169 best 23.8626 +07:41:01 it 16260569 acc 4861 cyc-rejected 9674854 T 0.0020 cur 24.0253 best 23.8626 +07:44:01 it 16393803 acc 4901 cyc-rejected 9754228 T 0.0020 cur 24.0253 best 23.8626 +07:46:54 FINAL best Lambda+centre = 23.8626 (word 23.8626); climbs/field hist {3: 72, 4: 128, 5: 225, 6: 63, 7: 77, 8: 61, 9: 6}; profile incl. centre {1: 2203, 2: 475, 3: 465, 4: 130, 5: 39, 8: 8}; centre read dims [8, 8, 8, 8, 8, 8, 8, 8] +07:46:54 done jcr_search4 diff --git a/research/fragmentation-reorder-rigidity/search/anneal_seed2.txt b/research/fragmentation-reorder-rigidity/search/anneal_seed2.txt new file mode 100644 index 0000000000..f84f63d9b8 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/anneal_seed2.txt @@ -0,0 +1,125 @@ +01:44:53 JCR v4: fields 632 (pinned 12), contacts 16273, ops 18159, dag edges 204174, frames 4615 +01:46:54 initial Lambda = 23.8626; dynamic graph built, nodes 26171 +01:46:59 sweep 1: 0 levels dropped, Lambda 23.8626; failed: no plan 322, cost 2, cycle 2202 +01:47:00 annealing until 360.0 min, seed 2 +01:50:00 it 133657 acc 39 cyc-rejected 79280 T 0.0041 cur 23.8674 best 23.8626 +01:53:00 it 272852 acc 83 cyc-rejected 161901 T 0.0020 cur 23.8700 best 23.8626 +01:56:00 it 411909 acc 131 cyc-rejected 244697 T 0.0020 cur 23.8700 best 23.8626 +01:59:00 it 549365 acc 176 cyc-rejected 326418 T 0.0020 cur 23.8726 best 23.8626 +02:02:00 it 688816 acc 216 cyc-rejected 409548 T 0.0020 cur 23.8778 best 23.8626 +02:05:00 it 828332 acc 255 cyc-rejected 492576 T 0.0020 cur 23.8778 best 23.8626 +02:08:00 it 968847 acc 291 cyc-rejected 576035 T 0.0020 cur 23.8872 best 23.8626 +02:11:00 it 1110598 acc 340 cyc-rejected 660157 T 0.0020 cur 23.8898 best 23.8626 +02:14:00 it 1251175 acc 390 cyc-rejected 743444 T 0.0020 cur 23.8898 best 23.8626 +02:17:00 it 1390996 acc 425 cyc-rejected 826619 T 0.0020 cur 23.8898 best 23.8626 +02:20:00 it 1531042 acc 466 cyc-rejected 909628 T 0.0020 cur 23.8930 best 23.8626 +02:23:00 it 1670598 acc 510 cyc-rejected 992649 T 0.0020 cur 23.8930 best 23.8626 +02:26:00 it 1809257 acc 549 cyc-rejected 1075060 T 0.0020 cur 23.8956 best 23.8626 +02:29:00 it 1950636 acc 587 cyc-rejected 1159124 T 0.0020 cur 23.8930 best 23.8626 +02:32:00 it 2090008 acc 635 cyc-rejected 1241840 T 0.0020 cur 23.8930 best 23.8626 +02:35:00 it 2231459 acc 666 cyc-rejected 1326094 T 0.0020 cur 23.8930 best 23.8626 +02:38:00 it 2370374 acc 716 cyc-rejected 1408892 T 0.0020 cur 23.8930 best 23.8626 +02:41:00 it 2510914 acc 756 cyc-rejected 1492478 T 0.0020 cur 23.8930 best 23.8626 +02:44:00 it 2649426 acc 797 cyc-rejected 1574842 T 0.0020 cur 23.8930 best 23.8626 +02:47:00 it 2789234 acc 836 cyc-rejected 1657918 T 0.0020 cur 23.8977 best 23.8626 +02:50:00 it 2930550 acc 887 cyc-rejected 1742073 T 0.0020 cur 23.9051 best 23.8626 +02:53:00 it 3072434 acc 923 cyc-rejected 1826332 T 0.0020 cur 23.9098 best 23.8626 +02:56:00 it 3211317 acc 963 cyc-rejected 1909146 T 0.0020 cur 23.9098 best 23.8626 +02:59:00 it 3351419 acc 1003 cyc-rejected 1992744 T 0.0020 cur 23.9114 best 23.8626 +03:02:00 it 3491175 acc 1048 cyc-rejected 2076053 T 0.0020 cur 23.9161 best 23.8626 +03:05:00 it 3630137 acc 1090 cyc-rejected 2158614 T 0.0020 cur 23.9208 best 23.8626 +03:08:00 it 3771451 acc 1141 cyc-rejected 2243038 T 0.0020 cur 23.9256 best 23.8626 +03:11:00 it 3914153 acc 1181 cyc-rejected 2327668 T 0.0020 cur 23.9256 best 23.8626 +03:14:00 it 4053509 acc 1219 cyc-rejected 2410893 T 0.0020 cur 23.9214 best 23.8626 +03:17:00 it 4194765 acc 1261 cyc-rejected 2494846 T 0.0020 cur 23.9214 best 23.8626 +03:20:00 it 4334262 acc 1299 cyc-rejected 2577882 T 0.0020 cur 23.9119 best 23.8626 +03:23:00 it 4475496 acc 1350 cyc-rejected 2661659 T 0.0020 cur 23.9072 best 23.8626 +03:26:00 it 4618098 acc 1400 cyc-rejected 2746379 T 0.0020 cur 23.9072 best 23.8626 +03:29:00 it 4761537 acc 1442 cyc-rejected 2831160 T 0.0020 cur 23.9072 best 23.8626 +03:32:00 it 4898990 acc 1482 cyc-rejected 2913038 T 0.0020 cur 23.9072 best 23.8626 +03:35:00 it 5040529 acc 1520 cyc-rejected 2997285 T 0.0020 cur 23.9072 best 23.8626 +03:38:00 it 5180182 acc 1560 cyc-rejected 3080701 T 0.0020 cur 23.9072 best 23.8626 +03:41:00 it 5318781 acc 1609 cyc-rejected 3163177 T 0.0020 cur 23.9072 best 23.8626 +03:44:00 it 5456266 acc 1651 cyc-rejected 3245023 T 0.0020 cur 23.9072 best 23.8626 +03:47:00 it 5595727 acc 1716 cyc-rejected 3328133 T 0.0020 cur 23.9046 best 23.8626 +03:50:00 it 5735206 acc 1773 cyc-rejected 3411313 T 0.0020 cur 23.9062 best 23.8626 +03:53:00 it 5874462 acc 1809 cyc-rejected 3494506 T 0.0020 cur 23.9151 best 23.8626 +03:56:00 it 6016469 acc 1850 cyc-rejected 3579121 T 0.0020 cur 23.9151 best 23.8626 +03:59:00 it 6157732 acc 1888 cyc-rejected 3662986 T 0.0020 cur 23.9198 best 23.8626 +04:02:00 it 6295887 acc 1927 cyc-rejected 3745227 T 0.0020 cur 23.9198 best 23.8626 +04:05:00 it 6437296 acc 1966 cyc-rejected 3829250 T 0.0020 cur 23.9198 best 23.8626 +04:08:00 it 6574869 acc 1999 cyc-rejected 3910989 T 0.0020 cur 23.9198 best 23.8626 +04:11:00 it 6696428 acc 2029 cyc-rejected 3983544 T 0.0020 cur 23.9246 best 23.8626 +04:14:00 it 6820248 acc 2071 cyc-rejected 4056985 T 0.0020 cur 23.9246 best 23.8626 +04:17:00 it 6950914 acc 2118 cyc-rejected 4134974 T 0.0020 cur 23.9246 best 23.8626 +04:20:00 it 7070906 acc 2160 cyc-rejected 4206464 T 0.0020 cur 23.9272 best 23.8626 +04:23:00 it 7206054 acc 2208 cyc-rejected 4286860 T 0.0020 cur 23.9439 best 23.8626 +04:26:00 it 7343133 acc 2249 cyc-rejected 4368435 T 0.0020 cur 23.9391 best 23.8626 +04:29:00 it 7479397 acc 2292 cyc-rejected 4449420 T 0.0020 cur 23.9423 best 23.8626 +04:32:00 it 7615578 acc 2335 cyc-rejected 4530931 T 0.0020 cur 23.9449 best 23.8626 +04:35:00 it 7754671 acc 2374 cyc-rejected 4613691 T 0.0020 cur 23.9449 best 23.8626 +04:38:00 it 7895145 acc 2413 cyc-rejected 4697191 T 0.0020 cur 23.9423 best 23.8626 +04:41:00 it 8031713 acc 2458 cyc-rejected 4778590 T 0.0020 cur 23.9470 best 23.8626 +04:44:00 it 8170129 acc 2497 cyc-rejected 4861261 T 0.0020 cur 23.9470 best 23.8626 +04:47:00 it 8308832 acc 2531 cyc-rejected 4943647 T 0.0020 cur 23.9470 best 23.8626 +04:50:00 it 8445656 acc 2570 cyc-rejected 5024933 T 0.0020 cur 23.9470 best 23.8626 +04:53:00 it 8572933 acc 2612 cyc-rejected 5100468 T 0.0020 cur 23.9439 best 23.8626 +04:56:00 it 8703490 acc 2658 cyc-rejected 5178378 T 0.0020 cur 23.9439 best 23.8626 +04:59:00 it 8833659 acc 2705 cyc-rejected 5255690 T 0.0020 cur 23.9439 best 23.8626 +05:02:00 it 8957908 acc 2736 cyc-rejected 5329549 T 0.0020 cur 23.9486 best 23.8626 +05:05:00 it 9087144 acc 2767 cyc-rejected 5406314 T 0.0020 cur 23.9439 best 23.8626 +05:08:00 it 9220681 acc 2789 cyc-rejected 5486012 T 0.0020 cur 23.9439 best 23.8626 +05:11:00 it 9349350 acc 2831 cyc-rejected 5562736 T 0.0020 cur 23.9470 best 23.8626 +05:14:00 it 9470980 acc 2869 cyc-rejected 5635379 T 0.0020 cur 23.9564 best 23.8626 +05:17:00 it 9598659 acc 2908 cyc-rejected 5711374 T 0.0020 cur 23.9564 best 23.8626 +05:20:00 it 9724081 acc 2937 cyc-rejected 5785726 T 0.0020 cur 23.9469 best 23.8626 +05:23:00 it 9852041 acc 2981 cyc-rejected 5861989 T 0.0020 cur 23.9516 best 23.8626 +05:26:00 it 9980780 acc 3015 cyc-rejected 5938660 T 0.0020 cur 23.9469 best 23.8626 +05:29:00 it 10111077 acc 3055 cyc-rejected 6016353 T 0.0020 cur 23.9463 best 23.8626 +05:32:00 it 10240456 acc 3092 cyc-rejected 6093435 T 0.0020 cur 23.9511 best 23.8626 +05:35:00 it 10366726 acc 3135 cyc-rejected 6168545 T 0.0020 cur 23.9463 best 23.8626 +05:38:00 it 10496122 acc 3181 cyc-rejected 6245788 T 0.0020 cur 23.9422 best 23.8626 +05:41:00 it 10623308 acc 3220 cyc-rejected 6321511 T 0.0020 cur 23.9422 best 23.8626 +05:44:00 it 10750325 acc 3260 cyc-rejected 6397246 T 0.0020 cur 23.9448 best 23.8626 +05:47:00 it 10879731 acc 3306 cyc-rejected 6474173 T 0.0020 cur 23.9479 best 23.8626 +05:50:00 it 11010257 acc 3340 cyc-rejected 6551646 T 0.0020 cur 23.9479 best 23.8626 +05:53:00 it 11138226 acc 3380 cyc-rejected 6627741 T 0.0020 cur 23.9510 best 23.8626 +05:56:00 it 11262810 acc 3414 cyc-rejected 6701760 T 0.0020 cur 23.9542 best 23.8626 +05:59:00 it 11394331 acc 3451 cyc-rejected 6780010 T 0.0020 cur 23.9542 best 23.8626 +06:02:00 it 11522476 acc 3481 cyc-rejected 6856179 T 0.0020 cur 23.9573 best 23.8626 +06:05:00 it 11649066 acc 3517 cyc-rejected 6931364 T 0.0020 cur 23.9573 best 23.8626 +06:08:00 it 11778640 acc 3551 cyc-rejected 7008599 T 0.0020 cur 23.9532 best 23.8626 +06:11:00 it 11906732 acc 3593 cyc-rejected 7084745 T 0.0020 cur 23.9480 best 23.8626 +06:14:00 it 12032644 acc 3643 cyc-rejected 7159705 T 0.0020 cur 23.9527 best 23.8626 +06:17:00 it 12151026 acc 3672 cyc-rejected 7230077 T 0.0020 cur 23.9527 best 23.8626 +06:20:00 it 12276375 acc 3719 cyc-rejected 7304709 T 0.0020 cur 23.9527 best 23.8626 +06:23:00 it 12401579 acc 3757 cyc-rejected 7379118 T 0.0020 cur 23.9527 best 23.8626 +06:26:00 it 12528410 acc 3796 cyc-rejected 7454473 T 0.0020 cur 23.9501 best 23.8626 +06:29:00 it 12657735 acc 3837 cyc-rejected 7531530 T 0.0020 cur 23.9501 best 23.8626 +06:32:00 it 12786593 acc 3882 cyc-rejected 7607956 T 0.0020 cur 23.9454 best 23.8626 +06:35:00 it 12915665 acc 3931 cyc-rejected 7684848 T 0.0020 cur 23.9454 best 23.8626 +06:38:00 it 13042856 acc 3966 cyc-rejected 7760626 T 0.0020 cur 23.9454 best 23.8626 +06:41:00 it 13172353 acc 3997 cyc-rejected 7837772 T 0.0020 cur 23.9501 best 23.8626 +06:44:00 it 13300622 acc 4038 cyc-rejected 7913884 T 0.0020 cur 23.9549 best 23.8626 +06:47:00 it 13428870 acc 4088 cyc-rejected 7990125 T 0.0020 cur 23.9549 best 23.8626 +06:50:00 it 13558506 acc 4128 cyc-rejected 8067208 T 0.0020 cur 23.9549 best 23.8626 +06:53:00 it 13686588 acc 4171 cyc-rejected 8143451 T 0.0020 cur 23.9549 best 23.8626 +06:56:00 it 13814881 acc 4210 cyc-rejected 8219831 T 0.0020 cur 23.9544 best 23.8626 +06:59:00 it 13940274 acc 4245 cyc-rejected 8294451 T 0.0020 cur 23.9544 best 23.8626 +07:02:00 it 14068364 acc 4282 cyc-rejected 8370652 T 0.0020 cur 23.9570 best 23.8626 +07:05:01 it 14196335 acc 4324 cyc-rejected 8446720 T 0.0020 cur 23.9638 best 23.8626 +07:08:01 it 14324824 acc 4366 cyc-rejected 8523032 T 0.0020 cur 23.9606 best 23.8626 +07:11:01 it 14452812 acc 4403 cyc-rejected 8599380 T 0.0020 cur 23.9653 best 23.8626 +07:14:01 it 14581437 acc 4443 cyc-rejected 8676076 T 0.0020 cur 23.9628 best 23.8626 +07:17:01 it 14709964 acc 4484 cyc-rejected 8752393 T 0.0020 cur 23.9628 best 23.8626 +07:20:01 it 14835023 acc 4524 cyc-rejected 8826637 T 0.0020 cur 23.9554 best 23.8626 +07:23:01 it 14966036 acc 4564 cyc-rejected 8904502 T 0.0020 cur 23.9649 best 23.8626 +07:26:01 it 15093126 acc 4602 cyc-rejected 8980033 T 0.0020 cur 23.9696 best 23.8626 +07:29:01 it 15224003 acc 4648 cyc-rejected 9057718 T 0.0020 cur 23.9649 best 23.8626 +07:32:01 it 15354224 acc 4695 cyc-rejected 9134825 T 0.0020 cur 23.9649 best 23.8626 +07:35:01 it 15484551 acc 4724 cyc-rejected 9212401 T 0.0020 cur 23.9649 best 23.8626 +07:38:01 it 15614711 acc 4769 cyc-rejected 9289733 T 0.0020 cur 23.9602 best 23.8626 +07:41:01 it 15742858 acc 4806 cyc-rejected 9365790 T 0.0020 cur 23.9602 best 23.8626 +07:44:01 it 15870942 acc 4846 cyc-rejected 9441825 T 0.0020 cur 23.9508 best 23.8626 +07:46:55 FINAL best Lambda+centre = 23.8626 (word 23.8626); climbs/field hist {3: 72, 4: 129, 5: 225, 6: 64, 7: 81, 8: 55, 9: 6}; profile incl. centre {1: 2197, 2: 462, 3: 470, 4: 133, 5: 40, 8: 8}; centre read dims [8, 8, 8, 8, 8, 8, 8, 8] +07:46:55 done jcr_search4 diff --git a/research/fragmentation-reorder-rigidity/search/anneal_seed3.txt b/research/fragmentation-reorder-rigidity/search/anneal_seed3.txt new file mode 100644 index 0000000000..c6219e8fb0 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/anneal_seed3.txt @@ -0,0 +1,65 @@ +04:50:56 JCR v4: fields 632 (pinned 12), contacts 16273, ops 18159, dag edges 204174, frames 4615 +04:52:48 initial Lambda = 23.8626; dynamic graph built, nodes 26171 +04:52:52 sweep 1: 0 levels dropped, Lambda 23.8626; failed: no plan 322, cost 0, cycle 2204 +04:52:53 annealing until 180.0 min, seed 3 +04:55:53 it 139177 acc 48 cyc-rejected 82833 T 0.0038 cur 23.8752 best 23.8626 +04:58:53 it 277244 acc 102 cyc-rejected 165102 T 0.0020 cur 23.8752 best 23.8626 +05:01:53 it 414272 acc 154 cyc-rejected 246847 T 0.0020 cur 23.8752 best 23.8626 +05:04:53 it 551473 acc 201 cyc-rejected 328618 T 0.0020 cur 23.8752 best 23.8626 +05:07:53 it 692798 acc 231 cyc-rejected 412942 T 0.0020 cur 23.8752 best 23.8626 +05:10:53 it 831342 acc 277 cyc-rejected 495364 T 0.0020 cur 23.8752 best 23.8626 +05:13:53 it 960485 acc 305 cyc-rejected 572086 T 0.0020 cur 23.8799 best 23.8626 +05:16:53 it 1099764 acc 348 cyc-rejected 655138 T 0.0020 cur 23.8799 best 23.8626 +05:19:53 it 1236192 acc 386 cyc-rejected 736303 T 0.0020 cur 23.8799 best 23.8626 +05:22:53 it 1373247 acc 434 cyc-rejected 818307 T 0.0020 cur 23.8799 best 23.8626 +05:25:53 it 1512026 acc 471 cyc-rejected 901077 T 0.0020 cur 23.8752 best 23.8626 +05:28:53 it 1652774 acc 515 cyc-rejected 984638 T 0.0020 cur 23.8752 best 23.8626 +05:31:53 it 1792769 acc 561 cyc-rejected 1068175 T 0.0020 cur 23.8799 best 23.8626 +05:34:53 it 1927147 acc 596 cyc-rejected 1148135 T 0.0020 cur 23.8799 best 23.8626 +05:37:53 it 2067173 acc 640 cyc-rejected 1231404 T 0.0020 cur 23.8799 best 23.8626 +05:40:53 it 2206679 acc 689 cyc-rejected 1314414 T 0.0020 cur 23.8856 best 23.8626 +05:43:53 it 2346691 acc 730 cyc-rejected 1397868 T 0.0020 cur 23.8856 best 23.8626 +05:46:53 it 2487330 acc 770 cyc-rejected 1481363 T 0.0020 cur 23.8856 best 23.8626 +05:49:53 it 2628882 acc 820 cyc-rejected 1565440 T 0.0020 cur 23.8856 best 23.8626 +05:52:53 it 2766217 acc 858 cyc-rejected 1647063 T 0.0020 cur 23.8872 best 23.8626 +05:55:53 it 2902450 acc 901 cyc-rejected 1728136 T 0.0020 cur 23.8983 best 23.8626 +05:58:53 it 3042020 acc 959 cyc-rejected 1810869 T 0.0020 cur 23.8977 best 23.8626 +06:01:53 it 3181697 acc 1003 cyc-rejected 1893616 T 0.0020 cur 23.8977 best 23.8626 +06:04:53 it 3322316 acc 1055 cyc-rejected 1977179 T 0.0020 cur 23.9024 best 23.8626 +06:07:53 it 3460633 acc 1091 cyc-rejected 2059387 T 0.0020 cur 23.9024 best 23.8626 +06:10:53 it 3599587 acc 1134 cyc-rejected 2141854 T 0.0020 cur 23.9024 best 23.8626 +06:13:53 it 3735238 acc 1171 cyc-rejected 2222674 T 0.0020 cur 23.9050 best 23.8626 +06:16:53 it 3863435 acc 1217 cyc-rejected 2298852 T 0.0020 cur 23.9145 best 23.8626 +06:19:53 it 3997047 acc 1261 cyc-rejected 2378577 T 0.0020 cur 23.9145 best 23.8626 +06:22:53 it 4130369 acc 1308 cyc-rejected 2457802 T 0.0020 cur 23.9145 best 23.8626 +06:25:53 it 4269253 acc 1346 cyc-rejected 2540553 T 0.0020 cur 23.9192 best 23.8626 +06:28:53 it 4408800 acc 1384 cyc-rejected 2623377 T 0.0020 cur 23.9240 best 23.8626 +06:31:53 it 4548864 acc 1427 cyc-rejected 2706793 T 0.0020 cur 23.9240 best 23.8626 +06:34:53 it 4685790 acc 1470 cyc-rejected 2788292 T 0.0020 cur 23.9282 best 23.8626 +06:37:53 it 4817819 acc 1523 cyc-rejected 2866664 T 0.0020 cur 23.9313 best 23.8626 +06:40:53 it 4953379 acc 1559 cyc-rejected 2947395 T 0.0020 cur 23.9313 best 23.8626 +06:43:53 it 5093588 acc 1606 cyc-rejected 3030852 T 0.0020 cur 23.9313 best 23.8626 +06:46:53 it 5232671 acc 1653 cyc-rejected 3113625 T 0.0020 cur 23.9313 best 23.8626 +06:49:53 it 5371077 acc 1696 cyc-rejected 3196144 T 0.0020 cur 23.9282 best 23.8626 +06:52:53 it 5505294 acc 1749 cyc-rejected 3276213 T 0.0020 cur 23.9276 best 23.8626 +06:55:53 it 5643562 acc 1795 cyc-rejected 3358507 T 0.0020 cur 23.9276 best 23.8626 +06:58:53 it 5776938 acc 1840 cyc-rejected 3437761 T 0.0020 cur 23.9229 best 23.8626 +07:01:53 it 5914000 acc 1889 cyc-rejected 3519122 T 0.0020 cur 23.9260 best 23.8626 +07:04:53 it 6049613 acc 1925 cyc-rejected 3600028 T 0.0020 cur 23.9260 best 23.8626 +07:07:53 it 6184043 acc 1957 cyc-rejected 3680164 T 0.0020 cur 23.9260 best 23.8626 +07:10:53 it 6323079 acc 1994 cyc-rejected 3762907 T 0.0020 cur 23.9318 best 23.8626 +07:13:53 it 6460296 acc 2029 cyc-rejected 3844152 T 0.0020 cur 23.9292 best 23.8626 +07:16:53 it 6597957 acc 2077 cyc-rejected 3926291 T 0.0020 cur 23.9371 best 23.8626 +07:19:53 it 6732501 acc 2122 cyc-rejected 4006310 T 0.0020 cur 23.9371 best 23.8626 +07:22:53 it 6871512 acc 2161 cyc-rejected 4088959 T 0.0020 cur 23.9339 best 23.8626 +07:25:53 it 7008110 acc 2207 cyc-rejected 4170246 T 0.0020 cur 23.9355 best 23.8626 +07:28:53 it 7146688 acc 2253 cyc-rejected 4252799 T 0.0020 cur 23.9386 best 23.8626 +07:31:53 it 7286015 acc 2295 cyc-rejected 4335775 T 0.0020 cur 23.9386 best 23.8626 +07:34:53 it 7425893 acc 2326 cyc-rejected 4419106 T 0.0020 cur 23.9386 best 23.8626 +07:37:53 it 7565736 acc 2361 cyc-rejected 4502500 T 0.0020 cur 23.9386 best 23.8626 +07:40:53 it 7703080 acc 2401 cyc-rejected 4584389 T 0.0020 cur 23.9434 best 23.8626 +07:43:53 it 7840844 acc 2435 cyc-rejected 4666394 T 0.0020 cur 23.9481 best 23.8626 +07:46:53 it 7975908 acc 2482 cyc-rejected 4746897 T 0.0020 cur 23.9481 best 23.8626 +07:49:53 it 8124467 acc 2525 cyc-rejected 4835207 T 0.0020 cur 23.9429 best 23.8626 +07:52:48 FINAL best Lambda+centre = 23.8626 (word 23.8626); climbs/field hist {3: 72, 4: 128, 5: 228, 6: 62, 7: 81, 8: 54, 9: 7}; profile incl. centre {1: 2205, 2: 446, 3: 478, 4: 133, 5: 40, 8: 8}; centre read dims [8, 8, 8, 8, 8, 8, 8, 8] +07:52:48 done jcr_search4 diff --git a/research/fragmentation-reorder-rigidity/search/sweep_exact_rules.txt b/research/fragmentation-reorder-rigidity/search/sweep_exact_rules.txt new file mode 100644 index 0000000000..2c911d2993 --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/sweep_exact_rules.txt @@ -0,0 +1,6 @@ +01:28:40 JCR v4: fields 632 (pinned 12), contacts 16273, ops 18159, dag edges 204174, frames 4615 +01:30:35 initial Lambda = 23.8626; dynamic graph built, nodes 26171 +01:30:39 sweep 1: 0 levels dropped, Lambda 23.8626; failed: no plan 330, cost 0, cycle 2196 +01:30:40 annealing until 1.0 min, seed 0 +01:31:35 FINAL best Lambda = 23.8626 (word 23.8626); climbs/field hist {3: 72, 4: 129, 5: 227, 6: 63, 7: 87, 8: 48, 9: 6}; climb profile {1: 2201, 2: 416, 3: 510, 4: 125, 5: 40} +01:31:35 done jcr_search4 diff --git a/research/fragmentation-reorder-rigidity/search/sweep_no_centre_pins.txt b/research/fragmentation-reorder-rigidity/search/sweep_no_centre_pins.txt new file mode 100644 index 0000000000..2eeb36beed --- /dev/null +++ b/research/fragmentation-reorder-rigidity/search/sweep_no_centre_pins.txt @@ -0,0 +1,7 @@ +01:32:28 JCR v4: fields 632 (pinned 12), contacts 16089, ops 18159, dag edges 204174, frames 4615 +01:34:16 initial Lambda = 23.8626; dynamic graph built, nodes 26171 +01:34:19 sweep 1: 24 levels dropped, Lambda 23.5009; failed: no plan 322, cost 0, cycle 2155 +01:34:23 sweep 2: 0 levels dropped, Lambda 23.5009; failed: no plan 322, cost 0, cycle 2155 +01:34:23 annealing until 0.2 min, seed 92 +01:34:28 FINAL best Lambda = 23.4866 (word 23.8626); climbs/field hist {3: 72, 4: 170, 5: 196, 6: 53, 7: 87, 8: 48, 9: 6}; climb profile {1: 2150, 2: 414, 3: 501, 4: 98, 5: 78} +01:34:28 done jcr_search4 From cd8cb828172c9ffaf5962bb7217f4118e5d57440 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:35:00 +0300 Subject: [PATCH 3/3] Point the current CI section at frontier5413 (exact repair from #5420) Canonical main still names make frontier4610-verify while the selected record requires frontier5413-verify, so the shared onboarding test fails before any package replay. This reuses byte-for-byte the docs/ci-verification.md repair of #5420 (head baa8fbb8345c2fab0bc213479539c338d4c80443, Clear1nsight); no scientific file changes. Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/ci-verification.md | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 494b7ca1d4..3bf623230e 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,40 @@ # CI verification -## Current selected-family replay: #4610 with #5241 +## Current selected-family replay: #5413 with #5407 and #5414 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md), +[explicit source closure](../certificates/frontier5413-source.json), +[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and +[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json). + +`make frontier5413-verify` authenticates the selected source manifest, derives +the certificate from frozen numerical evidence, and exports the complete +three-package execution closure. It replays #5407's five-stage provider audit, +#5413's eight-stage admission, and #5414's independent companion screen serially. +The exported inputs are checked again afterward. Source-bound #4610/#5241 and +earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly +reused; its historical suites are not rerun. + +Each package runs under an external sampled 1 GiB aggregate descendant-memory +guard, with timeouts of 660 seconds for the provider and primary packages and +120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS +adapter; on Linux it invokes the unmodified package wrappers. The recorded +successful local macOS replay does not establish a hosted Linux pass. + +The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only, +uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads +receipts and logs. Its status is separate from local validation and recorded in +the integration receipt. Routine donor PRs do not launch this selected replay. + +`make selected-record-check` verifies metadata and source/proof hashes. It does +not execute the operators or prove the five inherited framework assumptions. +The finite checks do not establish the full integer multiplication theorem, +and the uniform word remains unmaterialized. + +## Historical selected-family replay: #4610 with #5241 + +The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md), [explicit source closure](../certificates/frontier4610-source.json), [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and