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')