From c8e37d5d0276f8ddd01d9a242cdccba0f44ddbbd Mon Sep 17 00:00:00 2001 From: Hanson Sun Date: Tue, 13 Oct 2026 22:06:54 -0400 Subject: [PATCH] Prove cross-block locality for fixed complex late interfaces --- .../CERTIFICATE.json | 5615 +++++++++++++++++ .../INDEPENDENT.json | 411 ++ .../complex-cross-block-locality/NOTICE.md | 15 + .../complex-cross-block-locality/PROOF.md | 270 + .../complex-cross-block-locality/README.md | 146 + .../complex-cross-block-locality/SOURCES.json | 44 + .../complex-cross-block-locality/TASK.json | 93 + .../VALIDATION.md | 39 + .../complex-cross-block-locality/VERIFY.json | 42 + .../independent.py | 264 + .../test_package.py | 91 + .../complex-cross-block-locality/verify.py | 377 ++ 12 files changed, 7407 insertions(+) create mode 100644 research/complex-cross-block-locality/CERTIFICATE.json create mode 100644 research/complex-cross-block-locality/INDEPENDENT.json create mode 100644 research/complex-cross-block-locality/NOTICE.md create mode 100644 research/complex-cross-block-locality/PROOF.md create mode 100644 research/complex-cross-block-locality/README.md create mode 100644 research/complex-cross-block-locality/SOURCES.json create mode 100644 research/complex-cross-block-locality/TASK.json create mode 100644 research/complex-cross-block-locality/VALIDATION.md create mode 100644 research/complex-cross-block-locality/VERIFY.json create mode 100644 research/complex-cross-block-locality/independent.py create mode 100644 research/complex-cross-block-locality/test_package.py create mode 100644 research/complex-cross-block-locality/verify.py diff --git a/research/complex-cross-block-locality/CERTIFICATE.json b/research/complex-cross-block-locality/CERTIFICATE.json new file mode 100644 index 0000000000..9f98a13b3a --- /dev/null +++ b/research/complex-cross-block-locality/CERTIFICATE.json @@ -0,0 +1,5615 @@ +{ + "blocks": [ + { + "Q": [ + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "1/2", + "0", + "1/2" + ], + [ + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "1/2", + "0", + "1/2", + "0" + ] + ], + "R": [ + [ + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2" + ], + [ + "0", + "-1/2", + "0", + "1/2" + ] + ], + "base": 592, + "caps": [ + [ + 320, + 192, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 258, + 130, + 66, + 32, + 18, + 10, + 6, + 1 + ], + [ + 257, + 129, + 65, + 33, + 16, + 9, + 5, + 2 + ], + [ + 257, + 129, + 65, + 33, + 17, + 8, + 4, + 3 + ] + ], + "common": [ + 320, + 192, + 45, + 30 + ], + "corrections": [ + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431 + ], + "first_correction": 420, + "first_input": 1054, + "helpers": [ + 592, + 593, + 594, + 595, + 596, + 597, + 598, + 599 + ], + "high": [ + 595, + 597, + 598, + 599 + ], + "input_frames": [ + [ + 271, + 143, + 79, + 45, + 30 + ], + [ + 320, + 192, + 41, + 26, + 4 + ], + [ + 320, + 192, + 44, + 30, + 1 + ], + [ + 266, + 138, + 74, + 45, + 30 + ], + [ + 262, + 134, + 70, + 45, + 30 + ], + [ + 320, + 192, + 32, + 19, + 13 + ], + [ + 320, + 192, + 37, + 22, + 8 + ], + [ + 259, + 131, + 67, + 45, + 30 + ] + ], + "inputs": [ + 283, + 100, + 315, + 48, + 347, + 82, + 379, + 67 + ], + "low": [ + 592, + 593, + 594, + 596 + ], + "output_entries": [ + 1420, + 1417, + 1416, + 1421 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 320, + 192, + 33, + 16, + 9, + 5, + 2 + ], + [ + 258, + 130, + 66, + 33, + 18, + 11, + 7 + ], + [ + 320, + 192, + 33, + 16, + 9, + 5, + 2 + ], + [ + 258, + 130, + 66, + 33, + 18, + 11, + 7 + ] + ], + "targets": [ + 188, + 193, + 199, + 204 + ] + }, + { + "Q": [ + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "1/2", + "0", + "1/2" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "1/2", + "0", + "1/2", + "0" + ], + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2" + ] + ], + "R": [ + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "0", + "1/2" + ], + [ + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2" + ] + ], + "base": 600, + "caps": [ + [ + 257, + 128, + 64, + 32, + 16, + 8, + 5, + 2 + ], + [ + 264, + 128, + 64, + 40, + 16, + 4, + 2, + 1 + ], + [ + 272, + 128, + 80, + 32, + 8, + 4, + 2, + 1 + ], + [ + 257, + 128, + 65, + 33, + 17, + 9, + 5, + 2 + ] + ], + "common": [ + 409, + 80, + 40, + 5, + 2 + ], + "corrections": [ + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407 + ], + "first_correction": 396, + "first_input": 1062, + "helpers": [ + 600, + 601, + 602, + 603, + 604, + 605, + 606, + 607 + ], + "high": [ + 603, + 605, + 606, + 607 + ], + "input_frames": [ + [ + 385, + 72, + 40, + 24, + 5, + 2 + ], + [ + 408, + 80, + 40, + 4, + 2, + 1 + ], + [ + 273, + 136, + 80, + 40, + 5, + 2 + ], + [ + 264, + 145, + 80, + 40, + 5, + 2 + ], + [ + 392, + 65, + 40, + 17, + 5, + 2 + ], + [ + 401, + 80, + 32, + 8, + 5, + 2 + ], + [ + 280, + 129, + 80, + 40, + 5, + 2 + ], + [ + 257, + 152, + 80, + 40, + 5, + 2 + ] + ], + "inputs": [ + 279, + 274, + 295, + 290, + 343, + 338, + 359, + 354 + ], + "low": [ + 600, + 601, + 602, + 604 + ], + "output_entries": [ + 1449, + 1453, + 1452, + 1448 + ], + "profile": { + "1": 32, + "4": 4 + }, + "target_entries": [ + [ + 265, + 128, + 64, + 40, + 16, + 5, + 2 + ], + [ + 265, + 128, + 64, + 40, + 16, + 5, + 2 + ], + [ + 272, + 128, + 80, + 33, + 9, + 5, + 2 + ], + [ + 272, + 128, + 80, + 33, + 9, + 5, + 2 + ] + ], + "targets": [ + 123, + 175, + 183, + 202 + ] + }, + { + "Q": [ + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "1/2", + "0", + "1/2" + ], + [ + "-1/2", + "0", + "0", + "-1/2", + "-1/2", + "0", + "0", + "-1/2" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "1/2", + "0", + "1/2", + "0" + ] + ], + "R": [ + [ + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2" + ], + [ + "0", + "-1/2", + "0", + "1/2" + ] + ], + "base": 608, + "caps": [ + [ + 256, + 128, + 64, + 33, + 16, + 8, + 4, + 3 + ], + [ + 256, + 128, + 65, + 32, + 16, + 8, + 5, + 2 + ], + [ + 256, + 128, + 64, + 32, + 16, + 10, + 6, + 1 + ], + [ + 256, + 128, + 72, + 40, + 16, + 4, + 2, + 1 + ] + ], + "common": [ + 272, + 144, + 75, + 42, + 7 + ], + "corrections": [ + 408, + 409, + 410, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419 + ], + "first_correction": 408, + "first_input": 1070, + "helpers": [ + 608, + 609, + 610, + 611, + 612, + 613, + 614, + 615 + ], + "high": [ + 611, + 613, + 614, + 615 + ], + "input_frames": [ + [ + 266, + 138, + 75, + 42, + 26, + 7 + ], + [ + 272, + 144, + 72, + 41, + 4, + 3 + ], + [ + 264, + 136, + 75, + 42, + 24, + 7 + ], + [ + 272, + 144, + 74, + 42, + 6, + 1 + ], + [ + 257, + 129, + 75, + 42, + 17, + 7 + ], + [ + 272, + 144, + 67, + 34, + 8, + 7 + ], + [ + 259, + 131, + 75, + 42, + 19, + 7 + ], + [ + 272, + 144, + 65, + 32, + 10, + 7 + ] + ], + "inputs": [ + 278, + 276, + 294, + 292, + 358, + 356, + 342, + 340 + ], + "low": [ + 608, + 609, + 610, + 612 + ], + "output_entries": [ + 1484, + 1481, + 1480, + 1485 + ], + "profile": { + "1": 32, + "4": 4 + }, + "target_entries": [ + [ + 256, + 128, + 64, + 33, + 16, + 11, + 7 + ], + [ + 256, + 128, + 73, + 40, + 16, + 5, + 2 + ], + [ + 256, + 128, + 64, + 33, + 16, + 11, + 7 + ], + [ + 256, + 128, + 73, + 40, + 16, + 5, + 2 + ] + ], + "targets": [ + 114, + 121, + 137, + 173 + ] + }, + { + "Q": [ + [ + "0", + "-1/2", + "0", + "-1/2", + "-1", + "0", + "-1", + "0" + ], + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "1", + "1", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2", + "1", + "0", + "0", + "1" + ] + ], + "R": [ + [ + "0", + "-1/2", + "0", + "-1" + ], + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "1" + ] + ], + "base": 624, + "caps": [ + [ + 256, + 129, + 64, + 32, + 17, + 8, + 4, + 2 + ], + [ + 256, + 130, + 64, + 34, + 16, + 8, + 4, + 1 + ], + [ + 256, + 132, + 68, + 32, + 16, + 8, + 2, + 1 + ], + [ + 256, + 129, + 65, + 33, + 17, + 8, + 5, + 3 + ] + ], + "common": [ + 391, + 68, + 34, + 17, + 8 + ], + "corrections": [ + 384, + 385, + 386, + 387, + 388, + 389, + 390, + 391, + 392, + 393, + 394, + 395 + ], + "first_correction": 384, + "first_input": 1086, + "helpers": [ + 624, + 625, + 626, + 627, + 628, + 629, + 630, + 631 + ], + "high": [ + 627, + 629, + 630, + 631 + ], + "input_frames": [ + [ + 261, + 130, + 68, + 34, + 17, + 8 + ], + [ + 258, + 133, + 68, + 34, + 17, + 8 + ], + [ + 390, + 68, + 34, + 16, + 8, + 1 + ], + [ + 385, + 66, + 34, + 17, + 8, + 6 + ], + [ + 262, + 129, + 68, + 34, + 17, + 8 + ], + [ + 257, + 134, + 68, + 34, + 17, + 8 + ], + [ + 389, + 68, + 32, + 17, + 8, + 2 + ], + [ + 386, + 65, + 34, + 17, + 8, + 5 + ] + ], + "inputs": [ + 246, + 244, + 262, + 260, + 360, + 60, + 348, + 350 + ], + "low": [ + 624, + 625, + 626, + 628 + ], + "output_entries": [ + 1549, + 1545, + 1548, + 1544 + ], + "profile": { + "1": 32, + "4": 4 + }, + "target_entries": [ + [ + 256, + 131, + 64, + 34, + 17, + 8, + 4 + ], + [ + 256, + 131, + 64, + 34, + 17, + 8, + 4 + ], + [ + 256, + 132, + 68, + 33, + 17, + 8, + 3 + ], + [ + 256, + 132, + 68, + 33, + 17, + 8, + 3 + ] + ], + "targets": [ + 130, + 151, + 166, + 214 + ] + }, + { + "Q": [ + [ + "-1/2", + "0", + "0", + "-1/2", + "1", + "0", + "0", + "1" + ], + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "-1", + "0", + "-1", + "0" + ], + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "1", + "1", + "0" + ] + ], + "R": [ + [ + "-1/2", + "0", + "0", + "1" + ], + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "0", + "-1" + ], + [ + "0", + "-1/2", + "-1/2", + "0" + ] + ], + "base": 632, + "caps": [ + [ + 256, + 128, + 66, + 32, + 16, + 10, + 4, + 1 + ], + [ + 256, + 128, + 64, + 34, + 18, + 8, + 4, + 1 + ], + [ + 256, + 128, + 64, + 36, + 16, + 12, + 2, + 1 + ], + [ + 256, + 128, + 68, + 32, + 20, + 8, + 2, + 1 + ] + ], + "common": [ + 257, + 129, + 76, + 42, + 30 + ], + "corrections": [ + 372, + 373, + 374, + 375, + 376, + 377, + 378, + 379, + 380, + 381, + 382, + 383 + ], + "first_correction": 372, + "first_input": 1094, + "helpers": [ + 632, + 633, + 634, + 635, + 636, + 637, + 638, + 639 + ], + "high": [ + 635, + 637, + 638, + 639 + ], + "input_frames": [ + [ + 257, + 129, + 72, + 42, + 26, + 4 + ], + [ + 257, + 129, + 76, + 41, + 29, + 3 + ], + [ + 257, + 129, + 69, + 35, + 23, + 9 + ], + [ + 257, + 129, + 66, + 36, + 16, + 14 + ], + [ + 257, + 129, + 67, + 37, + 17, + 15 + ], + [ + 257, + 129, + 68, + 34, + 22, + 8 + ], + [ + 257, + 129, + 76, + 40, + 28, + 2 + ], + [ + 257, + 129, + 73, + 42, + 27, + 5 + ] + ], + "inputs": [ + 456, + 457, + 466, + 467, + 376, + 66, + 396, + 398 + ], + "low": [ + 632, + 633, + 634, + 636 + ], + "output_entries": [ + 1576, + 1577, + 1581, + 1580 + ], + "profile": { + "1": 32, + "4": 4 + }, + "target_entries": [ + [ + 256, + 128, + 70, + 32, + 20, + 10, + 1 + ], + [ + 256, + 128, + 64, + 38, + 18, + 12, + 1 + ], + [ + 256, + 128, + 64, + 38, + 18, + 12, + 1 + ], + [ + 256, + 128, + 70, + 32, + 20, + 10, + 1 + ] + ], + "targets": [ + 144, + 147, + 157, + 160 + ] + }, + { + "Q": [ + [ + "-1/2", + "0", + "-1/2", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "0", + "-1/2", + "-1/2", + "0", + "0", + "1", + "1", + "0" + ], + [ + "-1/2", + "0", + "0", + "-1/2", + "1", + "0", + "0", + "1" + ], + [ + "0", + "-1/2", + "0", + "-1/2", + "-1", + "0", + "-1", + "0" + ] + ], + "R": [ + [ + "-1/2", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "-1/2", + "0" + ], + [ + "-1/2", + "0", + "0", + "1" + ], + [ + "0", + "-1/2", + "0", + "-1" + ] + ], + "base": 640, + "caps": [ + [ + 257, + 128, + 65, + 32, + 16, + 8, + 4, + 2 + ], + [ + 258, + 128, + 64, + 32, + 16, + 10, + 4, + 1 + ], + [ + 260, + 128, + 64, + 32, + 20, + 8, + 2, + 1 + ], + [ + 257, + 128, + 65, + 32, + 17, + 9, + 5, + 3 + ] + ], + "common": [ + 423, + 65, + 20, + 10 + ], + "corrections": [ + 360, + 361, + 362, + 363, + 364, + 365, + 366, + 367, + 368, + 369, + 370, + 371 + ], + "first_correction": 360, + "first_input": 1102, + "helpers": [ + 640, + 641, + 642, + 643, + 644, + 645, + 646, + 647 + ], + "high": [ + 643, + 645, + 646, + 647 + ], + "input_frames": [ + [ + 261, + 130, + 65, + 32, + 20, + 10 + ], + [ + 258, + 133, + 65, + 32, + 20, + 10 + ], + [ + 387, + 65, + 32, + 16, + 10, + 4 + ], + [ + 388, + 65, + 32, + 20, + 9, + 3 + ], + [ + 260, + 131, + 65, + 32, + 20, + 10 + ], + [ + 259, + 132, + 65, + 32, + 20, + 10 + ], + [ + 386, + 65, + 32, + 17, + 10, + 5 + ], + [ + 389, + 65, + 32, + 20, + 8, + 2 + ] + ], + "inputs": [ + 458, + 459, + 464, + 465, + 392, + 97, + 380, + 382 + ], + "low": [ + 640, + 641, + 642, + 644 + ], + "output_entries": [ + 1609, + 1612, + 1608, + 1613 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 257, + 128, + 65, + 32, + 18, + 10, + 6 + ], + [ + 262, + 128, + 64, + 32, + 20, + 10, + 1 + ], + [ + 262, + 128, + 64, + 32, + 20, + 10, + 1 + ], + [ + 257, + 128, + 65, + 32, + 18, + 10, + 6 + ] + ], + "targets": [ + 135, + 146, + 162, + 220 + ] + }, + { + "Q": [ + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ], + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ] + ], + "R": [ + [ + "1", + "0", + "0", + "1" + ], + [ + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1" + ] + ], + "base": 648, + "caps": [ + [ + 288, + 160, + 64, + 16, + 8, + 4, + 2, + 1 + ], + [ + 258, + 130, + 64, + 34, + 18, + 10, + 6, + 1 + ], + [ + 257, + 129, + 65, + 33, + 17, + 8, + 5, + 2 + ], + [ + 257, + 129, + 65, + 33, + 16, + 9, + 4, + 3 + ] + ], + "common": [ + 288, + 160, + 75, + 25, + 7 + ], + "corrections": [ + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 442, + 443 + ], + "first_correction": 432, + "first_input": 1110, + "helpers": [ + 648, + 649, + 650, + 651, + 652, + 653, + 654, + 655 + ], + "high": [ + 651, + 653, + 654, + 655 + ], + "input_frames": [ + [ + 288, + 160, + 67, + 17, + 8, + 7 + ], + [ + 258, + 130, + 75, + 34, + 25, + 7 + ], + [ + 259, + 131, + 75, + 35, + 25, + 7 + ], + [ + 288, + 160, + 66, + 16, + 9, + 7 + ], + [ + 288, + 160, + 72, + 25, + 4, + 3 + ], + [ + 265, + 137, + 75, + 41, + 25, + 7 + ], + [ + 264, + 136, + 75, + 40, + 25, + 7 + ], + [ + 288, + 160, + 73, + 25, + 5, + 2 + ] + ], + "inputs": [ + 248, + 10, + 268, + 270, + 280, + 38, + 300, + 302 + ], + "low": [ + 648, + 649, + 650, + 652 + ], + "output_entries": [ + 1640, + 1644, + 1641, + 1645 + ], + "profile": { + "1": 32, + "4": 4 + }, + "target_entries": [ + [ + 288, + 160, + 64, + 18, + 10, + 6, + 1 + ], + [ + 288, + 160, + 64, + 18, + 10, + 6, + 1 + ], + [ + 257, + 129, + 65, + 33, + 19, + 10, + 7 + ], + [ + 257, + 129, + 65, + 33, + 19, + 10, + 7 + ] + ], + "targets": [ + 187, + 194, + 198, + 205 + ] + }, + { + "Q": [ + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ], + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ] + ], + "R": [ + [ + "1", + "0", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1" + ], + [ + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "1" + ] + ], + "base": 656, + "caps": [ + [ + 256, + 130, + 64, + 32, + 16, + 8, + 6, + 1 + ], + [ + 256, + 136, + 64, + 32, + 24, + 4, + 2, + 1 + ], + [ + 256, + 160, + 96, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 130, + 66, + 34, + 18, + 10, + 6, + 1 + ] + ], + "common": [ + 427, + 96, + 24, + 6 + ], + "corrections": [ + 348, + 349, + 350, + 351, + 352, + 353, + 354, + 355, + 356, + 357, + 358, + 359 + ], + "first_correction": 348, + "first_input": 1118, + "helpers": [ + 656, + 657, + 658, + 659, + 660, + 661, + 662, + 663 + ], + "high": [ + 659, + 661, + 662, + 663 + ], + "input_frames": [ + [ + 296, + 130, + 96, + 24, + 6, + 1 + ], + [ + 258, + 168, + 96, + 24, + 6, + 1 + ], + [ + 418, + 96, + 16, + 8, + 6, + 1 + ], + [ + 392, + 66, + 34, + 24, + 6, + 1 + ], + [ + 290, + 136, + 96, + 24, + 6, + 1 + ], + [ + 264, + 162, + 96, + 24, + 6, + 1 + ], + [ + 424, + 96, + 24, + 4, + 2, + 1 + ], + [ + 386, + 72, + 40, + 24, + 6, + 1 + ] + ], + "inputs": [ + 252, + 254, + 264, + 79, + 296, + 19, + 284, + 286 + ], + "low": [ + 656, + 657, + 658, + 660 + ], + "output_entries": [ + 1673, + 1677, + 1676, + 1672 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 256, + 138, + 64, + 32, + 24, + 6, + 1 + ], + [ + 256, + 138, + 64, + 32, + 24, + 6, + 1 + ], + [ + 256, + 160, + 96, + 18, + 10, + 6, + 1 + ], + [ + 256, + 160, + 96, + 18, + 10, + 6, + 1 + ] + ], + "targets": [ + 141, + 171, + 185, + 196 + ] + }, + { + "Q": [ + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ], + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ], + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ] + ], + "R": [ + [ + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "1", + "0" + ], + [ + "1", + "0", + "0", + "1" + ], + [ + "0", + "1", + "0", + "-1" + ] + ], + "base": 672, + "caps": [ + [ + 257, + 128, + 64, + 32, + 16, + 8, + 4, + 3 + ], + [ + 264, + 128, + 72, + 32, + 16, + 4, + 2, + 1 + ], + [ + 272, + 128, + 64, + 48, + 8, + 4, + 2, + 1 + ], + [ + 257, + 128, + 65, + 33, + 17, + 9, + 4, + 3 + ] + ], + "common": [ + 413, + 72, + 48, + 3 + ], + "corrections": [ + 283, + 284, + 285, + 286, + 287, + 288, + 289, + 290, + 291, + 292, + 293, + 294 + ], + "first_correction": 283, + "first_input": 1134, + "helpers": [ + 672, + 673, + 674, + 675, + 676, + 677, + 678, + 679 + ], + "high": [ + 675, + 677, + 678, + 679 + ], + "input_frames": [ + [ + 280, + 129, + 72, + 48, + 4, + 3 + ], + [ + 257, + 152, + 72, + 48, + 4, + 3 + ], + [ + 393, + 72, + 32, + 16, + 4, + 3 + ], + [ + 400, + 65, + 48, + 9, + 4, + 3 + ], + [ + 272, + 137, + 72, + 48, + 4, + 3 + ], + [ + 265, + 144, + 72, + 48, + 4, + 3 + ], + [ + 385, + 72, + 40, + 24, + 4, + 3 + ], + [ + 408, + 72, + 48, + 4, + 2, + 1 + ] + ], + "inputs": [ + 462, + 463, + 470, + 471, + 328, + 109, + 316, + 318 + ], + "low": [ + 672, + 673, + 674, + 676 + ], + "output_entries": [ + 1740, + 1737, + 1736, + 1741 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 273, + 128, + 64, + 48, + 8, + 4, + 3 + ], + [ + 264, + 128, + 72, + 33, + 17, + 4, + 3 + ], + [ + 273, + 128, + 64, + 48, + 8, + 4, + 3 + ], + [ + 264, + 128, + 72, + 33, + 17, + 4, + 3 + ] + ], + "targets": [ + 117, + 177, + 181, + 208 + ] + }, + { + "Q": [ + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ], + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ] + ], + "R": [ + [ + "0", + "1", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1" + ], + [ + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0" + ] + ], + "base": 680, + "caps": [ + [ + 256, + 129, + 64, + 32, + 16, + 9, + 4, + 2 + ], + [ + 256, + 130, + 66, + 32, + 16, + 8, + 4, + 1 + ], + [ + 256, + 132, + 64, + 36, + 16, + 8, + 2, + 1 + ], + [ + 256, + 129, + 65, + 33, + 16, + 9, + 5, + 3 + ] + ], + "common": [ + 407, + 66, + 36, + 9 + ], + "corrections": [ + 295, + 296, + 297, + 298, + 299, + 300, + 301, + 302, + 303, + 304, + 305, + 306 + ], + "first_correction": 295, + "first_input": 1142, + "helpers": [ + 680, + 681, + 682, + 683, + 684, + 685, + 686, + 687 + ], + "high": [ + 683, + 685, + 686, + 687 + ], + "input_frames": [ + [ + 388, + 65, + 36, + 16, + 9, + 3 + ], + [ + 387, + 66, + 32, + 16, + 9, + 4 + ], + [ + 262, + 129, + 66, + 36, + 16, + 9 + ], + [ + 257, + 134, + 66, + 36, + 16, + 9 + ], + [ + 390, + 66, + 36, + 16, + 8, + 1 + ], + [ + 385, + 66, + 34, + 16, + 9, + 6 + ], + [ + 260, + 131, + 66, + 36, + 16, + 9 + ], + [ + 259, + 132, + 66, + 36, + 16, + 9 + ] + ], + "inputs": [ + 478, + 479, + 490, + 491, + 502, + 503, + 514, + 515 + ], + "low": [ + 680, + 681, + 682, + 684 + ], + "output_entries": [ + 1772, + 1773, + 1768, + 1769 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 256, + 133, + 64, + 36, + 16, + 9, + 2 + ], + [ + 256, + 130, + 66, + 33, + 16, + 9, + 5 + ], + [ + 256, + 133, + 64, + 36, + 16, + 9, + 2 + ], + [ + 256, + 130, + 66, + 33, + 16, + 9, + 5 + ] + ], + "targets": [ + 126, + 153, + 164, + 218 + ] + }, + { + "Q": [ + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ], + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ] + ], + "R": [ + [ + "0", + "1", + "0", + "-1" + ], + [ + "0", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0" + ] + ], + "base": 688, + "caps": [ + [ + 258, + 130, + 64, + 32, + 16, + 8, + 4, + 1 + ], + [ + 258, + 130, + 66, + 34, + 18, + 10, + 4, + 1 + ], + [ + 257, + 129, + 65, + 32, + 17, + 8, + 5, + 3 + ], + [ + 257, + 129, + 64, + 33, + 16, + 9, + 5, + 3 + ] + ], + "common": [ + 258, + 130, + 85, + 45 + ], + "corrections": [ + 319, + 320, + 321, + 322, + 323, + 324, + 325, + 326, + 327, + 328, + 329, + 330 + ], + "first_correction": 319, + "first_input": 1150, + "helpers": [ + 688, + 689, + 690, + 691, + 692, + 693, + 694, + 695 + ], + "high": [ + 691, + 693, + 694, + 695 + ], + "input_frames": [ + [ + 257, + 129, + 76, + 45, + 25, + 3 + ], + [ + 258, + 130, + 72, + 41, + 25, + 4 + ], + [ + 258, + 130, + 70, + 39, + 19, + 10 + ], + [ + 258, + 130, + 65, + 32, + 20, + 13 + ], + [ + 258, + 130, + 68, + 37, + 17, + 8 + ], + [ + 258, + 130, + 67, + 34, + 22, + 15 + ], + [ + 258, + 130, + 76, + 44, + 24, + 1 + ], + [ + 258, + 130, + 74, + 43, + 25, + 6 + ] + ], + "inputs": [ + 480, + 481, + 492, + 493, + 516, + 517, + 504, + 505 + ], + "low": [ + 688, + 689, + 690, + 692 + ], + "output_entries": [ + 1805, + 1804, + 1800, + 1801 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 258, + 130, + 64, + 33, + 16, + 9, + 5 + ], + [ + 258, + 130, + 66, + 35, + 18, + 11, + 5 + ], + [ + 258, + 130, + 66, + 35, + 18, + 11, + 5 + ], + [ + 258, + 130, + 64, + 33, + 16, + 9, + 5 + ] + ], + "targets": [ + 155, + 190, + 211, + 216 + ] + }, + { + "Q": [ + [ + "0", + "1", + "1", + "0", + "0", + "1", + "1", + "0" + ], + [ + "0", + "1", + "0", + "1", + "-1", + "0", + "-1", + "0" + ], + [ + "1", + "0", + "0", + "1", + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0", + "0", + "-1", + "0", + "-1" + ] + ], + "R": [ + [ + "0", + "1", + "1", + "0" + ], + [ + "0", + "1", + "0", + "-1" + ], + [ + "1", + "0", + "0", + "1" + ], + [ + "1", + "0", + "1", + "0" + ] + ], + "base": 696, + "caps": [ + [ + 257, + 128, + 64, + 33, + 16, + 8, + 4, + 2 + ], + [ + 258, + 128, + 64, + 32, + 18, + 8, + 4, + 1 + ], + [ + 260, + 128, + 64, + 32, + 16, + 12, + 2, + 1 + ], + [ + 257, + 128, + 64, + 33, + 17, + 9, + 5, + 3 + ] + ], + "common": [ + 455, + 33, + 18, + 12 + ], + "corrections": [ + 307, + 308, + 309, + 310, + 311, + 312, + 313, + 314, + 315, + 316, + 317, + 318 + ], + "first_correction": 307, + "first_input": 1158, + "helpers": [ + 696, + 697, + 698, + 699, + 700, + 701, + 702, + 703 + ], + "high": [ + 699, + 701, + 702, + 703 + ], + "input_frames": [ + [ + 388, + 67, + 33, + 18, + 12 + ], + [ + 451, + 33, + 18, + 8, + 4 + ], + [ + 385, + 70, + 33, + 18, + 12 + ], + [ + 454, + 32, + 18, + 12, + 1 + ], + [ + 262, + 193, + 33, + 18, + 12 + ], + [ + 321, + 134, + 33, + 18, + 12 + ], + [ + 259, + 196, + 33, + 18, + 12 + ], + [ + 324, + 131, + 33, + 18, + 12 + ] + ], + "inputs": [ + 482, + 483, + 506, + 507, + 518, + 519, + 494, + 495 + ], + "low": [ + 696, + 697, + 698, + 700 + ], + "output_entries": [ + 1836, + 1837, + 1832, + 1833 + ], + "profile": { + "1": 24, + "2": 8, + "3": 4 + }, + "target_entries": [ + [ + 261, + 128, + 64, + 33, + 16, + 12, + 2 + ], + [ + 258, + 128, + 64, + 33, + 18, + 9, + 5 + ], + [ + 261, + 128, + 64, + 33, + 16, + 12, + 2 + ], + [ + 258, + 128, + 64, + 33, + 18, + 9, + 5 + ] + ], + "targets": [ + 133, + 149, + 159, + 222 + ] + } + ], + "boundary": { + "B_cut": 1054, + "deferred_corrections": [ + 283, + 284, + 285, + 286, + 287, + 288, + 289, + 290, + 291, + 292, + 293, + 294, + 295, + 296, + 297, + 298, + 299, + 300, + 301, + 302, + 303, + 304, + 305, + 306, + 307, + 308, + 309, + 310, + 311, + 312, + 313, + 314, + 315, + 316, + 317, + 318, + 319, + 320, + 321, + 322, + 323, + 324, + 325, + 326, + 327, + 328, + 329, + 330, + 348, + 349, + 350, + 351, + 352, + 353, + 354, + 355, + 356, + 357, + 358, + 359, + 360, + 361, + 362, + 363, + 364, + 365, + 366, + 367, + 368, + 369, + 370, + 371, + 372, + 373, + 374, + 375, + 376, + 377, + 378, + 379, + 380, + 381, + 382, + 383, + 384, + 385, + 386, + 387, + 388, + 389, + 390, + 391, + 392, + 393, + 394, + 395, + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407, + 408, + 409, + 410, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431, + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 442, + 443 + ], + "independent_coordinates": 192, + "main_arrays": 704, + "prefix_determinant": "-2475880078570760549798248448", + "prefix_gates": 4537, + "registers": [ + 10, + 19, + 38, + 48, + 60, + 66, + 67, + 79, + 82, + 97, + 100, + 109, + 244, + 246, + 248, + 252, + 254, + 260, + 262, + 264, + 268, + 270, + 274, + 276, + 278, + 279, + 280, + 283, + 284, + 286, + 290, + 292, + 294, + 295, + 296, + 300, + 302, + 315, + 316, + 318, + 328, + 338, + 340, + 342, + 343, + 347, + 348, + 350, + 354, + 356, + 358, + 359, + 360, + 376, + 379, + 380, + 382, + 392, + 396, + 398, + 456, + 457, + 458, + 459, + 462, + 463, + 464, + 465, + 466, + 467, + 470, + 471, + 478, + 479, + 480, + 481, + 482, + 483, + 490, + 491, + 492, + 493, + 494, + 495, + 502, + 503, + 504, + 505, + 506, + 507, + 514, + 515, + 516, + 517, + 518, + 519, + 592, + 593, + 594, + 595, + 596, + 597, + 598, + 599, + 600, + 601, + 602, + 603, + 604, + 605, + 606, + 607, + 608, + 609, + 610, + 611, + 612, + 613, + 614, + 615, + 624, + 625, + 626, + 627, + 628, + 629, + 630, + 631, + 632, + 633, + 634, + 635, + 636, + 637, + 638, + 639, + 640, + 641, + 642, + 643, + 644, + 645, + 646, + 647, + 648, + 649, + 650, + 651, + 652, + 653, + 654, + 655, + 656, + 657, + 658, + 659, + 660, + 661, + 662, + 663, + 672, + 673, + 674, + 675, + 676, + 677, + 678, + 679, + 680, + 681, + 682, + 683, + 684, + 685, + 686, + 687, + 688, + 689, + 690, + 691, + 692, + 693, + 694, + 695, + 696, + 697, + 698, + 699, + 700, + 701, + 702, + 703 + ] + }, + "controls": [ + "foreign_equal_input", + "high_information_can_escape", + "shared_output_cap", + "early_output_access", + "two_global_readers_for_kernel", + "zero_output_column", + "asynchronous_input_mutation", + "noncommuting_deferred_correction", + "singular_prefix", + "unpaid_helper_restoration" + ], + "global": { + "foreign_high_tests": 1056, + "input_pairs": 4560, + "input_target_tests": 4608, + "kernel_frames": [ + { + "contained_inputs": [ + 283, + 315, + 82, + 67 + ], + "eligible_targets": [ + 193 + ], + "frame": [ + 258, + 130, + 66, + 32, + 18, + 12, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 283, + 48, + 82, + 379 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 66, + 32, + 19, + 8, + 5 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 283, + 100, + 347, + 82 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 66, + 32, + 19, + 9, + 4 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 100, + 48, + 347, + 379 + ], + "eligible_targets": [ + 204 + ], + "frame": [ + 258, + 130, + 66, + 33, + 18, + 8, + 4 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 315, + 48, + 379, + 67 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 66, + 36, + 22, + 8, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 100, + 315, + 347, + 67 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 66, + 40, + 26, + 4, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 347, + 82, + 379, + 67 + ], + "eligible_targets": [], + "frame": [ + 259, + 131, + 67, + 32, + 19, + 8, + 5 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 100, + 48, + 82, + 67 + ], + "eligible_targets": [], + "frame": [ + 259, + 131, + 67, + 32, + 19, + 9, + 4 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 283, + 48, + 347, + 67 + ], + "eligible_targets": [ + 199 + ], + "frame": [ + 259, + 131, + 67, + 33, + 18, + 9, + 5 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 283, + 315, + 347, + 379 + ], + "eligible_targets": [], + "frame": [ + 262, + 134, + 70, + 36, + 22, + 8, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 283, + 100, + 315, + 48 + ], + "eligible_targets": [], + "frame": [ + 266, + 138, + 74, + 40, + 26, + 4, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 100, + 315, + 82, + 379 + ], + "eligible_targets": [ + 188 + ], + "frame": [ + 320, + 192, + 32, + 18, + 8, + 4, + 1 + ], + "owner": 592 + }, + { + "contained_inputs": [ + 482, + 483, + 518, + 519 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 67, + 33, + 18, + 8, + 4 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 506, + 507, + 494, + 495 + ], + "eligible_targets": [], + "frame": [ + 258, + 130, + 70, + 32, + 18, + 12, + 1 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 483, + 506, + 518, + 495 + ], + "eligible_targets": [], + "frame": [ + 258, + 131, + 66, + 33, + 18, + 8, + 4 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 482, + 506, + 519, + 495 + ], + "eligible_targets": [ + 222 + ], + "frame": [ + 258, + 131, + 67, + 33, + 18, + 9, + 5 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 482, + 507, + 519, + 494 + ], + "eligible_targets": [], + "frame": [ + 258, + 134, + 66, + 32, + 18, + 12, + 1 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 483, + 507, + 518, + 494 + ], + "eligible_targets": [ + 149 + ], + "frame": [ + 258, + 192, + 32, + 18, + 8, + 4, + 1 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 483, + 506, + 519, + 494 + ], + "eligible_targets": [ + 133 + ], + "frame": [ + 259, + 130, + 66, + 33, + 18, + 8, + 4 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 482, + 506, + 518, + 494 + ], + "eligible_targets": [], + "frame": [ + 259, + 130, + 67, + 33, + 18, + 9, + 5 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 518, + 519, + 494, + 495 + ], + "eligible_targets": [], + "frame": [ + 259, + 131, + 66, + 33, + 18, + 9, + 5 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 482, + 507, + 518, + 495 + ], + "eligible_targets": [ + 159 + ], + "frame": [ + 262, + 130, + 66, + 32, + 18, + 12, + 1 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 483, + 507, + 519, + 495 + ], + "eligible_targets": [], + "frame": [ + 320, + 130, + 32, + 18, + 8, + 4, + 1 + ], + "owner": 696 + }, + { + "contained_inputs": [ + 482, + 483, + 506, + 507 + ], + "eligible_targets": [], + "frame": [ + 384, + 66, + 32, + 18, + 8, + 4, + 1 + ], + "owner": 696 + } + ] + }, + "local": [ + { + "kernels": [ + [ + 258, + 130, + 66, + 32, + 18, + 12, + 1 + ], + [ + 258, + 130, + 66, + 32, + 19, + 8, + 5 + ], + [ + 258, + 130, + 66, + 32, + 19, + 9, + 4 + ], + [ + 258, + 130, + 66, + 33, + 18, + 8, + 4 + ], + [ + 258, + 130, + 66, + 36, + 22, + 8, + 1 + ], + [ + 258, + 130, + 66, + 40, + 26, + 4, + 1 + ], + [ + 259, + 131, + 67, + 32, + 19, + 8, + 5 + ], + [ + 259, + 131, + 67, + 32, + 19, + 9, + 4 + ], + [ + 259, + 131, + 67, + 33, + 18, + 9, + 5 + ], + [ + 262, + 134, + 70, + 36, + 22, + 8, + 1 + ], + [ + 266, + 138, + 74, + 40, + 26, + 4, + 1 + ], + [ + 320, + 192, + 32, + 18, + 8, + 4, + 1 + ] + ], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 5, + 1, + 8 + ], + [ + 2, + 6, + 2, + 28 + ], + [ + 3, + 7, + 3, + 56 + ], + [ + 4, + 7, + 3, + 12 + ], + [ + 4, + 7, + 4, + 2 + ], + [ + 4, + 8, + 4, + 56 + ], + [ + 5, + 8, + 4, + 56 + ], + [ + 6, + 8, + 4, + 28 + ], + [ + 7, + 8, + 4, + 8 + ], + [ + 8, + 8, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 6, + 1, + 8 + ], + [ + 2, + 7, + 2, + 28 + ], + [ + 3, + 8, + 3, + 56 + ], + [ + 4, + 8, + 3, + 12 + ], + [ + 4, + 8, + 4, + 2 + ], + [ + 4, + 9, + 4, + 56 + ], + [ + 5, + 9, + 4, + 56 + ], + [ + 6, + 9, + 4, + 28 + ], + [ + 7, + 9, + 4, + 8 + ], + [ + 8, + 9, + 4, + 1 + ] + ] + }, + { + "kernels": [ + [ + 258, + 130, + 67, + 33, + 18, + 8, + 4 + ], + [ + 258, + 130, + 70, + 32, + 18, + 12, + 1 + ], + [ + 258, + 131, + 66, + 33, + 18, + 8, + 4 + ], + [ + 258, + 131, + 67, + 33, + 18, + 9, + 5 + ], + [ + 258, + 134, + 66, + 32, + 18, + 12, + 1 + ], + [ + 258, + 192, + 32, + 18, + 8, + 4, + 1 + ], + [ + 259, + 130, + 66, + 33, + 18, + 8, + 4 + ], + [ + 259, + 130, + 67, + 33, + 18, + 9, + 5 + ], + [ + 259, + 131, + 66, + 33, + 18, + 9, + 5 + ], + [ + 262, + 130, + 66, + 32, + 18, + 12, + 1 + ], + [ + 320, + 130, + 32, + 18, + 8, + 4, + 1 + ], + [ + 384, + 66, + 32, + 18, + 8, + 4, + 1 + ] + ], + "projections": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 28 + ], + [ + 3, + 3, + 56 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 58 + ] + ], + "spectrum": [ + [ + 1, + 5, + 1, + 8 + ], + [ + 2, + 6, + 2, + 28 + ], + [ + 3, + 7, + 3, + 56 + ], + [ + 4, + 7, + 3, + 12 + ], + [ + 4, + 7, + 4, + 2 + ], + [ + 4, + 8, + 4, + 56 + ], + [ + 5, + 8, + 4, + 56 + ], + [ + 6, + 8, + 4, + 28 + ], + [ + 7, + 8, + 4, + 8 + ], + [ + 8, + 8, + 4, + 1 + ] + ] + } + ], + "profile": { + "1": 328, + "2": 56, + "3": 28, + "4": 20 + }, + "schema_version": 1, + "source_payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c", + "status": "PASS_CROSS_BLOCK_LOCALITY_PREMISES" +} diff --git a/research/complex-cross-block-locality/INDEPENDENT.json b/research/complex-cross-block-locality/INDEPENDENT.json new file mode 100644 index 0000000000..af0c302eb9 --- /dev/null +++ b/research/complex-cross-block-locality/INDEPENDENT.json @@ -0,0 +1,411 @@ +{ + "boundary_controls": 2, + "boundary_witnesses": [ + { + "pivot_columns": [ + 8, + 15, + 12, + 32, + 19, + 14, + 3, + 2, + 1, + 5, + 26, + 23, + 10, + 11, + 4, + 22, + 33, + 24, + 9, + 25, + 31, + 241, + 17, + 35, + 41, + 38, + 45, + 18, + 44, + 13, + 29, + 39, + 61, + 274, + 54, + 16, + 279, + 272, + 43, + 68, + 52, + 6, + 28, + 58, + 257, + 30, + 70, + 259, + 73, + 59, + 243, + 338, + 280, + 64, + 336, + 49, + 290, + 304, + 294, + 370, + 244, + 248, + 295, + 322, + 354, + 359, + 260, + 264, + 310, + 306, + 342, + 386, + 343, + 344, + 347, + 358, + 66, + 62, + 296, + 391, + 360, + 390, + 288, + 297, + 283, + 313, + 368, + 417, + 276, + 308, + 392, + 401, + 278, + 328, + 281, + 320, + 592, + 593, + 594, + 595, + 596, + 597, + 598, + 599, + 600, + 601, + 602, + 603, + 604, + 605, + 606, + 607, + 608, + 609, + 610, + 611, + 612, + 613, + 614, + 615, + 624, + 625, + 626, + 627, + 628, + 629, + 630, + 631, + 632, + 633, + 634, + 635, + 636, + 637, + 638, + 639, + 640, + 641, + 642, + 643, + 644, + 645, + 646, + 647, + 648, + 649, + 650, + 651, + 652, + 653, + 654, + 655, + 656, + 657, + 658, + 659, + 660, + 661, + 662, + 663, + 672, + 673, + 674, + 675, + 676, + 677, + 678, + 679, + 680, + 681, + 682, + 683, + 684, + 685, + 686, + 687, + 688, + 689, + 690, + 691, + 692, + 693, + 694, + 695, + 696, + 697, + 698, + 699, + 700, + 701, + 702, + 703 + ], + "pivot_product_mod_prime": 2184, + "prime": 65521, + "rank": 192 + }, + { + "pivot_columns": [ + 8, + 15, + 12, + 32, + 19, + 14, + 3, + 2, + 1, + 5, + 26, + 23, + 10, + 11, + 4, + 22, + 33, + 24, + 9, + 25, + 31, + 241, + 17, + 35, + 41, + 38, + 45, + 18, + 44, + 13, + 29, + 39, + 61, + 274, + 54, + 16, + 279, + 272, + 43, + 68, + 52, + 6, + 28, + 58, + 257, + 30, + 70, + 259, + 73, + 59, + 243, + 338, + 280, + 64, + 336, + 49, + 290, + 304, + 294, + 370, + 244, + 248, + 295, + 322, + 354, + 359, + 260, + 264, + 310, + 306, + 342, + 386, + 343, + 344, + 347, + 358, + 66, + 62, + 296, + 391, + 360, + 390, + 288, + 297, + 283, + 313, + 368, + 417, + 276, + 308, + 392, + 401, + 278, + 328, + 281, + 320, + 592, + 593, + 594, + 595, + 596, + 597, + 598, + 599, + 600, + 601, + 602, + 603, + 604, + 605, + 606, + 607, + 608, + 609, + 610, + 611, + 612, + 613, + 614, + 615, + 624, + 625, + 626, + 627, + 628, + 629, + 630, + 631, + 632, + 633, + 634, + 635, + 636, + 637, + 638, + 639, + 640, + 641, + 642, + 643, + 644, + 645, + 646, + 647, + 648, + 649, + 650, + 651, + 652, + 653, + 654, + 655, + 656, + 657, + 658, + 659, + 660, + 661, + 662, + 663, + 672, + 673, + 674, + 675, + 676, + 677, + 678, + 679, + 680, + 681, + 682, + 683, + 684, + 685, + 686, + 687, + 688, + 689, + 690, + 691, + 692, + 693, + 694, + 695, + 696, + 697, + 698, + 699, + 700, + 701, + 702, + 703 + ], + "pivot_product_mod_prime": 32769, + "prime": 65537, + "rank": 192 + } + ], + "foreign_high_tests": 1056, + "input_pairs": 4560, + "input_target_tests": 4608, + "kernel_frames": 24, + "literal_columns": 240, + "source_payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c", + "status": "PASS_INDEPENDENT_CROSS_BLOCK_PREMISES", + "subset_cases": 3060 +} diff --git a/research/complex-cross-block-locality/NOTICE.md b/research/complex-cross-block-locality/NOTICE.md new file mode 100644 index 0000000000..021925a7a8 --- /dev/null +++ b/research/complex-cross-block-locality/NOTICE.md @@ -0,0 +1,15 @@ +# Attribution + +New material: Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance, +2026. Licensed under the repository's Apache License 2.0. + +The block extraction in `verify.py` is adapted from Ali Romman's +`research/complex-block-rank-optimum/verify.py`, PR1429 at +`591582004d82302268da3b264a6ba5edec1521de`, Apache-2.0. The proof reuses his +carrier-count and early-retirement arguments with the attribution in +`PROOF.md`; it adds the simultaneous boundary and global localization needed +for cross-block mixing. The original predecessor is not overwritten. + +The selected source archive is consumed intact. Its original notices, +licenses and authorship remain in that archive and the source packages. +No ownership of their supplier constructions or previous bounds is claimed. diff --git a/research/complex-cross-block-locality/PROOF.md b/research/complex-cross-block-locality/PROOF.md new file mode 100644 index 0000000000..3477ffabdd --- /dev/null +++ b/research/complex-cross-block-locality/PROOF.md @@ -0,0 +1,270 @@ +# Cross-block mixing at the twelve frozen late interfaces + +The source is the selected PR1094 local word, retained in the PR1042 replay +archive. Ali Romman's PR1429 proves a moment minimum separately for twelve +eight-helper blocks and explicitly excludes communication between blocks. +This note removes that exclusion for the **joint fixed late interface** below. +It uses PR1429's carrier-count and retirement arguments, adding global +localization and a simultaneous boundary. It does not claim a new supplier. + +## Statement and exact scope + +Let `0 < s < 1`. A frame growth of rank `d` costs `d^s`. At the joint +interface, there are 96 helpers, 96 independent read-only input values, +and 48 additive output ports, all of the retained equal array volume. +The helpers are those in the twelve blocks with bases + +``` +592, 600, 608, 624, 632, 640, 648, 656, 672, 680, 688, 696. +``` + +Block `j` has four initial helpers at its common frame `U_j`, of rank +`u_j = 4` or `5`, and four initially at rank one. Write their independent +initial values as `x_j` and `y_j`. Input `z_ji` is available at its fixed +frame `F_ji`, of rank five or six. The required four-port increment is +`R_j y_j + Q_j z_j`, with no `x_j` response. The matrices and every frame +are extracted from the word, rather than stipulated from an aggregate bill. +Each output has the retained late entry frame `G_t` and final hyperplane +`H_t`. Every helper must end at the full rank-nine frame with its dirty +information retained. We relax its endpoint to any invertible helper map. + +Allow any finite rational ADD/SCALE program on **all 96 helpers**, including +cross-block mixing, arbitrary order, arbitrary nonzero scaling, repeated +reads of a fixed input port, repeated additive writes to the output ports, +and assignment of an input to a helper from a different original block. +Input reads add into helpers; output writes add from helpers into targets. +Every interaction requires a common frame in F2^9; frames only grow by inclusion. +All helper growth, including completion to rank nine, is charged. + +There are no extra arrays, frame descents, writable input ports, target +scratch, additional later versions of an input port, earlier target access, +changed centre paths, or changes to the exterior program. In particular, +the physical input arrays undergo later exterior updates; granting repeated +access to their **fixed early values** is a relaxation of this port interface, +not permission to read their later updated values as additional inputs. +This distinction is material. + +**Theorem.** Every such joint replacement has helper-growth cost at least + +``` +328 + 56*2^s + 28*3^s + 20*4^s. +``` + +The retained twelve blocks attain equality. Thus arbitrary cross-block +coding cannot improve this cost with the declared interfaces. This is an +all-length written argument; the executable checks establish its finite +source premises. It is not a proof-assistant theorem or a global circuit +lower bound. + +## 1. One genuine joint boundary + +The earliest retained correction starts at zero-based B index 283. All +96 helpers already have their stated initial frames there. From each +block's correction start until its input segment, only that block's own +helper-only correction touches its helpers. The 144 correction ADDs +therefore commute past all intervening exterior operations and can be +deferred to immediately before B index 1054, the first selected input. +No input value or helper value is copied for this rearrangement. + +At index 1054, all 96 distinct input arrays are already at their stated +frames. None changes before its own input segment. The 96 helper arrays +are distinct from these inputs and from the 48 targets. Removing the +corrections leaves a prefix of 4537 scalar operations on the 704 main +arrays. Every ADD has distinct source and destination, and every SCALE +is nonzero. The copied-centre contribution here is its retained main-array +shear. This prefix is invertible; its determinant is the checked nonzero +product of SCALE factors. Hence any 192 distinct coordinates at this +boundary are independent under the retained arbitrary-main-input contract. + +As a separate check, `independent.py` executes the prefix over each of +the primes 65521 and 65537 and exhibits 192 pivot columns. All rational +denominators are invertible modulo each prime. Either nonzero minor alone +certifies rational independence; these are exact witnesses, not a +probabilistic rank estimate. Duplicate-coordinate and singular-prefix +controls reduce the witnessed rank to 191. + +Allowing all fixed inputs from the outset and all targets at their late +entry frames removes timing restrictions and only enlarges the replacement +class. The theorem can therefore use this common abstract boundary. It +does not silently assume asynchronous values to be independent. + +## 2. Checked local and global premises + +For every block, `Q_j` has rank four and each of its eight columns has +exactly two nonzero entries at distinct output ports. For every set `S` +of at most four input coordinates, + +``` +rank(projection_S ker(Q_j)) + = |S| - 4 + rank(Q_j on the complementary columns) + >= ceil(3|S|/4). +``` + +All 255 nonempty supports per block are checked. A nonzero local kernel +vector cannot have input-frame union of rank at most six. There are +exactly 24 distinct rank-seven kernel frames, twelve each in blocks +592 and 696; these are all such frames, not sampled examples. + +The new global checks establish: + +1. The 96 input frames form an antichain: none contains another. +2. `U_j` is contained in no input frame of another block (1056 tests). +3. The 48 target caps are distinct, and every input frame joined with + every target entry frame has rank at least eight (4608 tests). +4. Each rank-seven kernel frame contains input frames from its own block + only, all of rank five, and is contained in at most one of the **48** + target caps. Previously the corresponding target check was local. + +Because output ports are disjoint, the complete input response is +`Q = diag(Q_j)`. If a nonzero vector in `ker(Q)` is supported on input +frames contained in a frame `E` of rank at most seven, one of its nonzero +block components is a local kernel vector. The local support result +forces that component's union to have rank seven, and hence to equal `E`. +Premise 4 then forces all supported inputs to belong to that same block. +Consequently every such global kernel is local, all contained inputs +have rank five, and `E` reaches at most one global output. This argument +covers every support in 96 coordinates without a finite-support cutoff. + +The two implementations use rational elimination versus integer Gram +principal minors, and binary pivot bases versus explicit sets. They +reproduce all 3060 subset cases and the global premises. + +## 3. Input barrier and high-information confinement + +Every input must be read because its required output column is nonzero. +A helper cannot read two incomparable fixed input frames while its own +frame grows. There are exactly 96 helpers and 96 required inputs, so the +input-to-helper assignment is a bijection. + +An already-read helper cannot mix with an unread one: their common frame +would have to contain the first helper's input frame and fit inside the +second helper's incomparable future input frame. After two read helpers +mix, both exceed their individual input frames and cannot read again. +A target read also prevents a subsequent input read. A helper cannot +write an output before its assigned input, as that would leave one input +without a reader. Moving operations on disjoint helpers past one another +therefore gives a barrier after all input reads and before post-input +mixing. Repeated reads and scaling combine to one nonzero coefficient +per input. In input order the barrier values are + +``` +h = P(y,x) + D z, +``` + +where `P` is invertible and `D` is invertible diagonal. This uses the +192 independent boundary coordinates established above. + +Each initial high value `x_j` starts at `U_j`. Any physical route for its +information retains that subspace. A helper that ever receives this +information must eventually read an input whose frame contains `U_j`. +By global premise 2, that input belongs to block `j`. The original four +high helpers of block `j` are also confined to its eight input slots. +No high helper from another block can occupy those slots. They thus +contain exactly four original high helpers and four rank-one helpers, +although the latter may have migrated from other blocks. + +All columns of `P` belonging to `x_j` are supported on those eight rows, +have rank four by invertibility, and are annihilated by `Q_j D_j^-1`, +since high dirty input has zero output response. Their scaled column +space is exactly `ker(Q_j)`. The same local projection lower bounds +therefore hold after arbitrary cross-block pre-input mixing. The labels +of the four low helpers do not matter for these bounds. + +## 4. Complete pre-input cost + +For positive growth increments and `0= (sum d_i)^s`. + +If `u_j=5`, all eight input ranks are six. Every low helper needs a +nonzero `x_j` coefficient by the singleton projection bound. It must +visit `U_j`: pre-input mixing between two distinct future input slots +has rank at most five. The pre-input cost is at least `4*4^s + 8`. + +If `u_j=4`, let `S` be the low helpers that first receive `x_j` +information at rank five, and put `k=|S|`. They must have rank-six input +slots; rank-five slots cannot meet another slot at their own frame. +Relative to `1 -> 4 -> 6`, each can save at most + +``` +A(s) = 3^s + 2^s - 4^s - 1. +``` + +Their independent `x_j` directions must arrive through carriers that +already possess such information at rank four and then enter rank five. +A carrier cannot return to rank four; later mixing inside rank five +does not supply an additional independent direction. Hence there are +at least `ceil(3k/4)` distinct carriers, by the projection bound. +Confinement keeps every such carrier in this same group. Each carrier +has a rank-six input and a paid `4 -> 5 -> 6` path, and is not in `S`. +Relative to direct `4 -> 6`, its excess is at least `B(s)=2-2^s`. + +The inequality `4 A(s) < 3 B(s)` for `0 0` for `18` and `243<256` give `3/20` on `[1,2]`, +whereas `f'(2)=9-6p<0`. So `f` is decreasing there and exceeds `f(2)=0`. + +Writing `n_5+n_6=8` for the input rank counts, the pre-input cost is +therefore at least `4*3^s + n_5 + n_6*2^s`. + +## 5. Complete post-input cost, including early retirement + +Treat all 96 barrier helper values as independent inputs. Their required +output matrix is `Q D^-1`. Every output write requires rank at least +eight by global premise 3. A helper must mix with another helper before +first reaching rank eight. Otherwise its injected variable, still unique +to that helper, could reach at most one of the distinct target caps, +contrary to its two required outputs. This first mixing strictly exceeds +its incomparable input frame. + +Now consider any helper jumping from rank at most seven to its final +rank nine. Put a nonzero perturbation in that helper just before the jump, +with all other current helper and output perturbations zero, and reverse +the executed post-input program. Monotone common-frame interactions keep +every reachable barrier input frame inside the retiring frame `E`. +No earlier target output can respond, since every output write has rank +at least eight. After the jump, no later output cap can be reached either. +The nonzero barrier perturbation is therefore in `ker(Q D^-1)`. + +Diagonal scaling does not change supports. Section 2 forces `E` to have +rank seven, to contain only rank-five input frames, and to reach at most +one target. The retiring helper must also have mixed at rank six earlier: +if its first mixing were at rank seven, all routes for its initially +unique injected variable would contain `E` and reach at most one target. +Its path thus includes `5 -> 6 -> 7 -> 9`, costing at least `2+2^s`. +This argument allows previous output writes, information splitting and +mixing with every other block; it is not merely a final-kernel test. + +A rank-five input helper that does visit rank eight also costs at least +`2+2^s`, including its first mixing and final restoration. A rank-six +input helper cannot retire below rank eight, since its own input frame +would be contained in `E`. Its path includes `6 -> 7 -> 8 -> 9`, costing +at least three. The complete post-input cost is at least +`n_5*(2+2^s) + 3*n_6`. + +## 6. Attainment and supplier accounting + +Adding the two parts gives `24+8*2^s+4*3^s` per rank-four group and +`32+4*4^s` per rank-five group. The selected word has seven of the former +and five of the latter, giving the stated bound. Both checkers recount +the literal paths, including completion to full rank, and obtain exactly +`{1:328, 2:56, 3:28, 4:20}`. The original unmixed word is an attaining +member of the enlarged class. There is no proposed replacement to admit. + +With the remaining paid profile, role inventory, copied centres, source +ports, target paths, owner map and recurrence held fixed, this lower bound +applies pointwise at `s=1-a` in the complete supplier moment. For each +call, the unchanged exterior contribution plus this minimum is the +original numerator; extra accesses, wrappers, frames or restoration are +nonnegative charges. Multiplication by the unchanged positive call counts +and division by the unchanged normalization preserve the inequality. +The admissible moment region cannot increase by this mechanism. + +This does not assert an optimum for scalar primitive counts or constant +compiler allowances. The one-canonical-word orientation convention and +all-size/compiler, common-label/mutable-source, hosting, precision/tape, +exact recovery and analytic interfaces remain inherited. No new kappa, +native admission, full cold replay, hosted CI or unconditional multiplication +theorem is claimed. Extra helpers, altered source/target availability, +additional versions of the input ports, frame descents and changed +centres remain outside the result. diff --git a/research/complex-cross-block-locality/README.md b/research/complex-cross-block-locality/README.md new file mode 100644 index 0000000000..c5ffd4ae09 --- /dev/null +++ b/research/complex-cross-block-locality/README.md @@ -0,0 +1,146 @@ +# Cross-block mixing retains the fixed late-interface moment floor + +**Scoped negative result; no new kappa.** Allowing all twelve late complex +blocks to mix their helpers does not reduce their complete helper-growth +moment under the retained fixed-port, monotone-frame contract. This closes +one specific exclusion in Ali Romman's [PR1429](https://github.com/CrocSwap/integer-mult-bounds/pull/1429). +It does not exclude new source versions, earlier output access, extra helpers, +frame descents or changed centres. + +For every `0 < s < 1`, the exact minimum for the 96 helpers is + +``` +328 + 56*2^s + 28*3^s + 20*4^s. +``` + +The original selected local word attains this value, from the declared late +entries through completion of every helper to rank nine. Arbitrary finite +rational helper programs, +input reassignment and repeated fixed-port reads are permitted. Source and +target interfaces, centre paths and the exterior program are held fixed; +all extra charges are nonnegative. The result concerns recursive rank cost, +not a global scalar-operation optimum or a new multiplication theorem. + +## What is new + +PR1429 already establishes the per-block floor. Its proof explicitly leaves +cross-block communication outside scope. Here the exact source geometry +confines each high dirty input to its original eight input slots even when +low helpers migrate. Every rank-seven cancellation frame is also confined +to one block and can reach at most one of all 48 outputs. These global +premises let the carrier and retirement arguments survive arbitrary mixing +of the 96 helpers. The [proof](PROOF.md) supplies the all-length argument. + +The actual word admits a common boundary before B index 1054 after +deferring 144 commuting correction ADDs. Its 192 source/helper coordinates +are independent. A separate modular replay supplies full-rank witnesses +over two checked primes, so the argument does not assume independence of +arbitrarily chosen asynchronous snapshots. + +| Finite evidence | Completed coverage | +| --- | ---: | +| Block support cases, rational ranks and binary spans | 3060 | +| Distinct input-frame pairs | 4560 | +| Foreign high-frame/input tests | 1056 | +| Input-frame/target-entry tests | 4608 | +| Rank-seven cancellation frames | 24 | +| Literal scalar input columns across the twelve blocks | 240 | +| Joint boundary rank, independently checked modulo two primes | 192 | +| Primary semantic rejection controls / independent boundary controls | 10 / 2 | + +The primary checker uses rational elimination and binary pivot bases. The +separate implementation imports none of it and uses integer Gram minors, +explicit subspace sets, single-column scalar execution and modular prefix +replay. Both implementations were written by the same AI-assisted author; +this is algorithmic crosschecking, not independent human review. The finite +checks establish the proof's source premises, not a formal theorem about +every possible multiplication algorithm. + +## Reproduce + +From the repository root, Python 3.12 and its standard library: + +```sh +python3.12 scripts/research_package.py --package research/complex-cross-block-locality +``` + +Expected final line: + +``` +PASS_REGISTERED_RESEARCH_PACKAGE research/complex-cross-block-locality outcome=negative-result +``` + +The command checks exact Git/SHA256 source pins, both deterministic receipts, +semantic controls, and package corruption/relocation checks. Direct replays +work with Python 3.10 or later, including optimized execution: + +```sh +python3 -I -O -B research/complex-cross-block-locality/verify.py +python3 -I -O -B research/complex-cross-block-locality/independent.py +``` + +Default replay is read-only. `--record` explicitly regenerates only this +package's receipt. It does not regenerate any predecessor artifact. +The generic registered replay needs the pinned base Git object. Direct +replay also works in a minimal source export containing this package and +the one declared archive. The decompressed canonical word is authenticated +separately from its immutable source archive. + +## Scope, sources and assignment + +Base: `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. At that base, the selected +conditional kappa is `0.001672660197076918`, with the complex supplier +binding. Its certificate, actual construction and review were followed; +the baseline source-binding check was run, not the full cold replay. + +The runtime input is the canonical local word in +`research/community-frontier1042-audit/selected-replay.tar.gz`, still used +by the selected PR1094 owner map. Its decompressed SHA256 is +`4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c`. +[SOURCES.json](SOURCES.json) pins the exact base, archive, predecessor head +and consulted proof/extractor. No pending implementation is imported at +runtime. The block extractor is adapted from PR1429 with attribution. + +OS assignment seed **33** selected the complex track. The three candidates +were deeper decoder punctures, coefficient-work sharing, and joint late-block +mixing. Nearby work made the first two poor choices. Pair 33 of the sorted +66 block pairs, bases 624/656, was the pilot; the new localization property +then supported the full twelve-block statement. This is an enlarged +interface class, not another random search in a closed scalar neighborhood. +[TASK.json](TASK.json) records the bounded experiment, overlap limits and +[coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1492). + +The selected frontier, frozen predecessors and `upstream/` are unchanged. +All-size/compiler, common-label/mutable-source, whole-call hosting, +precision/tape, exact recovery, analytic transfer and bit H1-H5 assumptions +remain inherited. A full selected cold replay, native/global admission, +hosted CI and proof-assistant verification are not claimed. + +## Open next questions + +An additional source version or an earlier target entry can break the +antichain or global output wall. A useful next experiment would specify +one actual earlier target frame or later source value, then recheck the +global premises and charge its complete preparation/continuation cost. +No such replacement interface or favorable complete budget is supplied +here. The precise question and blocker are in [TASK.json](TASK.json). + +## Attribution and license + +Credit **Ali Romman** for PR1429's fixed-block statement, extractor, +carrier-count proof and retirement argument. Its inspected head is +`591582004d82302268da3b264a6ba5edec1521de`; its pending status is retained. +The joint boundary, global confinement argument and cross-block extension +are this contribution. PR1429's additional PR1319 provider coverage is +not claimed here. + +Credit **Jeremy Kothe** for the mutable-leaver/local supplier lineage, +**Rohan Arun** for the k8 slots and PR1094 owner exchanges, **Hao Yan** for +the controller, and **icekylinx**, **Chafik Boukhalfa**, **Jonathan Capalbo** +and the retained source-notice contributors for the underlying construction. +The retained bit supplier is **DreamingOfClouds**' PR589 on **eumemic**'s +PR555. All original archives and notices remain intact. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex** +assistance in derivation, code, proof, checks and writing. New material +is Apache-2.0 under the repository license. diff --git a/research/complex-cross-block-locality/SOURCES.json b/research/complex-cross-block-locality/SOURCES.json new file mode 100644 index 0000000000..10bf13e470 --- /dev/null +++ b/research/complex-cross-block-locality/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + } + ], + "predecessors": [ + { + "pr": 1429, + "author": "Ali Romman", + "head": "591582004d82302268da3b264a6ba5edec1521de", + "status": "pending; consulted and credited, not a runtime code dependency", + "files": [ + { + "path": "research/complex-block-rank-optimum/verify.py", + "sha256": "3741b64dc76f771b74f06c80d4dfcbb6263bf34a790478640d813b59f8b38a3d", + "git_blob": "5b08fcad862e6bd35d491bf49894e475396320b3" + }, + { + "path": "research/complex-block-rank-optimum/PROOF.md", + "git_blob": "31c6c2bdf23be41ac1ecc07ab64a5a27baed28f2", + "sha256": "89a03b68d16e25603dbaae6b80df9e4f70cda314fe43396433fa2b9037fb5213" + } + ] + } + ] +} diff --git a/research/complex-cross-block-locality/TASK.json b/research/complex-cross-block-locality/TASK.json new file mode 100644 index 0000000000..cdda10d664 --- /dev/null +++ b/research/complex-cross-block-locality/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract, not another mixture already covered by the frozen catalogue.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the frozen catalogue bound exclusions and select one genuinely different helper endpoint inventory.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the complete optimistic child histogram and reject it immediately if even the relaxation has insufficient headroom.", + "bottleneck_link": "Helper inventory changes can improve the moment; repacking a covered cost interface cannot evade its scoped bound.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Allow arbitrary cross-block helper mixing among the twelve frozen selected late interfaces, and determine its complete helper-growth moment floor.", + "scope_change_reason": "Refined the helper-inventory card to an explicit changed interface: remove PR1429's no-cross-block condition while retaining fixed input/output ports, 96 helpers and monotone frames.", + "bottleneck_link": "The complex supplier binds. A lower complete helper-growth moment could improve it; the proved joint floor closes this particular larger coding class.", + "budget_minutes": 50, + "stop_rule": "50-minute session; orient within ten minutes, test global localization and simultaneous boundary, stop if either fails, reserve final quarter for verification. Complete all 12 blocks and all 255 nonempty supports each; no heuristic cutoff.", + "outcome": "negative-result", + "evidence": "PROOF.md supplies the all-length argument; CERTIFICATE.json and INDEPENDENT.json bind exact finite premises and rejection controls to the selected canonical word.", + "author": "Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in research, derivation, implementation, proof writing and verification. No delegated worker or independent human review.", + "open_questions": [ + { + "question": "Can one explicit earlier target entry or later source version break the global localization bound with a favorable complete bill?", + "why_it_matters": "Those changes evade a material hypothesis and could change the binding complex paid moment.", + "first_step": "Extract one candidate interface from the actual word, identify the failed global premise and price every new source, frame, continuation and restoration charge before synthesis.", + "blocked_by": "This package supplies neither the new legal interface nor a favorable complete cost recurrence." + } + ], + "assignment_seed": 33, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "pilot_pair": { + "zero_based_pair_index": 33, + "bases": [ + 624, + 656 + ] + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1492", + "candidate_tasks": [ + "Deeper punctures for an eight-term complex decoder; nearby decoder work made this less attractive.", + "Coefficient-work sharing; already covered by PR722/739/751/769/945/975 and related packages.", + "Cross-block helper mixing at the fixed late interfaces; expressly excluded by PR1429 and selected here." + ], + "overlap": { + "initial": { + "open_pr_bodies": 745, + "discussion_records": 59, + "discussion_comment_scope": "last six comments per discussion; nested replies and all historical comments not fully searched", + "helper_discussion_query": "HTTP 500; replaced by direct GraphQL list with complete discussion pagination" + }, + "final": { + "checked_at_utc": "2026-10-14T02:03:08Z", + "open_pr_bodies": 758, + "discussion_records": 68, + "discussion_complete_pagination": true, + "nearest_pr": 1429, + "nearest_head_unchanged": true, + "main_head": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6" + }, + "limits": "Open PR titles/bodies, current discussion bodies and last six comments, local READMEs and review ledger. No claim of complete code-diff/history or reply coverage, or guaranteed novelty." + } +} diff --git a/research/complex-cross-block-locality/VALIDATION.md b/research/complex-cross-block-locality/VALIDATION.md new file mode 100644 index 0000000000..ab9d1068cc --- /dev/null +++ b/research/complex-cross-block-locality/VALIDATION.md @@ -0,0 +1,39 @@ +# Local validation + +Validated on macOS arm64, Python 3.12.13 and Python 3.14.2. Base commit: +`ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. + +The registered Python 3.12 command in the README passed. It checks exact +Git and SHA256 source identities, freshly reconstructs both committed +receipts, runs ten primary semantic controls and two independent boundary +controls, and passes four public-entrypoint tests. Those tests reject a +changed primary certificate, a changed independent receipt and source drift +in both engines, and check both optimized engines in a minimal read-only +export with spaces in its path. The export's file hashes remain unchanged. + +The primary replay covers all twelve block interfaces, 3060 support cases, +4560 input-frame pairs, 1056 foreign high/input tests, 4608 input/target +tests and 24 rank-seven kernel frames. The separate set/integer-minor +implementation agrees, checks 240 scalar columns including target dirt, +and establishes joint boundary rank 192 over each of two checked primes. +Its rank-deficient controls return 191. + +Both direct replays also passed with isolated, optimized Python 3.14. +`make selected-record-check` passed with the original selected kappa +`836330098538459/500000000000000000`. No selected input or predecessor was +regenerated. The patch is confined to this new research directory. + +Before submission, main remained at the recorded base and PR1429 remained +open at `591582004d82302268da3b264a6ba5edec1521de`, with no review comments. +Its two consulted file blobs were checked against the exact GitHub tree. +The overlap refresh covered 758 open PR bodies and 68 discussion bodies +with their last six comments. Nested replies, all historical comments and +every code diff were not searched. PR1429 is the nearest contribution; this +package explicitly changes its no-cross-block premise and credits it. + +The all-length argument is written mathematics supported by these finite +premises. No proof-assistant build, independent human review, full selected +cold replay, new native/global supplier admission, hosted CI success or new +kappa is claimed. Both checking implementations are by the same assisted +author. The fixed early source versions and late target frames remain +essential restrictions. diff --git a/research/complex-cross-block-locality/VERIFY.json b/research/complex-cross-block-locality/VERIFY.json new file mode 100644 index 0000000000..eec94b686a --- /dev/null +++ b/research/complex-cross-block-locality/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-bound extraction, all local/global premises, saved certificate and ten semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate set/integer-minor, scalar-column and modular-boundary replay, with saved receipt and two rank controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Four public-entrypoint tests: source drift, receipt corruption and minimal read-only relocation." + } + ] +} diff --git a/research/complex-cross-block-locality/independent.py b/research/complex-cross-block-locality/independent.py new file mode 100644 index 0000000000..c4771b799f --- /dev/null +++ b/research/complex-cross-block-locality/independent.py @@ -0,0 +1,264 @@ +"""Separate set/integer-minor replay; imports no primary checker code. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +Both implementations are by the same assisted author, not independent human review. +""" +import argparse +from collections import Counter +from fractions import Fraction +import gzip +import hashlib +from itertools import combinations +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASES = (592, 600, 608, 624, 632, 640, 648, 656, 672, 680, 688, 696) + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def span(generators, initial=frozenset({0})): + out = set(initial) + for x in generators: + out.update([a ^ x for a in out]) + return frozenset(out) + + +def det(a): + """Integer Bareiss determinant, with exact division checked.""" + a = [row.copy() for row in a] + last, sign = 1, 1 + for k in range(len(a) - 1): + p = next((i for i in range(k, len(a)) if a[i][k]), None) + if p is None: + return 0 + if p != k: + a[p], a[k] = a[k], a[p] + sign = -sign + pivot = a[k][k] + for i in range(k + 1, len(a)): + for j in range(k + 1, len(a)): + n = pivot * a[i][j] - a[i][k] * a[k][j] + check(n % last == 0, "nonexact Bareiss division") + a[i][j] = n // last + a[i][k] = 0 + last = pivot + return sign * a[-1][-1] if a else 1 + + +def column_rank(q, columns): + # Every Q entry is a half integer. Its real Gram matrix is positive semidefinite. + a = [[2 * Fraction(row[j]) for j in columns] for row in q] + check(all(x.denominator == 1 for row in a for x in row), "non-half-integer input") + a = [[int(x) for x in row] for row in a] + gram = [[sum(x * y for x, y in zip(r, s)) for s in a] for r in a] + for n in range(min(4, len(columns)), 0, -1): + for s in combinations(range(4), n): + if det([[gram[i][j] for j in s] for i in s]): + return n + return 0 + + +def registers(g): + return g[1:3] if g[0] == "add" else g[1:2] + + +def modular_boundary(prefix, wanted, width, prime): + check(prime > 2 and all(prime % d for d in range(2, int(prime ** .5) + 1)), "nonprime modulus") + rows = [{i: 1} for i in range(width)] + for g in prefix: + if g[0] == "add": + _, dst, src, n, d, _ = g + check(d % prime != 0, "nonunit modular denominator") + q = n * pow(d, -1, prime) % prime + for k, v in rows[src].items(): + rows[dst][k] = (rows[dst].get(k, 0) + q * v) % prime + rows[dst] = {k: v for k, v in rows[dst].items() if v} + else: + _, dst, n, d, _ = g + check(d % prime != 0, "nonunit modular denominator") + q = n * pow(d, -1, prime) % prime + rows[dst] = {k: q * v % prime for k, v in rows[dst].items() if q * v % prime} + pivots = {} + product = 1 + for r in wanted: + row = rows[r].copy() + while row: + c = min(row) + factor = row[c] + if c in pivots: + for j, v in pivots[c].items(): + row[j] = (row.get(j, 0) - factor * v) % prime + row = {j: v for j, v in row.items() if v} + else: + product = product * factor % prime + inverse = pow(factor, -1, prime) + pivots[c] = {j: v * inverse % prime for j, v in row.items()} + break + return {"prime": prime, "rank": len(pivots), "pivot_columns": list(pivots), + "pivot_product_mod_prime": product} + + +def compute(): + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + sources = json.loads((HERE / "SOURCES.json").read_text()) + pin = next(p for p in sources["files"] if p["usage"] == "input") + data = (ROOT / pin["path"]).read_bytes() + check(hashlib.sha256(data).hexdigest() == pin["sha256"], "input source mismatch") + with tarfile.open(ROOT / pin["path"], "r:gz") as t: + raw = gzip.decompress(t.extractfile("t16/global/base/providers/gauge44/CANONICAL-WORD.json.gz").read()) + check(hashlib.sha256(raw).hexdigest() == expected["source_payload_sha256"], "payload mismatch") + w = json.loads(raw) + frames = [span(f) for f in w["frames"]] + state = [frames[i] for i in w["start"]] + for g in w["A"]: + for r in registers(g): + check(state[r] <= frames[g[-1]], "independent A descent") + state[r] = frames[g[-1]] + states = [] + for g in w["B"]: + states.append(state.copy()) + for r in registers(g): + check(state[r] <= frames[g[-1]], "independent B descent") + state[r] = frames[g[-1]] + blocks = expected["blocks"] + check([b["base"] for b in blocks] == list(BASES), "missing or reordered block") + kernels = [] + checked_columns = 0 + corrections = set() + for b, local in zip(blocks, expected["local"]): + hs = set(range(b["base"], b["base"] + 8)) + reads = [(i, g) for i, g in enumerate(w["B"]) if g[0] == "add" and g[1] in hs + and g[2] not in hs and len(frames[g[-1]]) > 2] + check([g[2] for _, g in reads] == b["inputs"], "input extraction") + check([frames[g[-1]] for _, g in reads] == list(map(span, b["input_frames"])), "input frames") + corr = [i for i, g in enumerate(w["B"][:reads[0][0]]) + if g[0] == "add" and g[1] in hs and g[2] in hs] + check(corr == b["corrections"], "correction extraction") + corrections.update(corr) + start = min(corr) + low = sorted(r for r in hs if len(states[start][r]) == 2) + high = sorted(hs - set(low)) + check(low == b["low"] and high == b["high"], "low/high extraction") + check(all(states[start][r] == span(b["common"]) for r in high), "common extraction") + outs = [(i, g) for i, g in enumerate(w["B"]) if i >= start and g[0] == "add" + and g[2] in hs and g[1] not in hs] + targets = sorted({g[1] for _, g in outs}) + check(targets == b["targets"], "output extraction") + for r, entry, cap, at in zip(targets, b["target_entries"], b["caps"], b["output_entries"]): + check(at == next(i for i, g in outs if g[1] == r), "output boundary") + check(states[at][r] == span(entry) and frames[w["final"][r]] == span(cap), "output frames") + # Execute each formal input separately, including arbitrary target dirt. + variables = sorted(hs) + b["inputs"] + targets + maps = {r: [] for r in targets} + for origin in variables: + values = {r: Fraction(int(r == origin)) for r in variables} + for i, g in enumerate(w["B"]): + if i >= start and hs.intersection(registers(g)): + if g[0] == "add": + values[g[1]] += Fraction(g[3], g[4]) * values[g[2]] + else: + values[g[1]] *= Fraction(g[2], g[3]) + for r in targets: + maps[r].append(values[r]) + checked_columns += 1 + q = [[str(v) for v in maps[r][8:16]] for r in targets] + check(q == b["Q"], "literal Q map") + check([[str(maps[r][variables.index(h)]) for h in low] for r in targets] == b["R"], "literal R map") + check(all(maps[r][variables.index(h)] == 0 for r in targets for h in high), "dirty-high output") + check(all(maps[r][16 + j] == int(r == t) for r in targets for j, t in enumerate(targets)), "target dirt") + paths = {r: states[start][r] for r in hs} + bill = Counter() + for i, g in enumerate(w["B"]): + if i >= start: + for r in hs.intersection(registers(g)): + a, z = paths[r], frames[g[-1]] + check(a <= z, "independent helper descent") + d = (len(z) // len(a)).bit_length() - 1 + if d: + bill[d] += 1 + paths[r] = z + for r, f in paths.items(): + check(len(frames[w["final"][r]]) == 512, "full endpoint") + d = (512 // len(f)).bit_length() - 1 + if d: + bill[d] += 1 + check({str(k): v for k, v in bill.items()} == b["profile"], "independent complete bill") + spaces = {0: frozenset({0})} + spectrum, projections = Counter(), Counter() + found = set() + for mask in range(1, 256): + lowbit = mask & -mask + j = lowbit.bit_length() - 1 + spaces[mask] = span(b["input_frames"][j], spaces[mask ^ lowbit]) + cols = [j for j in range(8) if mask >> j & 1] + dim = len(spaces[mask]).bit_length() - 1 + r = column_rank(q, cols) + spectrum[len(cols), dim, r] += 1 + if len(cols) <= 4: + other = [j for j in range(8) if j not in cols] + proj = len(cols) - 4 + column_rank(q, other) + projections[len(cols), proj] += 1 + check(proj >= (3 * len(cols) + 3) // 4, "independent projection") + if r < len(cols): + check(dim >= 7, "independent low-rank kernel") + if dim == 7: + found.add(spaces[mask]) + check(found == {span(f) for f in local["kernels"]}, "kernel-frame census") + check([list(k) + [v] for k, v in sorted(spectrum.items())] == local["spectrum"], "subset rank census") + check([list(k) + [v] for k, v in sorted(projections.items())] == local["projections"], "projection census") + kernels.extend((b["base"], f) for f in found) + inputs = [(b["base"], r, span(f)) for b in blocks for r, f in zip(b["inputs"], b["input_frames"])] + caps = [(r, span(f)) for b in blocks for r, f in zip(b["targets"], b["caps"])] + entries = [span(f) for b in blocks for f in b["target_entries"]] + check(len(inputs) == len({r for _, r, _ in inputs}) == 96, "independent global input alias") + check(len(caps) == len({r for r, _ in caps}) == len({f for _, f in caps}) == 48, "global target identity") + check(all(not f <= g and not g <= f for (_, _, f), (_, _, g) in combinations(inputs, 2)), "independent antichain") + check(all(not span(b["common"]) <= f for b in blocks for owner, _, f in inputs if owner != b["base"]), "independent high locality") + check(all(len(f) * len(g) >= 256 * len(f & g) for _, _, f in inputs for g in entries), "independent output wall") + check(len({f for _, f in kernels}) == 24, "global kernel identity") + for owner, f in kernels: + included = [(o, r, len(g)) for o, r, g in inputs if g <= f] + allowed = sorted(r for r, g in caps if f <= g) + check(all(o == owner and size == 32 for o, _, size in included), "independent kernel locality") + check(len(allowed) <= 1, "independent kernel outputs") + record = next(k for k in expected["global"]["kernel_frames"] if span(k["frame"]) == f) + check(record["owner"] == owner and record["eligible_targets"] == allowed + and record["contained_inputs"] == [r for _, r, _ in included], "global kernel receipt") + cut = min(b["first_input"] for b in blocks) + prefix = w["A"] + w["cut"] + [g for i, g in enumerate(w["B"][:cut]) if i not in corrections] + wanted = sorted({r for b in blocks for r in b["helpers"] + b["inputs"]}) + minor_witnesses = [modular_boundary(prefix, wanted, len(w["start"]), p) for p in (65521, 65537)] + check(all(m["rank"] == 192 for m in minor_witnesses), "joint boundary rank") + check(modular_boundary(prefix, wanted[:-1] + wanted[:1], len(w["start"]), 65521)["rank"] == 191, + "duplicated boundary coordinate control") + broken = prefix + [["scale", wanted[0], 0, 1, 0]] + check(modular_boundary(broken, wanted, len(w["start"]), 65521)["rank"] == 191, + "singular boundary control") + return {"status": "PASS_INDEPENDENT_CROSS_BLOCK_PREMISES", "source_payload_sha256": hashlib.sha256(raw).hexdigest(), + "literal_columns": checked_columns, "subset_cases": 3060, "input_pairs": 4560, + "foreign_high_tests": 1056, "input_target_tests": 4608, "kernel_frames": 24, + "boundary_witnesses": minor_witnesses, "boundary_controls": 2} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--record", action="store_true") + args = parser.parse_args() + result = compute() + out = HERE / "INDEPENDENT.json" + if args.record: + out.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + check(json.loads(out.read_text()) == result, "independent saved receipt mismatch") + print("PASS_INDEPENDENT_CROSS_BLOCK_PREMISES columns=240 subsets=3060 boundary_rank=192 primes=2 controls=2") + + +if __name__ == "__main__": + main() diff --git a/research/complex-cross-block-locality/test_package.py b/research/complex-cross-block-locality/test_package.py new file mode 100644 index 0000000000..bf72b788f3 --- /dev/null +++ b/research/complex-cross-block-locality/test_package.py @@ -0,0 +1,91 @@ +"""Corruption and minimal read-only relocation checks for the public replay. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = HERE.relative_to(ROOT) +ARCHIVE = Path("research/community-frontier1042-audit/selected-replay.tar.gz") + + +def run(root, script, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(root / PACKAGE / script), *map(str, args)], + cwd=root.parent, capture_output=True, text=True, timeout=60) + + +def export(root): + shutil.copytree(HERE, root / PACKAGE, ignore=shutil.ignore_patterns("__pycache__")) + (root / ARCHIVE).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / ARCHIVE, root / ARCHIVE) + + +def hashes(root): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + +class PackageTests(unittest.TestCase): + def test_changed_primary_certificate_is_rejected(self): + with tempfile.TemporaryDirectory() as d: + receipt = json.loads((HERE / "CERTIFICATE.json").read_text()) + receipt["profile"]["1"] -= 1 + bad = Path(d) / "wrong.json" + bad.write_text(json.dumps(receipt)) + result = run(ROOT, "verify.py", "--certificate", bad) + self.assertNotEqual(result.returncode, 0) + self.assertIn("saved certificate mismatch", result.stderr) + + def test_source_drift_is_rejected_before_replay(self): + with tempfile.TemporaryDirectory() as d: + root = Path(d) / "source export" + export(root) + with (root / ARCHIVE).open("ab") as f: + f.write(b"changed source") + for script, message in (("verify.py", "source hash mismatch"), + ("independent.py", "input source mismatch")): + result = run(root, script) + self.assertNotEqual(result.returncode, 0) + self.assertIn(message, result.stderr) + + def test_changed_independent_receipt_is_rejected(self): + with tempfile.TemporaryDirectory() as d: + root = Path(d) / "source export" + export(root) + path = root / PACKAGE / "INDEPENDENT.json" + receipt = json.loads(path.read_text()) + receipt["boundary_witnesses"][0]["rank"] = 191 + path.write_text(json.dumps(receipt)) + result = run(root, "independent.py") + self.assertNotEqual(result.returncode, 0) + self.assertIn("independent saved receipt mismatch", result.stderr) + + def test_minimal_read_only_export_is_unchanged(self): + with tempfile.TemporaryDirectory() as d: + root = Path(d) / "read only export with spaces" + export(root) + before = hashes(root) + paths = [root, *root.rglob("*")] + try: + for p in paths: + p.chmod(0o555 if p.is_dir() else 0o444) + for script in ("verify.py", "independent.py"): + result = run(root, script) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_", result.stdout) + self.assertEqual(hashes(root), before) + finally: + for p in paths: + p.chmod(0o755 if p.is_dir() else 0o644) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/complex-cross-block-locality/verify.py b/research/complex-cross-block-locality/verify.py new file mode 100644 index 0000000000..b68d7d860e --- /dev/null +++ b/research/complex-cross-block-locality/verify.py @@ -0,0 +1,377 @@ +"""Exact premises for joint late-block mixing; standard library, read-only replay. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +Block extraction follows Ali Romman's PR1429, pinned in SOURCES.json. +Global localization, joint boundary and independent checks are new here. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +from itertools import combinations +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASES = (592, 600, 608, 624, 632, 640, 648, 656, 672, 680, 688, 696) +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +MEMBER = "t16/global/base/providers/gauge44/CANONICAL-WORD.json.gz" +PAYLOAD_HASH = "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def basis(values): + pivots = {} + for x in values: + while x: + p = x.bit_length() + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + for p in sorted(pivots): + for q in pivots: + if q > p and pivots[q] >> (p - 1) & 1: + pivots[q] ^= pivots[p] + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def inside(a, b): + return len(basis(tuple(a) + tuple(b))) == len(basis(b)) + + +def rank(matrix): + rows = [list(map(Q, row)) for row in matrix] + if not rows: + return 0 + k = 0 + for col in range(len(rows[0])): + p = next((i for i in range(k, len(rows)) if rows[i][col]), None) + if p is None: + continue + rows[k], rows[p] = rows[p], rows[k] + d = rows[k][col] + rows[k] = [v / d for v in rows[k]] + for i in range(k + 1, len(rows)): + if rows[i][col]: + d = rows[i][col] + rows[i] = [a - d * b for a, b in zip(rows[i], rows[k])] + k += 1 + if k == len(rows): + break + return k + + +def incident(g): + need(g[0] in ("add", "scale"), "unknown scalar opcode") + return g[1:3] if g[0] == "add" else g[1:2] + + +def scalar(g, rows): + if g[0] == "add": + _, dst, src, n, d, _ = g + rows[dst] = [a + Q(n, d) * b for a, b in zip(rows[dst], rows[src])] + else: + _, dst, n, d, _ = g + rows[dst] = [Q(n, d) * a for a in rows[dst]] + + +def load_word(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for pin in pins["files"]: + if pin["usage"] == "input": + data = (ROOT / pin["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == pin["sha256"], "source hash mismatch") + with tarfile.open(ROOT / ARCHIVE, "r:gz") as archive: + payload = gzip.decompress(archive.extractfile(MEMBER).read()) + need(hashlib.sha256(payload).hexdigest() == PAYLOAD_HASH, "canonical payload mismatch") + return json.loads(payload) + + +def frame_states(w): + f = w["frames"] + state = list(w["start"]) + for g in w["A"]: + for r in incident(g): + need(inside(f[state[r]], f[g[-1]]), "A frame descent") + state[r] = g[-1] + states = [] + for g in w["B"]: + states.append(state.copy()) + for r in incident(g): + need(inside(f[state[r]], f[g[-1]]), "B frame descent") + state[r] = g[-1] + states.append(state) + return states + + +def extract(w, states, base): + helpers = list(range(base, base + 8)) + hs = set(helpers) + f, gates = w["frames"], w["B"] + arrivals = [(i, g) for i, g in enumerate(gates) + if g[0] == "add" and g[1] in hs and g[2] not in hs] + reads = [(i, g) for i, g in arrivals if len(basis(f[g[-1]])) > 1] + need(len(reads) == 8 and len({g[1] for _, g in reads}) == 8 + and len({g[2] for _, g in reads}) == 8, "eight independent input slots") + first = reads[0][0] + need(reads[-1][0] == first + 7, "input segment is not contiguous") + correction = [i for i, g in enumerate(gates[:first]) + if g[0] == "add" and g[1] in hs and g[2] in hs] + need(correction, "missing correction") + start = min(correction) + need(all(i < start for i, g in arrivals if (i, g) not in reads), "extra late input") + low = [r for r in helpers if len(basis(f[states[start][r]])) == 1] + high = [r for r in helpers if r not in low] + need(len(low) == len(high) == 4, "four low and four high helpers required") + common = basis(f[states[start][high[0]]]) + need(len(common) in (4, 5), "common rank") + need(all(basis(f[states[start][r]]) == common for r in high), "unequal high frames") + need(all(inside(f[states[start][r]], common) for r in low), "low outside common") + need(all(basis(f[gates[i][-1]]) == common for i in correction), "correction frame") + outputs = [(i, g) for i, g in enumerate(gates) if i >= start and g[0] == "add" + and g[2] in hs and g[1] not in hs] + need(len(outputs) == 8 and min(i for i, _ in outputs) > first + 7, "late output segment") + targets = sorted({g[1] for _, g in outputs}) + need(len(targets) == 4, "four target ports") + inputs = [g[2] for _, g in reads] + input_frames = [basis(f[g[-1]]) for _, g in reads] + entries = [next(i for i, g in outputs if g[1] == r) for r in targets] + entry_frames = [basis(f[states[i][r]]) for i, r in zip(entries, targets)] + caps = [basis(f[w["final"][r]]) for r in targets] + need(all(len(x) in (5, 6) and inside(common, x) for x in input_frames), "input frame") + need(all(len(x) in (7, 8) for x in entry_frames) and all(len(x) == 8 for x in caps), "target ranks") + need(all(inside(g, h) for g, h in zip(entry_frames, caps)), "target entry outside cap") + need(all(not (g[0] == "scale" and g[1] in targets) + and not (g[0] == "add" and g[2] in targets) + for g in gates[min(entries):]), "late target used as scratch") + variables = helpers + inputs + need(len(set(variables + targets)) == 20, "block register alias") + rows = {r: [Q(int(i == j)) for i in range(16)] for j, r in enumerate(variables)} + rows.update({r: [Q(0)] * 16 for r in targets}) + current = {r: basis(f[states[start][r]]) for r in helpers} + profile = Counter() + for i, g in enumerate(gates): + if i >= start and hs.intersection(incident(g)): + need(set(incident(g)) <= set(rows), "undeclared block wire") + scalar(g, rows) + for r in hs.intersection(incident(g)): + new = basis(f[g[-1]]) + need(inside(current[r], new), "helper descent") + if len(new) > len(current[r]): + profile[len(new) - len(current[r])] += 1 + current[r] = new + for r in helpers: + need(len(basis(f[w["final"][r]])) == 9, "helper endpoint not full") + if len(current[r]) < 9: + profile[9 - len(current[r])] += 1 + out = [rows[r] for r in targets] + need(all(row[helpers.index(r)] == 0 for row in out for r in high), "high dirt reaches output") + q = [row[8:] for row in out] + need(rank(q) == 4, "Q rank") + need(all(sum(row[j] != 0 for row in q) == 2 for j in range(8)), "two output demands per input") + expected = Counter({1: 24, 2: 8, 3: 4}) if len(common) == 4 else Counter({1: 32, 4: 4}) + need(profile == expected, "complete block profile") + return dict(base=base, helpers=helpers, low=low, high=high, common=list(common), + first_correction=start, corrections=correction, first_input=first, + inputs=inputs, input_frames=list(map(list, input_frames)), targets=targets, + output_entries=entries, target_entries=list(map(list, entry_frames)), + caps=list(map(list, caps)), Q=[[str(v) for v in row] for row in q], + R=[[str(row[helpers.index(r)]) for r in low] for row in out], + profile={str(k): v for k, v in sorted(profile.items())}) + + +def local_premises(block): + q, fs = block["Q"], block["input_frames"] + kernel_frames = {} + projection = Counter() + spectrum = Counter() + for mask in range(1, 256): + cols = [i for i in range(8) if mask >> i & 1] + r = rank([[row[i] for i in cols] for row in q]) + f = basis(v for i in cols for v in fs[i]) + spectrum[(len(cols), len(f), r)] += 1 + if len(cols) <= 4: + comp = [i for i in range(8) if i not in cols] + proj = len(cols) - 4 + rank([[row[i] for i in comp] for row in q]) + need(proj >= (3 * len(cols) + 3) // 4, "kernel projection too small") + projection[(len(cols), proj)] += 1 + if r < len(cols): + need(len(f) >= 7, "kernel below rank seven") + if len(f) == 7: + kernel_frames[f] = True + return {"kernels": [list(f) for f in sorted(kernel_frames)], + "spectrum": [list(k) + [v] for k, v in sorted(spectrum.items())], + "projections": [list(k) + [v] for k, v in sorted(projection.items())]} + + +def global_premises(blocks, local): + inputs = [(b["base"], r, f) for b in blocks for r, f in zip(b["inputs"], b["input_frames"])] + targets = [(b["base"], r, f) for b in blocks for r, f in zip(b["targets"], b["caps"])] + need(len({r for _, r, _ in inputs}) == 96, "global input alias") + need(len({r for _, r, _ in targets}) == 48, "global target alias") + main = {r for b in blocks for r in b["helpers"] + b["inputs"]} + need(not main.intersection(r for _, r, _ in targets), "output aliases a source/helper") + for (_, _, f), (_, _, g) in combinations(inputs, 2): + need(not inside(f, g) and not inside(g, f), "global input antichain") + for (_, _, f), (_, _, g) in combinations(targets, 2): + need(basis(f) != basis(g), "global target caps distinct") + high_tests = 0 + for b in blocks: + for owner, _, f in inputs: + if owner != b["base"]: + need(not inside(b["common"], f), "foreign high-frame access") + high_tests += 1 + for _, _, f in inputs: + for b in blocks: + for g in b["target_entries"]: + need(len(basis(f + g)) >= 8, "global output below rank eight") + kernel_records = [] + for b, result in zip(blocks, local): + for f in result["kernels"]: + contained = [(owner, r, len(g)) for owner, r, g in inputs if inside(g, f)] + eligible = [r for _, r, g in targets if inside(f, g)] + need(all(owner == b["base"] for owner, _, _ in contained), "foreign input in kernel frame") + need(all(dim == 5 for _, _, dim in contained), "rank-six input in kernel frame") + need(len(eligible) <= 1, "kernel frame reaches two global outputs") + kernel_records.append({"owner": b["base"], "frame": f, + "contained_inputs": [r for _, r, _ in contained], + "eligible_targets": eligible}) + need(len({tuple(k["frame"]) for k in kernel_records}) == len(kernel_records), "shared kernel frame") + return {"input_pairs": len(inputs) * (len(inputs) - 1) // 2, + "foreign_high_tests": high_tests, "input_target_tests": len(inputs) * len(targets), + "kernel_frames": kernel_records} + + +def boundary(w, states, blocks): + """All corrections commute to one actual, full-rank main-array boundary.""" + cut = min(b["first_input"] for b in blocks) + helpers = {r for b in blocks for r in b["helpers"]} + inputs = {r for b in blocks for r in b["inputs"]} + need(len(helpers | inputs) == 192, "joint boundary aliases") + removed = {i for b in blocks for i in b["corrections"]} + earliest = min(b["first_correction"] for b in blocks) + for b in blocks: + hs = set(b["helpers"]) + need(all(basis(w["frames"][states[earliest][r]]) == + basis(w["frames"][states[b["first_correction"]][r]]) for r in hs), + "helper not ready at joint entry") + for i in range(b["first_correction"], b["first_input"]): + g = w["B"][i] + if hs.intersection(incident(g)): + need(i in b["corrections"] and set(incident(g)) <= hs, "correction crosses exterior event") + for r, f in zip(b["inputs"], b["input_frames"]): + need(basis(w["frames"][states[cut][r]]) == tuple(f), "input not ready at common cut") + need(all(g[1] != r for g in w["B"][cut:b["first_input"]]), "input changes before own read") + prefix = w["A"] + w["cut"] + [g for i, g in enumerate(w["B"][:cut]) if i not in removed] + determinant = Q(1) + for g in prefix: + need(all(0 <= r < len(w["start"]) for r in incident(g)), "private array in boundary prefix") + if g[0] == "add": + need(g[1] != g[2] and g[4] != 0, "noninvertible ADD in prefix") + else: + need(g[2] != 0 and g[3] != 0, "noninvertible SCALE in prefix") + determinant *= Q(g[2], g[3]) + need(determinant != 0, "singular joint prefix") + return {"B_cut": cut, "main_arrays": len(w["start"]), "independent_coordinates": 192, + "prefix_gates": len(prefix), "deferred_corrections": sorted(removed), + "prefix_determinant": str(determinant), "registers": sorted(helpers | inputs)} + + +def controls(w, states, blocks, local): + names = [] + def rejects(name, run, expected): + try: + run() + except ValueError as error: + need(expected in str(error), name + " rejected for wrong reason: " + str(error)) + else: + raise ValueError(name + " incorrectly passed") + names.append(name) + bad = deepcopy(blocks) + bad[1]["input_frames"][0] = bad[0]["input_frames"][0] + rejects("foreign_equal_input", lambda: global_premises(bad, local), "antichain") + bad = deepcopy(blocks) + bad[1]["common"] = bad[0]["common"] + rejects("high_information_can_escape", lambda: global_premises(bad, local), "high-frame") + bad = deepcopy(blocks) + bad[1]["caps"][0] = bad[0]["caps"][0] + rejects("shared_output_cap", lambda: global_premises(bad, local), "caps distinct") + bad = deepcopy(blocks) + bad[1]["target_entries"][0] = bad[0]["input_frames"][0] + rejects("early_output_access", lambda: global_premises(bad, local), "below rank eight") + bad = deepcopy(blocks) + f = local[0]["kernels"][0] + old_caps = {tuple(basis(cap)) for b in bad for cap in b["caps"]} + extensions = [] + for v in range(1, 512): + cap = basis(f + [v]) + if len(cap) == 8 and cap not in old_caps and cap not in extensions: + extensions.append(cap) + need(len(extensions) >= 2, "kernel-output control has no witness") + bad[1]["caps"][:2] = [list(c) for c in extensions[:2]] + rejects("two_global_readers_for_kernel", lambda: global_premises(bad, local), "two global outputs") + bad = deepcopy(blocks[0]) + for row in bad["Q"]: + row[0] = "0" + rejects("zero_output_column", lambda: local_premises(bad), "kernel below rank seven") + bad = deepcopy(w) + bad["B"][1054] = ["add", blocks[1]["inputs"][0], 0, 1, 1, bad["B"][1054][-1]] + rejects("asynchronous_input_mutation", lambda: boundary(bad, states, blocks), "input changes") + bad = deepcopy(w) + i = blocks[0]["corrections"][0] + bad["B"][i] = ["add", blocks[0]["helpers"][0], 0, 1, 1, bad["B"][i][-1]] + rejects("noncommuting_deferred_correction", lambda: boundary(bad, states, blocks), "exterior event") + bad = deepcopy(w) + bad["A"][0] = ["scale", 0, 0, 1, bad["A"][0][-1]] + rejects("singular_prefix", lambda: boundary(bad, states, blocks), "noninvertible SCALE") + bad = deepcopy(w) + bad["final"][BASES[0]] = w["start"][BASES[0]] + rejects("unpaid_helper_restoration", lambda: extract(bad, states, BASES[0]), "endpoint not full") + return names + + +def compute(): + w = load_word() + states = frame_states(w) + blocks = [extract(w, states, b) for b in BASES] + local = [local_premises(b) for b in blocks] + global_result = global_premises(blocks, local) + joint = boundary(w, states, blocks) + total = Counter() + for b in blocks: + total.update({int(k): v for k, v in b["profile"].items()}) + need(total == Counter({1: 328, 2: 56, 3: 28, 4: 20}), "total moment profile") + return {"schema_version": 1, "status": "PASS_CROSS_BLOCK_LOCALITY_PREMISES", + "source_payload_sha256": PAYLOAD_HASH, "blocks": blocks, "local": local, + "global": global_result, "boundary": joint, + "profile": {str(k): v for k, v in sorted(total.items())}, + "controls": controls(w, states, blocks, local)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--record", action="store_true") + parser.add_argument("--certificate", type=Path, default=HERE / "CERTIFICATE.json") + args = parser.parse_args() + result = compute() + if args.record: + args.certificate.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(json.loads(args.certificate.read_text()) == result, "saved certificate mismatch") + print("PASS_CROSS_BLOCK_LOCALITY_PREMISES blocks=12 inputs=96 ports=48 " + "input_pairs=4560 foreign_high=1056 output_pairs=4608 kernels=24 controls=" + + str(len(result["controls"]))) + + +if __name__ == "__main__": + main()