From 9bdd01dd0d3142517f5268285a9fb4ce35469172 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:06:49 -0500 Subject: [PATCH] Compress final Cao word by 151 scalar ADDs per orientation Preserve the complete paid profile and credit the retained compressor. Include exact replay and bounded negative search records. Prepared with substantial OpenAI Codex assistance. --- .../COMPRESSION-STAGES.json | 418 ++++++ .../FILTERED-SEARCH.json | 1121 ++++++++++++++++ .../cao-trace-retiming-20261023/README.md | 98 ++ .../cao-trace-retiming-20261023/SOURCES.json | 139 ++ .../cao-trace-retiming-20261023/TASK.json | 14 + .../UNFILTERED-SEARCH.json | 1127 +++++++++++++++++ .../VERIFICATION.json | 48 + .../cao-trace-retiming-20261023/construct.py | 109 ++ .../cao-trace-retiming-20261023/search.py | 199 +++ .../cao-trace-retiming-20261023/verify.py | 65 + 10 files changed, 3338 insertions(+) create mode 100644 research/cao-trace-retiming-20261023/COMPRESSION-STAGES.json create mode 100644 research/cao-trace-retiming-20261023/FILTERED-SEARCH.json create mode 100644 research/cao-trace-retiming-20261023/README.md create mode 100644 research/cao-trace-retiming-20261023/SOURCES.json create mode 100644 research/cao-trace-retiming-20261023/TASK.json create mode 100644 research/cao-trace-retiming-20261023/UNFILTERED-SEARCH.json create mode 100644 research/cao-trace-retiming-20261023/VERIFICATION.json create mode 100644 research/cao-trace-retiming-20261023/construct.py create mode 100644 research/cao-trace-retiming-20261023/search.py create mode 100644 research/cao-trace-retiming-20261023/verify.py diff --git a/research/cao-trace-retiming-20261023/COMPRESSION-STAGES.json b/research/cao-trace-retiming-20261023/COMPRESSION-STAGES.json new file mode 100644 index 0000000000..414082375a --- /dev/null +++ b/research/cao-trace-retiming-20261023/COMPRESSION-STAGES.json @@ -0,0 +1,418 @@ +{ + "backward": { + "stages": [ + { + "iteration": 0, + "merge": [ + 70, + 28 + ], + "triangles": { + "source_update": 14, + "target_update": 3 + }, + "len": 21334, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 1, + "merge": [ + 8, + 8 + ], + "triangles": { + "target_update": 2 + }, + "len": 21316, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 2, + "merge": [ + 4, + 4 + ], + "triangles": { + "target_update": 2 + }, + "len": 21306, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 3, + "merge": [ + 4, + 4 + ], + "triangles": {}, + "len": 21298, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 4, + "merge": [ + 0, + 0 + ], + "triangles": {}, + "len": 21298, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + } + ], + "caps": [ + { + "operator": 52, + "owner": 83, + "next_event": 9347, + "cap": [ + 0, + 382 + ] + }, + { + "operator": 53, + "owner": 98, + "next_event": 8886, + "cap": [ + 0, + 487 + ] + }, + { + "operator": 48, + "owner": 55, + "next_event": 8739, + "cap": [ + 0, + 324 + ] + }, + { + "operator": 49, + "owner": 74, + "next_event": 9353, + "cap": [ + 0, + 352 + ] + }, + { + "operator": 50, + "owner": 85, + "next_event": 8892, + "cap": [ + 0, + 505 + ] + }, + { + "operator": 54, + "owner": 101, + "next_event": 8733, + "cap": [ + 0, + 375 + ] + }, + { + "operator": 56, + "owner": 80, + "next_event": 9500, + "cap": [ + 0, + 494 + ] + }, + { + "operator": 58, + "owner": 31, + "next_event": 8586, + "cap": [ + 0, + 26 + ] + }, + { + "operator": 47, + "owner": 33, + "next_event": 9046, + "cap": [ + 0, + 138 + ] + }, + { + "operator": 51, + "owner": 49, + "next_event": 9040, + "cap": [ + 0, + 148 + ] + }, + { + "operator": 57, + "owner": 88, + "next_event": 9506, + "cap": [ + 0, + 477 + ] + }, + { + "operator": 55, + "owner": 68, + "next_event": 9653, + "cap": [ + 0, + 176 + ] + } + ], + "old_scalar": 17453, + "new_scalar": 17302 + }, + "forward": { + "stages": [ + { + "iteration": 0, + "merge": [ + 70, + 28 + ], + "triangles": { + "source_update": 3, + "target_update": 14 + }, + "len": 21334, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 1, + "merge": [ + 8, + 8 + ], + "triangles": { + "source_update": 2 + }, + "len": 21316, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 2, + "merge": [ + 4, + 4 + ], + "triangles": { + "source_update": 2 + }, + "len": 21306, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 3, + "merge": [ + 4, + 4 + ], + "triangles": {}, + "len": 21298, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + }, + { + "iteration": 4, + "merge": [ + 0, + 0 + ], + "triangles": {}, + "len": 21298, + "paid": { + "1": 2201, + "3": 510, + "2": 412, + "4": 127, + "8": 8, + "5": 40 + } + } + ], + "caps": [ + { + "operator": 52, + "owner": 83, + "next_event": 9347, + "cap": [ + 0, + 382 + ] + }, + { + "operator": 53, + "owner": 98, + "next_event": 8886, + "cap": [ + 0, + 487 + ] + }, + { + "operator": 48, + "owner": 55, + "next_event": 8739, + "cap": [ + 0, + 324 + ] + }, + { + "operator": 49, + "owner": 74, + "next_event": 9353, + "cap": [ + 0, + 352 + ] + }, + { + "operator": 50, + "owner": 85, + "next_event": 8892, + "cap": [ + 0, + 505 + ] + }, + { + "operator": 54, + "owner": 101, + "next_event": 8733, + "cap": [ + 0, + 375 + ] + }, + { + "operator": 56, + "owner": 80, + "next_event": 9500, + "cap": [ + 0, + 494 + ] + }, + { + "operator": 58, + "owner": 31, + "next_event": 8586, + "cap": [ + 0, + 26 + ] + }, + { + "operator": 47, + "owner": 33, + "next_event": 9046, + "cap": [ + 0, + 138 + ] + }, + { + "operator": 51, + "owner": 49, + "next_event": 9040, + "cap": [ + 0, + 148 + ] + }, + { + "operator": 57, + "owner": 88, + "next_event": 9506, + "cap": [ + 0, + 477 + ] + }, + { + "operator": 55, + "owner": 68, + "next_event": 9653, + "cap": [ + 0, + 176 + ] + } + ], + "old_scalar": 17453, + "new_scalar": 17302 + } +} diff --git a/research/cao-trace-retiming-20261023/FILTERED-SEARCH.json b/research/cao-trace-retiming-20261023/FILTERED-SEARCH.json new file mode 100644 index 0000000000..301bb9d18e --- /dev/null +++ b/research/cao-trace-retiming-20261023/FILTERED-SEARCH.json @@ -0,0 +1,1121 @@ +{ + "actual_moment_reduction": 0.0, + "changed_helpers": [], + "changed_scalar_contacts": 170, + "constant": 15.162203279216296, + "constraints": 308767, + "counts": { + "gap_0": 605, + "gap_1": 835, + "gap_2": 67, + "gap_3": 17, + "gap_4": 2, + "gap_5": 21 + }, + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "message": "Optimization terminated successfully. (HiGHS Status 7: Optimal)", + "numpy": "2.3.5", + "objective": 12.636866373023686, + "old_objective": 12.63686637302348, + "operator": "all", + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "scipy": "1.17.0", + "seconds": 13.645766321999986, + "solver_status": 0, + "status": "DISCOVERY_ONLY", + "variables": 1635654, + "warp_recipes": { + "1": { + "G_columns": [ + 1, + 2, + 4, + 8, + 64, + 19, + 104, + 197, + 325 + ], + "input": 292, + "output": 293 + }, + "2": { + "G_columns": [ + 1, + 2, + 4, + 8, + 128, + 76, + 290, + 406, + 392 + ], + "input": 292, + "output": 3929 + }, + "3": { + "G_columns": [ + 1, + 2, + 4, + 71, + 8, + 420, + 406, + 128, + 261 + ], + "input": 295, + "output": 3929 + }, + "4": { + "G_columns": [ + 1, + 2, + 4, + 71, + 8, + 420, + 406, + 128, + 261 + ], + "input": 295, + "output": 3929 + }, + "5": { + "G_columns": [ + 2, + 4, + 8, + 32, + 76, + 128, + 404, + 392, + 37 + ], + "input": 304, + "output": 4308 + }, + "6": { + "G_columns": [ + 2, + 4, + 8, + 32, + 76, + 410, + 392, + 128, + 131 + ], + "input": 303, + "output": 4308 + }, + "7": { + "G_columns": [ + 1, + 2, + 8, + 15, + 27, + 74, + 170, + 32, + 257 + ], + "input": 297, + "output": 298 + }, + "8": { + "G_columns": [ + 1, + 2, + 4, + 16, + 27, + 53, + 81, + 128, + 275 + ], + "input": 299, + "output": 300 + }, + "9": { + "G_columns": [ + 1, + 2, + 4, + 16, + 27, + 53, + 81, + 128, + 275 + ], + "input": 299, + "output": 300 + }, + "10": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 143, + 151, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "11": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 143, + 151, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "12": { + "G_columns": [ + 1, + 2, + 4, + 64, + 74, + 86, + 99, + 128, + 326 + ], + "input": 303, + "output": 302 + }, + "13": { + "G_columns": [ + 1, + 2, + 4, + 64, + 74, + 128, + 81, + 99, + 389 + ], + "input": 304, + "output": 302 + }, + "14": { + "G_columns": [ + 1, + 2, + 4, + 27, + 46, + 8, + 198, + 64, + 264 + ], + "input": 305, + "output": 293 + }, + "15": { + "G_columns": [ + 1, + 2, + 4, + 40, + 86, + 8, + 132, + 16, + 282 + ], + "input": 305, + "output": 306 + }, + "16": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 64, + 107, + 198, + 326 + ], + "input": 307, + "output": 293 + }, + "17": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 64, + 107, + 198, + 326 + ], + "input": 307, + "output": 293 + }, + "18": { + "G_columns": [ + 1, + 2, + 4, + 8, + 43, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "19": { + "G_columns": [ + 1, + 2, + 4, + 8, + 43, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "20": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 62, + 94, + 129, + 257 + ], + "input": 309, + "output": 306 + }, + "21": { + "G_columns": [ + 1, + 2, + 4, + 16, + 128, + 138, + 55, + 65, + 404 + ], + "input": 309, + "output": 300 + }, + "22": { + "G_columns": [ + 1, + 2, + 4, + 10, + 33, + 68, + 16, + 128, + 263 + ], + "input": 310, + "output": 300 + }, + "23": { + "G_columns": [ + 1, + 2, + 8, + 75, + 13, + 400, + 16, + 128, + 163 + ], + "input": 310, + "output": 2081 + }, + "24": { + "G_columns": [ + 1, + 2, + 8, + 75, + 13, + 400, + 16, + 128, + 163 + ], + "input": 310, + "output": 2081 + }, + "25": { + "G_columns": [ + 1, + 2, + 8, + 75, + 13, + 400, + 16, + 128, + 163 + ], + "input": 310, + "output": 2081 + }, + "26": { + "G_columns": [ + 1, + 2, + 8, + 16, + 128, + 81, + 141, + 403, + 58 + ], + "input": 292, + "output": 2081 + }, + "27": { + "G_columns": [ + 2, + 4, + 8, + 32, + 128, + 74, + 312, + 422, + 11 + ], + "input": 292, + "output": 4308 + }, + "28": { + "G_columns": [ + 2, + 4, + 8, + 108, + 32, + 436, + 422, + 128, + 161 + ], + "input": 295, + "output": 4308 + }, + "29": { + "G_columns": [ + 1, + 2, + 4, + 71, + 8, + 420, + 406, + 128, + 261 + ], + "input": 295, + "output": 3929 + }, + "30": { + "G_columns": [ + 2, + 1, + 8, + 16, + 128, + 29, + 160, + 81, + 408 + ], + "input": 313, + "output": 314 + }, + "31": { + "G_columns": [ + 1, + 8, + 16, + 128, + 155, + 148, + 160, + 88, + 401 + ], + "input": 315, + "output": 314 + }, + "32": { + "G_columns": [ + 1, + 8, + 16, + 128, + 154, + 264, + 217, + 249, + 252 + ], + "input": 1909, + "output": 314 + }, + "33": { + "G_columns": [ + 1, + 2, + 8, + 16, + 266, + 30, + 57, + 112, + 224 + ], + "input": 1909, + "output": 1552 + }, + "34": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "35": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "36": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "37": { + "G_columns": [ + 1, + 2, + 4, + 128, + 140, + 148, + 163, + 389, + 451 + ], + "input": 1922, + "output": 1551 + }, + "38": { + "G_columns": [ + 1, + 2, + 4, + 128, + 142, + 156, + 260, + 183, + 243 + ], + "input": 1934, + "output": 1551 + }, + "39": { + "G_columns": [ + 1, + 2, + 4, + 128, + 142, + 156, + 260, + 183, + 243 + ], + "input": 1934, + "output": 1551 + }, + "40": { + "G_columns": [ + 1, + 2, + 4, + 128, + 142, + 156, + 260, + 183, + 243 + ], + "input": 1934, + "output": 1551 + }, + "41": { + "G_columns": [ + 1, + 2, + 8, + 32, + 266, + 425, + 36, + 195, + 218 + ], + "input": 1934, + "output": 298 + }, + "42": { + "G_columns": [ + 1, + 2, + 8, + 15, + 27, + 74, + 32, + 129, + 298 + ], + "input": 323, + "output": 298 + }, + "43": { + "G_columns": [ + 1, + 2, + 4, + 257, + 456, + 8, + 415, + 16, + 43 + ], + "input": 305, + "output": 3503 + }, + "44": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 279, + 448, + 410, + 48 + ], + "input": 309, + "output": 3503 + }, + "45": { + "G_columns": [ + 1, + 2, + 4, + 257, + 456, + 8, + 415, + 16, + 43 + ], + "input": 305, + "output": 3503 + }, + "46": { + "G_columns": [ + 1, + 2, + 4, + 8, + 270, + 450, + 402, + 16, + 39 + ], + "input": 299, + "output": 3503 + }, + "47": { + "G_columns": [ + 1, + 2, + 4, + 64, + 84, + 128, + 98, + 111, + 389 + ], + "input": 304, + "output": 302 + }, + "48": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 145, + 367, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "49": { + "G_columns": [ + 1, + 2, + 4, + 64, + 84, + 128, + 364, + 39, + 449 + ], + "input": 307, + "output": 302 + }, + "50": { + "G_columns": [ + 1, + 2, + 4, + 64, + 415, + 86, + 99, + 128, + 326 + ], + "input": 303, + "output": 302 + }, + "51": { + "G_columns": [ + 1, + 2, + 4, + 16, + 121, + 128, + 55, + 80, + 389 + ], + "input": 304, + "output": 300 + }, + "52": { + "G_columns": [ + 1, + 2, + 4, + 16, + 392, + 128, + 162, + 68, + 401 + ], + "input": 307, + "output": 300 + }, + "53": { + "G_columns": [ + 1, + 2, + 4, + 16, + 50, + 492, + 80, + 128, + 278 + ], + "input": 303, + "output": 300 + }, + "54": { + "G_columns": [ + 1, + 2, + 4, + 16, + 128, + 285, + 161, + 195, + 278 + ], + "input": 301, + "output": 300 + }, + "55": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 188, + 94, + 129, + 257 + ], + "input": 309, + "output": 306 + }, + "56": { + "G_columns": [ + 1, + 2, + 4, + 8, + 83, + 424, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "57": { + "G_columns": [ + 1, + 2, + 4, + 8, + 427, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "58": { + "G_columns": [ + 1, + 2, + 4, + 8, + 39, + 92, + 137, + 16, + 278 + ], + "input": 299, + "output": 306 + }, + "59": { + "G_columns": [ + 1, + 4, + 8, + 16, + 23, + 33, + 68, + 128, + 268 + ], + "input": 299, + "output": 326 + }, + "60": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 67, + 128, + 259 + ], + "input": 299, + "output": 327 + }, + "61": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 89, + 153, + 256 + ], + "input": 301, + "output": 328 + }, + "62": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 89, + 128, + 281 + ], + "input": 301, + "output": 329 + }, + "63": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 70, + 128, + 262 + ], + "input": 303, + "output": 330 + }, + "64": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 106, + 128, + 298 + ], + "input": 304, + "output": 331 + }, + "65": { + "G_columns": [ + 1, + 2, + 8, + 6, + 32, + 17, + 73, + 136, + 291 + ], + "input": 332, + "output": 298 + }, + "66": { + "G_columns": [ + 2, + 1, + 8, + 5, + 16, + 32, + 81, + 128, + 256 + ], + "input": 333, + "output": 314 + }, + "67": { + "G_columns": [ + 1, + 2, + 4, + 31, + 44, + 72, + 131, + 8, + 264 + ], + "input": 334, + "output": 335 + }, + "68": { + "G_columns": [ + 1, + 2, + 4, + 30, + 8, + 47, + 65, + 131, + 259 + ], + "input": 336, + "output": 335 + }, + "69": { + "G_columns": [ + 1, + 2, + 4, + 8, + 24, + 39, + 79, + 131, + 259 + ], + "input": 337, + "output": 335 + }, + "70": { + "G_columns": [ + 1, + 2, + 4, + 31, + 8, + 46, + 78, + 130, + 269 + ], + "input": 338, + "output": 335 + }, + "71": { + "G_columns": [ + 1, + 2, + 8, + 16, + 274, + 30, + 32, + 112, + 248 + ], + "input": 1909, + "output": 1160 + }, + "72": { + "G_columns": [ + 1, + 2, + 8, + 16, + 274, + 30, + 32, + 112, + 248 + ], + "input": 1909, + "output": 1160 + } + } +} diff --git a/research/cao-trace-retiming-20261023/README.md b/research/cao-trace-retiming-20261023/README.md new file mode 100644 index 0000000000..ea1c3ea016 --- /dev/null +++ b/research/cao-trace-retiming-20261023/README.md @@ -0,0 +1,98 @@ +# Scalar compression on the final Cao native word + +**Author-checked result; not yet independently reviewed; no new kappa.** Applying Cinna Davis's +PR4692 compressor to Cao Yifan's final PR4610 word, with one paid-profile-safe +exception, removes **151 scalar ADD macros in each orientation** while preserving +every chronological per-owner Fourier climb. The conservative real scalar allowance falls by **1,216 per call**: forward `158120 -> 156904`, backward `158168 -> 156952`. The complete paid profile remains +`{1:2201,2:412,3:510,4:127,5:40,8:8}`. All 408 independent helper boundaries, +632 independent inputs, main boundaries, native maps, phases and owned operations +are unchanged. Consequently the entire recursive moment is identical. + +The changed word passes both retained exact literal interpreters on all 632 +arbitrary-input columns in both directions. The formal prefix magnitude remains below the retained 2^192 envelope. A corrupted scalar sign is rejected. +No new native phase recipe is needed: every chronological frame transition is +exactly inherited. This is not an integer-multiplication theorem, a higher +conditional exponent, a measured runtime speedup or a selected-result update. + +## Construction and predecessor credit + +`construct.py` imports the original commuting ADD merger and reproduces the +credited triangle rewrite from PR4692. Its only new triangle restriction excludes +helper 628. Without that restriction, the repeated compressor removes 152 macros +but splits its original rank-four transition `0 -> 2085` into rank-two transitions +`0 -> 131 -> 2085`. For `0 4^t`, so that +additional deletion worsens the recursive bill. The restriction keeps 151 deletions +and the entire predecessor invoice. Four productive rewrite rounds suffice; +a fifth round confirms the fixed point. + +PR5265 independently supplied 17 commuting inverse pairs (34 removed ADDs) on the +same final Cao word. This package uses PR4692's broader predecessor compressor; +it claims neither priority for the rewrite identities nor a kappa improvement. +Cinna Davis's original PR4692 applied the compressor to the older selected PR4470 +word. Cao Yifan's PR4610 supplies the newer native word and joint-map optimizer. +Credit Cinna Davis, Dugongue, zxv, Jacob Alan Sussman and all retained native, +Clifford, scalar, geometry, compiler, precision and analytic sources. +Prepared for ahrazzle with substantial OpenAI Codex assistance; Apache-2.0. + +## Exact replay + +From the repository root, with Python 3.12 and the source files pinned in +`SOURCES.json`: + +```sh +python3 -B research/cao-trace-retiming-20261023/verify.py +``` + +This rebuilds the word in memory, checks every source hash, verifies both exact +interpreters and the scalar corruption controls. The source archive and all frozen +predecessor receipts remain unchanged. The default verifier is read-only; `--write` is an explicit authoring option. `COMPRESSION-STAGES.json` records the +initial discovery run; `VERIFICATION.json` records the final package replay. + +## Bounded search for a paid gain + +Two full contact/helper/native-map models were run on the changed scalar graphs, +reusing the credited PR4610 exact frame enumeration and floating SciPy/HiGHS +optimizer. All 72 late native maps were available; the 12 prelude line contracts +were preserved. Every enumerated quotient interval had dimension at most five. +The helper exits, scalar chronology after the rewrite, and main boundaries were +fixed; all 408 helper entrances and scalar contacts were variable. + +| Input graph | Variables | Constraints | Best local moment improvement over PR4610 | +|---|---:|---:|---:| +| 152 deletions, including the costly helper 628 triangle | 1,623,742 | 307,270 | -0.000223150946 | +| 151 deletions, helper 628 triangle excluded | 1,635,654 | 308,767 | 0 | + +Both discovery runs retained the predecessor optimizer exponent `t = 1 - 0.00302157135`; the comparator is the final PR4610 paid/helper profile. The filtered optimum has identical complete profiles, so its zero gain holds at every exponent. Both runs completed in about 14 seconds and reported numerical finite-model optimality. +**These are bounded numerical negative searches, not exact ceilings or universal +impossibility results.** `UNFILTERED-SEARCH.json` and `FILTERED-SEARCH.json` preserve +the actual outputs. No negative-screen map candidate is admitted as a new supplier. + +To rerun the filtered optional discovery (SciPy 1.17.0, NumPy 2.3.5 used here): + +```sh +python3 -B research/cao-trace-retiming-20261023/construct.py --output /tmp/cao-trace-word.json.gz +OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 python3 -B research/cao-trace-retiming-20261023/search.py --word /tmp/cao-trace-word.json.gz --operator all --seconds 180 +``` + +The discovery writes separate `DISCOVERY-*` files and does not overwrite the +frozen two search receipts. A solver is unnecessary for the exact positive scalar +result. The candidate has no changed recursive invoice, so no full controller, +compiler, BIT or outer-ledger run is claimed. + +## Prelude-route scope + +An initial attempt to free the common prelude lines was stopped when the live +overlap check found PR5096's first-image theorem and PR5179's inverse-return +rigidity theorem. The 152- and 151-deletion graphs both retain all 12 exact +post-inverse line caps, checked independently through reachable main-Y exits. +This is supplementary bounded evidence, not a new proof of those predecessors. + +## Open next questions + +A paid-profile improvement must change a restriction beyond this tested scalar +rewrite/contact model. One concrete first step is to replace an actual chronological +owner dependency while preserving arbitrary-input action, then test whether the +PR5179 path cap disappears. Its single-edge deletion is a relaxed graph control, +not a legal circuit edit. No repeated fixed-invoice search is justified by the +present negative results alone. The retained physical/native all-size, compiler, +precision, stock, analytic and recovery assumptions remain unresolved here. diff --git a/research/cao-trace-retiming-20261023/SOURCES.json b/research/cao-trace-retiming-20261023/SOURCES.json new file mode 100644 index 0000000000..e4c17024c0 --- /dev/null +++ b/research/cao-trace-retiming-20261023/SOURCES.json @@ -0,0 +1,139 @@ +{ + "canonical_base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "predecessors": { + "native_word": "Cao Yifan / intqwq, PR4610 final round3 payload cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "scalar_compressor": "Cinna Davis /1337isnot1337, PR4692", + "bounded_inverse_pairs": "Chrisbryan17, PR5265", + "underlying": "Cinna Davis PR4470, Dugongue, zxv, Jacob Alan Sussman and retained Apache2.0 source notices" + }, + "files": [ + { + "path": "research/fresh-helper-boundary/CHANGES.json", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/joint-helper-lattice/NATIVE.json.gz", + "sha256": "74582cce642c80f0235be7fcbce3716174666326ac6a1d46d02a62a75d7be4c6" + }, + { + "path": "research/joint-helper-lattice/PATCH.json", + "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727" + }, + { + "path": "research/joint-helper-lattice/native_joint.py", + "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7" + }, + { + "path": "research/kappa-function-composition/complex/prune_native.py", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/kappa-rebuild/complex/native_extensions.py", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3" + }, + { + "path": "research/kappa-rebuild/complex/power_two_balance.py", + "sha256": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD-FREEZE.json", + "sha256": "b464b18dde15a4f3f0f71252f4eacf5a1883115fdff87734819e0b8e59b26285" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/kappa-round3-warp-20261022/constrained_map.py", + "sha256": "2a9767817ce201be17039b6669373abc12df4c9519104d653b0ecda746913b0b" + }, + { + "path": "research/kappa-round3-warp-20261022/helper_line_milp.py", + "sha256": "802defef1b112b70bb9e9ed2ed8fc6c820278e0c745c0ed36c936a64ba684e3b" + }, + { + "path": "research/missing-join-frame/PATCH.json", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e" + }, + { + "path": "research/native-warp-extraction-boundary/algebra.py", + "sha256": "52b73c482f9aa171ac266bf0f5752bb520b100d79949f615d0aa26cb926452ba" + }, + { + "path": "research/native-warp-extraction-boundary/operators.py", + "sha256": "4427aa6bb35b095868381de947d177bdbfc2c92e8e0ef9c5a75731ac4d0ca5bd" + }, + { + "path": "research/scalar-reorder-20261022/intervals.py", + "sha256": "ce8571b2446debaecd83b43441417e102ae1ca3322eb8e118b3e84994f214eed" + }, + { + "path": "research/scalar-trace-compression/verify.py", + "sha256": "b41d69aca44852b4b7b880b74b3b482c2274f7b093573ca663a8f5419c8858be" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/transported-warp-frames/PROOF.md", + "sha256": "cd227d0cc0e34c7b4b6a850a042f0f99099f1fe9b25e0519982e8f5973603f2d" + }, + { + "path": "research/warp-interface-20261022/ACTUAL-WORD-FREEZE.json", + "sha256": "474c3fdd8194639bcfcf7b46259198c8a189bab0be9e059438d74d27a08ec8ca" + }, + { + "path": "research/warp-interface-20261022/ACTUAL-WORD.json.gz", + "sha256": "d578875344095047c383ef513e69b9deb9d99d2b75abe14f7359d06365a924ac" + }, + { + "path": "research/warp-interface-20261022/PATCH.json", + "sha256": "9da8af096dfc08d9a2e953bf8b78e81195fe74e8da2583d5d7fd0eed97f7a748" + }, + { + "path": "research/warp-interface-20261022/PHASE-VALIDATION.json.gz", + "sha256": "352572dd77a20dd4569b0172aed5971f5bdb324efa75798ce6d84089812a1d38" + }, + { + "path": "research/warp-interface-20261022/SOURCES.json", + "sha256": "7d40ebea3255181e900a15557825ba92cc7dd25c7963285b82736b2c2fb2bb0c" + }, + { + "path": "research/warp-interface-20261022/free_warp_contacts.py", + "sha256": "a9f27324c35844cf35193de643bca4231d2b6ac8274ffc89fa1e07b8ef987b1b" + }, + { + "path": "research/warp-interface-20261022/verify_candidate.py", + "sha256": "7aae8922f456673f3be7045c064e4700cf929c51da1316368758fb5cdd3a3e50" + }, + { + "path": "research/warp-interface-20261022/warp_merge.py", + "sha256": "661fe7dc9d079da2753ba8af9b512d24e8c16b39caf709b459709a495d7d17f6" + } + ] +} diff --git a/research/cao-trace-retiming-20261023/TASK.json b/research/cao-trace-retiming-20261023/TASK.json new file mode 100644 index 0000000000..7582042749 --- /dev/null +++ b/research/cao-trace-retiming-20261023/TASK.json @@ -0,0 +1,14 @@ +{ + "task": "paid-profile gain from broader exact scalar rewriting on final PR4610", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "declared_target": "Strict decrease of complete paid-minus-productive moment against PR4610, followed by exact native and full outer admission", + "outcome": "Target not achieved. Exact local 151-macro and 1216-scalar-allowance reduction preserves the complete paid profile. Two bounded global frame/native-map optimizations find no strict gain.", + "scope": "changed scalar chronology, fixed main endpoints/helper exits, free helper entrances and 72 late native maps with 12 retained prelude lines", + "source_delta": "PR4692 broader compressor applied to final PR4610; skip helper 628 triangle because it splits a rank-4 job into two rank-2 jobs", + "related": "PR5265 supplies the 34-macro commuting inverse subset; PR5096/5179 block fixed-scalar-graph prelude freeing", + "stop_rule": "Two complete changed-graph optimizations without positive paid gain; no further fixed-model rounds", + "unrun": "No new full supplier/controller/compiler/outer replay; no end-to-end theorem or exact global-optimum certificate", + "open_next_question": "Replace a chronological owner dependency with a legal arbitrary-input circuit and demonstrate removal of a specific forcing path before further optimization", + "evidence": "VERIFICATION.json, UNFILTERED-SEARCH.json, FILTERED-SEARCH.json", + "status": "AUTHOR_CHECKED_UNREVIEWED" +} diff --git a/research/cao-trace-retiming-20261023/UNFILTERED-SEARCH.json b/research/cao-trace-retiming-20261023/UNFILTERED-SEARCH.json new file mode 100644 index 0000000000..dc913b17d3 --- /dev/null +++ b/research/cao-trace-retiming-20261023/UNFILTERED-SEARCH.json @@ -0,0 +1,1127 @@ +{ + "actual_moment_reduction": -0.00022315094588520878, + "changed_helpers": [ + [ + 538, + 131, + 0 + ] + ], + "changed_scalar_contacts": 86, + "constant": 15.162203279216296, + "constraints": 307270, + "counts": { + "gap_0": 605, + "gap_1": 835, + "gap_2": 67, + "gap_3": 17, + "gap_4": 2, + "gap_5": 21 + }, + "helpers": { + "4": 28, + "7": 6, + "8": 47, + "9": 327 + }, + "message": "Optimization terminated successfully. (HiGHS Status 7: Optimal)", + "numpy": "2.3.5", + "objective": 12.637089523969575, + "old_objective": 12.64521767158779, + "operator": "all", + "paid": { + "1": 2200, + "2": 410, + "3": 511, + "4": 128, + "5": 40, + "8": 8 + }, + "scipy": "1.17.0", + "seconds": 13.878552850000005, + "solver_status": 0, + "status": "DISCOVERY_ONLY", + "variables": 1623742, + "warp_recipes": { + "1": { + "G_columns": [ + 1, + 2, + 4, + 8, + 64, + 19, + 104, + 197, + 325 + ], + "input": 292, + "output": 293 + }, + "2": { + "G_columns": [ + 1, + 2, + 4, + 128, + 256, + 196, + 293, + 17, + 15 + ], + "input": 292, + "output": 3923 + }, + "3": { + "G_columns": [ + 1, + 2, + 4, + 71, + 128, + 35, + 17, + 256, + 394 + ], + "input": 295, + "output": 3923 + }, + "4": { + "G_columns": [ + 1, + 2, + 4, + 71, + 128, + 35, + 17, + 256, + 394 + ], + "input": 295, + "output": 3923 + }, + "5": { + "G_columns": [ + 1, + 2, + 8, + 32, + 384, + 128, + 67, + 60, + 59 + ], + "input": 304, + "output": 4329 + }, + "6": { + "G_columns": [ + 1, + 2, + 8, + 32, + 384, + 72, + 60, + 128, + 152 + ], + "input": 303, + "output": 4329 + }, + "7": { + "G_columns": [ + 1, + 2, + 8, + 15, + 27, + 74, + 170, + 32, + 257 + ], + "input": 297, + "output": 298 + }, + "8": { + "G_columns": [ + 1, + 2, + 4, + 16, + 27, + 53, + 81, + 128, + 275 + ], + "input": 299, + "output": 300 + }, + "9": { + "G_columns": [ + 1, + 2, + 4, + 16, + 27, + 53, + 81, + 128, + 275 + ], + "input": 299, + "output": 300 + }, + "10": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 143, + 151, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "11": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 143, + 151, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "12": { + "G_columns": [ + 1, + 2, + 4, + 64, + 74, + 86, + 99, + 128, + 326 + ], + "input": 303, + "output": 302 + }, + "13": { + "G_columns": [ + 1, + 2, + 4, + 64, + 74, + 128, + 81, + 99, + 389 + ], + "input": 304, + "output": 302 + }, + "14": { + "G_columns": [ + 1, + 2, + 4, + 27, + 46, + 8, + 198, + 64, + 264 + ], + "input": 305, + "output": 293 + }, + "15": { + "G_columns": [ + 1, + 2, + 4, + 40, + 86, + 8, + 132, + 16, + 282 + ], + "input": 305, + "output": 306 + }, + "16": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 64, + 107, + 198, + 326 + ], + "input": 307, + "output": 293 + }, + "17": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 64, + 107, + 198, + 326 + ], + "input": 307, + "output": 293 + }, + "18": { + "G_columns": [ + 1, + 2, + 4, + 8, + 43, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "19": { + "G_columns": [ + 1, + 2, + 4, + 8, + 43, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "20": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 62, + 94, + 129, + 257 + ], + "input": 309, + "output": 306 + }, + "21": { + "G_columns": [ + 1, + 2, + 4, + 16, + 128, + 138, + 55, + 65, + 404 + ], + "input": 309, + "output": 300 + }, + "22": { + "G_columns": [ + 1, + 2, + 4, + 10, + 33, + 68, + 16, + 128, + 263 + ], + "input": 310, + "output": 300 + }, + "23": { + "G_columns": [ + 1, + 8, + 16, + 400, + 21, + 27, + 64, + 128, + 243 + ], + "input": 310, + "output": 2087 + }, + "24": { + "G_columns": [ + 1, + 8, + 16, + 400, + 21, + 27, + 64, + 128, + 243 + ], + "input": 310, + "output": 2087 + }, + "25": { + "G_columns": [ + 1, + 8, + 16, + 400, + 21, + 27, + 64, + 128, + 243 + ], + "input": 310, + "output": 2087 + }, + "26": { + "G_columns": [ + 1, + 8, + 16, + 64, + 128, + 456, + 149, + 18, + 34 + ], + "input": 292, + "output": 2087 + }, + "27": { + "G_columns": [ + 1, + 2, + 8, + 32, + 128, + 387, + 233, + 23, + 16 + ], + "input": 292, + "output": 4329 + }, + "28": { + "G_columns": [ + 1, + 2, + 8, + 416, + 32, + 99, + 23, + 128, + 185 + ], + "input": 295, + "output": 4329 + }, + "29": { + "G_columns": [ + 1, + 2, + 4, + 71, + 128, + 35, + 17, + 256, + 394 + ], + "input": 295, + "output": 3923 + }, + "30": { + "G_columns": [ + 2, + 1, + 8, + 16, + 128, + 29, + 160, + 81, + 408 + ], + "input": 313, + "output": 314 + }, + "31": { + "G_columns": [ + 1, + 8, + 16, + 128, + 155, + 148, + 160, + 88, + 401 + ], + "input": 315, + "output": 314 + }, + "32": { + "G_columns": [ + 1, + 8, + 16, + 128, + 154, + 264, + 217, + 249, + 252 + ], + "input": 1909, + "output": 314 + }, + "33": { + "G_columns": [ + 1, + 2, + 8, + 16, + 266, + 30, + 57, + 112, + 224 + ], + "input": 1909, + "output": 1552 + }, + "34": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "35": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "36": { + "G_columns": [ + 1, + 2, + 8, + 16, + 31, + 51, + 90, + 274, + 384 + ], + "input": 1922, + "output": 1552 + }, + "37": { + "G_columns": [ + 1, + 2, + 4, + 128, + 140, + 148, + 163, + 389, + 451 + ], + "input": 1922, + "output": 1551 + }, + "38": { + "G_columns": [ + 1, + 2, + 4, + 387, + 397, + 415, + 128, + 436, + 496 + ], + "input": 1933, + "output": 1551 + }, + "39": { + "G_columns": [ + 1, + 2, + 4, + 387, + 397, + 415, + 128, + 436, + 496 + ], + "input": 1933, + "output": 1551 + }, + "40": { + "G_columns": [ + 1, + 2, + 4, + 387, + 397, + 415, + 128, + 436, + 496 + ], + "input": 1933, + "output": 1551 + }, + "41": { + "G_columns": [ + 1, + 2, + 8, + 15, + 293, + 390, + 32, + 236, + 245 + ], + "input": 1933, + "output": 298 + }, + "42": { + "G_columns": [ + 1, + 2, + 8, + 15, + 27, + 74, + 32, + 129, + 298 + ], + "input": 323, + "output": 298 + }, + "43": { + "G_columns": [ + 1, + 2, + 4, + 129, + 456, + 8, + 415, + 16, + 43 + ], + "input": 305, + "output": 3499 + }, + "44": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 151, + 448, + 410, + 48 + ], + "input": 309, + "output": 3499 + }, + "45": { + "G_columns": [ + 1, + 2, + 4, + 129, + 456, + 8, + 415, + 16, + 43 + ], + "input": 305, + "output": 3499 + }, + "46": { + "G_columns": [ + 1, + 2, + 4, + 8, + 142, + 450, + 402, + 16, + 39 + ], + "input": 299, + "output": 3499 + }, + "47": { + "G_columns": [ + 1, + 2, + 4, + 64, + 84, + 128, + 98, + 111, + 389 + ], + "input": 304, + "output": 302 + }, + "48": { + "G_columns": [ + 1, + 2, + 4, + 64, + 128, + 145, + 367, + 160, + 326 + ], + "input": 301, + "output": 302 + }, + "49": { + "G_columns": [ + 1, + 2, + 4, + 64, + 84, + 128, + 364, + 39, + 449 + ], + "input": 307, + "output": 302 + }, + "50": { + "G_columns": [ + 1, + 2, + 4, + 64, + 415, + 86, + 99, + 128, + 326 + ], + "input": 303, + "output": 302 + }, + "51": { + "G_columns": [ + 1, + 2, + 4, + 16, + 121, + 128, + 55, + 80, + 389 + ], + "input": 304, + "output": 300 + }, + "52": { + "G_columns": [ + 1, + 2, + 4, + 16, + 392, + 128, + 162, + 68, + 401 + ], + "input": 307, + "output": 300 + }, + "53": { + "G_columns": [ + 1, + 2, + 4, + 16, + 50, + 492, + 80, + 128, + 278 + ], + "input": 303, + "output": 300 + }, + "54": { + "G_columns": [ + 1, + 2, + 4, + 16, + 128, + 285, + 161, + 195, + 278 + ], + "input": 301, + "output": 300 + }, + "55": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 188, + 94, + 129, + 257 + ], + "input": 309, + "output": 306 + }, + "56": { + "G_columns": [ + 1, + 2, + 4, + 8, + 83, + 424, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "57": { + "G_columns": [ + 1, + 2, + 4, + 8, + 427, + 80, + 129, + 16, + 282 + ], + "input": 308, + "output": 306 + }, + "58": { + "G_columns": [ + 1, + 2, + 4, + 8, + 39, + 92, + 137, + 16, + 278 + ], + "input": 299, + "output": 306 + }, + "59": { + "G_columns": [ + 1, + 4, + 8, + 16, + 23, + 33, + 68, + 128, + 268 + ], + "input": 299, + "output": 326 + }, + "60": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 67, + 128, + 259 + ], + "input": 299, + "output": 327 + }, + "61": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 89, + 153, + 256 + ], + "input": 301, + "output": 328 + }, + "62": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 89, + 128, + 281 + ], + "input": 301, + "output": 329 + }, + "63": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 70, + 128, + 262 + ], + "input": 303, + "output": 330 + }, + "64": { + "G_columns": [ + 1, + 2, + 4, + 8, + 16, + 32, + 106, + 128, + 298 + ], + "input": 304, + "output": 331 + }, + "65": { + "G_columns": [ + 1, + 2, + 8, + 6, + 32, + 17, + 73, + 136, + 291 + ], + "input": 332, + "output": 298 + }, + "66": { + "G_columns": [ + 2, + 1, + 8, + 5, + 16, + 32, + 81, + 128, + 256 + ], + "input": 333, + "output": 314 + }, + "67": { + "G_columns": [ + 1, + 2, + 4, + 31, + 44, + 72, + 131, + 8, + 264 + ], + "input": 334, + "output": 335 + }, + "68": { + "G_columns": [ + 1, + 2, + 4, + 30, + 8, + 47, + 65, + 131, + 259 + ], + "input": 336, + "output": 335 + }, + "69": { + "G_columns": [ + 1, + 2, + 4, + 8, + 24, + 39, + 79, + 131, + 259 + ], + "input": 337, + "output": 335 + }, + "70": { + "G_columns": [ + 1, + 2, + 4, + 31, + 8, + 46, + 78, + 130, + 269 + ], + "input": 338, + "output": 335 + }, + "71": { + "G_columns": [ + 1, + 2, + 8, + 16, + 274, + 30, + 32, + 112, + 248 + ], + "input": 1909, + "output": 1160 + }, + "72": { + "G_columns": [ + 1, + 2, + 8, + 16, + 274, + 30, + 32, + 112, + 248 + ], + "input": 1909, + "output": 1160 + } + } +} diff --git a/research/cao-trace-retiming-20261023/VERIFICATION.json b/research/cao-trace-retiming-20261023/VERIFICATION.json new file mode 100644 index 0000000000..639aebc390 --- /dev/null +++ b/research/cao-trace-retiming-20261023/VERIFICATION.json @@ -0,0 +1,48 @@ +{ + "directions": { + "backward": { + "all632_two_interpreters": true, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "owned_center_cleared": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "payload_sha256": "226ed366e94f7c814a7130486b057af790a6b8b80696265abbcb2686e479d6fe", + "real_scalar_allowance_after": 156952, + "real_scalar_allowance_before": 158168, + "removed_scalar_macros": 151, + "saved_allowance": 1216, + "unchanged_ordered_climbs": true, + "wrong_scalar_sign_rejected": true + }, + "forward": { + "all632_two_interpreters": true, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "owned_center_cleared": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "payload_sha256": "7962a288ec9f443f3b74f386b6d76d6bbf8f7d34f0a39742d39d0c7c95745246", + "real_scalar_allowance_after": 156904, + "real_scalar_allowance_before": 158120, + "removed_scalar_macros": 151, + "saved_allowance": 1216, + "unchanged_ordered_climbs": true, + "wrong_scalar_sign_rejected": true + } + }, + "new_kappa": null, + "status": "PASS_CAO_151_MACROS_SAME_COMPLETE_PAID_PROFILE" +} diff --git a/research/cao-trace-retiming-20261023/construct.py b/research/cao-trace-retiming-20261023/construct.py new file mode 100644 index 0000000000..94d8c4ad39 --- /dev/null +++ b/research/cao-trace-retiming-20261023/construct.py @@ -0,0 +1,109 @@ +"""Source-bound scalar compression on Cao Yifan's final PR4610 word. + +The triangle rewrite below is adapted verbatim except its helper628 exclusion +from Cinna Davis's PR4692 (scalar-trace-compression/verify.py), Apache-2.0. +That exclusion preserves the parent's entire chronological transport invoice. +Prepared for ahrazzle with substantial OpenAI Codex assistance. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from pathlib import Path +import importlib.util,gzip,json,sys +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +spec=importlib.util.spec_from_file_location('credited_scalar_compressor',ROOT/'research/scalar-trace-compression/verify.py') +T=importlib.util.module_from_spec(spec);spec.loader.exec_module(T) +roles,is_add,add=T.roles,T.is_add,T.add +SOURCE=ROOT/'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' + +def span(basis): + s={0} + for v in basis:s|={x^v for x in tuple(s)} + return frozenset(s) + +def triangles(program, spaces): + """A B A^-1 shortcuts, requiring all moved-across roles to be disjoint.""" + deleted, replacements, counts = set(), {}, Counter() + for i, first in enumerate(program): + if i in deleted or i in replacements or not is_add(first): + continue + a, b = map(tuple, first[1][1:3]) + alpha = Q(*first[1][3:5]) + j = None + for pos in range(i+1, min(i+180, len(program))): + event = program[pos] + if pos in deleted or pos in replacements or event[0] == 'phase': + break + if roles(event) & {a, b}: + j = pos + break + if j is None or not is_add(program[j]): + continue + middle = program[j] + x, y = map(tuple, middle[1][1:3]) + union = {a, b, x, y} + if len(union) != 3 or ('L', 628) in union: + continue + k = None + for pos in range(j+1, min(j+180, len(program))): + event = program[pos] + if pos in deleted or pos in replacements or event[0] == 'phase': + break + if roles(event) & union: + k = pos + break + if k is None or not is_add(program[k]): + continue + last = program[k] + if last[1][1:3] != first[1][1:3] or Q(*last[1][3:5]) != -alpha: + continue + if any(roles(event) & union for event in program[i+1:j]): + continue + frame = middle[2] + if not spaces[first[2]] <= spaces[frame] <= spaces[last[2]]: + continue + beta = Q(*middle[1][3:5]) + if x == b and y not in {a, b}: + replacement = [middle, add(a, y, -alpha*beta, frame)] + kind = 'source_update' + elif y == a and x not in {a, b}: + replacement = [add(x, a, beta, frame), add(x, b, alpha*beta, frame)] + kind = 'target_update' + else: + continue + deleted.update((i, j, k)) + replacements[j] = replacement + counts[kind] += 1 + result = [] + for index, event in enumerate(program): + if index in replacements: + result.extend(replacements[index]) + elif index not in deleted: + result.append(event) + return result, dict(sorted(counts.items())) + + +def construct(): + original=json.loads(gzip.decompress(SOURCE.read_bytes()));c=deepcopy(original['canonical']) + spaces=[span(b) for b in c['frames']];programs={};history={} + for direction,source in original['programs'].items(): + p=source;history[direction]=[] + for iteration in range(6): + combined,merge=T.combine(p) + reduced,counts=triangles(combined,spaces) + candidate=T.synthesize(c,reduced,spaces) + T.need(T.paid(candidate)==T.paid(source),'Complete original paid profile at every rewrite stage') + history[direction].append({'iteration':iteration,'merge':merge,'triangles':counts,'scalar_count':sum(e[0]=='scalar' for e in candidate)}) + if candidate==p:break + p=candidate + else:raise ValueError('Declared six-round compression budget exceeded') + programs[direction]=p + return original,{'canonical':c,'programs':programs},history + +if __name__=='__main__': + import argparse + ap=argparse.ArgumentParser();ap.add_argument('--output');args=ap.parse_args() + old,new,history=construct() + if args.output:Path(args.output).write_bytes(gzip.compress(json.dumps(new,sort_keys=True,separators=(',',':')).encode(),mtime=0)) + print(json.dumps(history,sort_keys=True)) diff --git a/research/cao-trace-retiming-20261023/search.py b/research/cao-trace-retiming-20261023/search.py new file mode 100644 index 0000000000..07f2d1168c --- /dev/null +++ b/research/cao-trace-retiming-20261023/search.py @@ -0,0 +1,199 @@ +"""Credited PR4610 helper_line_milp adapted to an explicitly supplied changed word. +Discovery only, no exact optimality claim. Apache-2.0; OpenAI assistance. +""" +from collections import Counter,defaultdict +from copy import deepcopy +from itertools import product +from pathlib import Path +import argparse,gzip,json,sys,time +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +sys.path.insert(0,str(HERE/'.deps')) +import numpy as np +import scipy +from scipy.optimize import milp,Bounds,LinearConstraint +from scipy.sparse import csc_array +sys.path.insert(0,str(ROOT/'research/kappa-round3-warp-20261022')) +sys.path.insert(0,str(ROOT/'research/warp-interface-20261022')) +from warp_merge import J,F,roles,synthesize +from constrained_map import line_matching_map +from free_warp_contacts import matching_map +sys.path.insert(0,str(ROOT/'research/scalar-reorder-20261022')) +from intervals import complete_interval + + +def main(op,time_limit): + started=time.monotonic();payload=json.loads(gzip.decompress((Path(INPUT_WORD)).read_bytes()));c=payload['canonical'];programs=payload['programs'];p=[deepcopy(e) for e in programs['forward'] if e[0]!='climb'] + spans=[F.span(b) for b in c['frames']];dims=[len(b) for b in c['frames']];labels={s:i for i,s in enumerate(spans)} + def label(s): + s=frozenset(s) + if s not in labels: + b=[];v={0} + for x in sorted(s): + if x not in v:b.append(x);v|={y^x for y in tuple(v)} + labels[s]=len(spans);spans.append(s);dims.append(len(b));c['frames'].append(b) + return labels[s] + jc={};mc={} + def join(a,b): + key=min(a,b),max(a,b) + if key not in jc: + if spans[a]<=spans[b]:jc[key]=b + elif spans[b]<=spans[a]:jc[key]=a + else: + v=set(spans[a]) + for x in c['frames'][b]: + if x not in v:v|={y^x for y in tuple(v)} + jc[key]=label(v) + return jc[key] + def meet(a,b): + key=min(a,b),max(a,b) + if key not in mc:mc[key]=label(spans[a]&spans[b]) + return mc[key] + const=lambda f:-f-1 + fixed=lambda n:-n-1 + ops=list(range(1,73)) if op=='all' else [op] + line_constraints={} + selected_ops={} + for operator in ops: + occurrence=[i for i,e in enumerate(p) if e[0]=='warp' and abs(e[2])==operator] + candidates=[i for i in occurrence if dims[p[i][3]] not in (0,9) or dims[p[i][4]] not in (0,9)] + chosen=max(candidates,key=lambda i:dims[p[i][3]]) + F.need(p[chosen][2]>0,'Positive selected late warp') + selected_ops[chosen]=operator + if len(candidates)>1: + pairs={(p[i][3],p[i][4]) if p[i][2]>0 else (p[i][4],p[i][3]) for i in candidates if i!=chosen} + F.need(len(pairs)==1,'One preserved prelude line pair') + a,b=next(iter(pairs));F.need(dims[a]==dims[b]==1,'Fixed line constraint');line_constraints[operator]=(c['frames'][a][0],c['frames'][b][0]) + helper_nodes={len(p)+r:r for r in range(224,632)} + current=[len(p)+r if r>=224 else const(f) for r,f in enumerate(c['start'])];edges=[];original={n:c['start'][r] for n,r in helper_nodes.items()};variables=list(helper_nodes);free_records={} + def edge(a,b): + if isinstance(a,tuple): + edges.append((a[0],b,a[1]));free_records[a[1]]=(a[0],b) + else:edges.append((a,b,'normal')) + for i,e in enumerate(p): + rs=roles(e) + if e[0]=='scalar' and rs: + g=e[1];allL=all(r[0]=='L' for r in (g[1:3] if g[0] in ('add','copy') else g[1:2])) + node=i if allL else const(e[2]) + if allL:variables.append(i);original[i]=e[2] + for r in rs:edge(current[r],node);current[r]=node + elif e[0]=='warp': + r=e[1][1] + if i in selected_ops:current[r]=(current[r],selected_ops[i]) + else:edge(current[r],const(e[3]));current[r]=const(e[4]) + for r,f in enumerate(c['final']):edge(current[r],const(f)) + for n,r in helper_nodes.items():edges.append((n,const(c['final'][r]),'helper')) + incoming=defaultdict(list);outgoing=defaultdict(list) + for a,b,k in edges: + if k=='normal':incoming[b].append(a);outgoing[a].append(b) + lower={};upper={} + for n in variables: + z=0 + for a in incoming[n]:z=join(z,lower[a] if a>=0 else fixed(a)) + lower[n]=z + for n in reversed(variables): + z=1 + for b in outgoing[n]:z=meet(z,upper[b] if b>=0 else fixed(b)) + upper[n]=z + domain={};cache={};counts=Counter() + for n in variables: + lo,hi=lower[n],upper[n];key=lo,hi + F.need(spans[lo]<=spans[original[n]]<=spans[hi],'Original scalar in relaxed interval') + if key not in cache: + qs={};choices=complete_interval(spans,dims,c['frames'],(lo,),(hi,),qs,max_gap=5) + counts.update(qs) + # Wide intervals use a bounded, explicitly incomplete catalogue. + if qs.get('skipped_large_interval') and len(choices)>128: + choices=sorted(choices,key=lambda f:(dims[f],f));step=max(1,len(choices)//120);choices=choices[::step][:120]+[lo,hi] + counts['catalogue_truncated']+=1 + cache[key]=choices + domain[n]=list(dict.fromkeys(cache[key]+[original[n]])) + aliases={n:const(v[0]) for n,v in domain.items() if len(v)==1} + E=Counter((aliases.get(a,a),aliases.get(b,b),k) for a,b,k in edges) + active={n:v for n,v in domain.items() if len(v)>1} + print('MODEL_DOMAINS',op,len(active),sum(map(len,active.values())),dict(counts),flush=True) + costs=[];integrality=[];nodevars={};rows=[];cols=[];data=[];lb=[];ub=[] + def newvar(cost,integer=False): + i=len(costs);costs.append(cost);integrality.append(int(integer));return i + def constraint(coefs,target): + r=len(lb);lb.append(target);ub.append(target) + for v,a in coefs.items(): + if a:rows.append(r);cols.append(v);data.append(a) + for n,choices in active.items(): + nodevars[n]={f:newvar(0.,True) for f in choices};constraint({v:1 for v in nodevars[n].values()},1) + t=1-.00302157135;weight=[0.]+[r**t-r for r in range(1,10)];constant=0.;old_objective=0. + def oldframe(n):return original[n] if n>=0 else fixed(n) + for (a,b,kind),multiplicity in E.items(): + A=active[a] if a>=0 else [fixed(a)];B=active[b] if b>=0 else [fixed(b)] + # The retained native grammar has no zero-rank frame-retag event. + # Keep identical frame IDs on zero-rank ordinary edges; a same-span + # different-gauge monomial is outside this bounded discovery model. + def valid(f,g): + if kind=='helper':return spans[f]dims[g]:return False + if kind not in line_constraints:return True + a,b=line_constraints[kind] + return (b in spans[g]) if a in spans[f] else (dims[f].999,'Integral proposed frame') + recipes={} + for operator,(A,B) in free_records.items(): + fa=chosen[A] if A>=0 else fixed(A);fb=chosen[B] if B>=0 else fixed(B) + F.need(dims[fa]<=dims[fb],'Actual free-warp rank compatibility') + if operator in line_constraints: + G,outbasis=line_matching_map(c['frames'][fa],c['frames'][fb],*line_constraints[operator]) + fo=label(F.span(outbasis)) + else: + fo=fb if dims[fa]==dims[fb] else label(F.span(c['frames'][fb][:dims[fa]]));G=matching_map(c['frames'][fa],c['frames'][fo]) + recipes[operator]={'input':fa,'output':fo,'G_columns':G} + altered={} + for direction,word in programs.items(): + raw=[deepcopy(e) for e in word if e[0]!='climb'] + for i,f in chosen.items(): + if i1e-9: + row['status']='POSITIVE_UNVERIFIED_NATIVE_CANDIDATE' + (HERE/'DISCOVERY-CANDIDATE.json').write_text(json.dumps(row,indent=2,sort_keys=True)+'\n') + (HERE/'DISCOVERY-CANDIDATE-WORD.json.gz').write_bytes(gzip.compress(json.dumps({'canonical':c,'programs':altered},sort_keys=True,separators=(',',':')).encode(),mtime=0)) + (HERE/f'DISCOVERY-OP{op}.json').write_text(json.dumps(row,indent=2,sort_keys=True)+'\n');print(json.dumps(row,sort_keys=True));return row + + +if __name__=='__main__': + ap=argparse.ArgumentParser();ap.add_argument('--word',required=True);ap.add_argument('--operator',default='all');ap.add_argument('--seconds',type=float,default=20);args=ap.parse_args();INPUT_WORD=args.word;main(args.operator if args.operator=='all' else int(args.operator),args.seconds) diff --git a/research/cao-trace-retiming-20261023/verify.py b/research/cao-trace-retiming-20261023/verify.py new file mode 100644 index 0000000000..bd7fae654d --- /dev/null +++ b/research/cao-trace-retiming-20261023/verify.py @@ -0,0 +1,65 @@ +#!/usr/bin/env python3 +"""Independent-endpoint replay of the exact proposed scalar word, no optimizer. + +Apache-2.0; substantial OpenAI Codex assistance. The native interpreters are +credited retained dependencies, not newly independent implementations here. +""" +from collections import defaultdict +from copy import deepcopy +from hashlib import sha256 +from fractions import Fraction +from pathlib import Path +import json,sys +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +sys.path.insert(0,str(HERE)) +from construct import construct,T +sys.path.insert(0,str(ROOT/'research/warp-interface-20261022')) +from warp_merge import F + +def climbs(word): + result=defaultdict(list) + for e in word: + if e[0]=='climb':result[e[2]].append(e[3:]) + return dict(result) + +def main(): + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + F.need(sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'Pinned source '+row['path']) + old,new,history=construct();c=new['canonical'] + F.need(c==old['canonical'],'All helper/main boundaries, native maps and frame registry are unchanged') + V=F.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py','trace_cao_rows') + X=F.load(ROOT/'research/kappa-rebuild/complex/native_extensions.py','trace_cao_literal') + result={'status':'PASS_CAO_151_MACROS_SAME_COMPLETE_PAID_PROFILE','new_kappa':None,'directions':{}} + for d,p in new['programs'].items(): + original=old['programs'][d];b=d=='backward' + F.need(climbs(p)==climbs(original),'Every chronological per-owner transport is unchanged') + F.need([e for e in p if e[0] not in ('climb','scalar')]==[e for e in original if e[0] not in ('climb','scalar')],'Native warps, centers, adapters and phases are unchanged') + F.need(sum(e[0]=='scalar' for e in original)-sum(e[0]=='scalar' for e in p)==151,'Exactly151 removed scalar macros') + rows,rec=X.literal_replay(V,c,p,b) + F.need(all(rows['L',r]==V.expected(('L',r),[],b,False) for r in range(632)),'All632 arbitrary independent endpoint columns') + F.need(Fraction(rec['max_formal_prefix_l1']) < 2**192, + 'Retained formal prefix magnitude envelope') + rebound=deepcopy(c);rebound['R']=len(c['start'])-2*c['v'];rebound['local_profile']={int(k):v for k,v in rec['paid_profile'].items()} + second=V.replay(p,rebound,[],b,False) + _,baseline=X.literal_replay(V,c,original,b) + wrong=deepcopy(p);e=next(e for e in wrong if T.is_add(e));e[1][3]*=-1 + rejected=False + try: + badrows,_=X.literal_replay(V,c,wrong,b) + rejected=any(badrows['L',r]!=V.expected(('L',r),[],b,False) for r in range(632)) + except (ValueError,AssertionError):rejected=True + F.need(rejected,'A scalar coefficient sign corruption is rejected') + result['directions'][d]={'removed_scalar_macros':151,'real_scalar_allowance_before':baseline['real_scalar_allowance'],'real_scalar_allowance_after':rec['real_scalar_allowance'],'saved_allowance':baseline['real_scalar_allowance']-rec['real_scalar_allowance'],'paid':rec['paid_profile'],'owned_center_cleared':rec['arbitrary_owned_C0_cleared'],'all632_two_interpreters':True,'unchanged_ordered_climbs':True,'wrong_scalar_sign_rejected':True,'payload_sha256':sha256(json.dumps(p,sort_keys=True,separators=(',',':')).encode()).hexdigest()} + result['directions'][d]['max_formal_prefix_l1']=rec['max_formal_prefix_l1'] + result['directions'][d]['max_denominator']=rec['max_denominator'] + print('PASS',d,result['directions'][d]['saved_allowance'],flush=True) + print(json.dumps(result,sort_keys=True)) + return result +if __name__=='__main__': + import argparse + ap=argparse.ArgumentParser();ap.add_argument('--write',action='store_true');args=ap.parse_args() + result=json.loads(json.dumps(main()));path=HERE/'VERIFICATION.json' + if args.write:path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:F.need(result==json.loads(path.read_text()),'Exact deterministic committed receipt') + print('PASS_DETERMINISTIC_CAO_TRACE_RECEIPT')