diff --git a/research/r439-bsection-multwrite/CANDIDATE.json b/research/r439-bsection-multwrite/CANDIDATE.json new file mode 100644 index 0000000000..16532f2d8d --- /dev/null +++ b/research/r439-bsection-multwrite/CANDIDATE.json @@ -0,0 +1,3205 @@ +{ + "schema": "r439-bsection-multwrite/1", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "source": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "search": { + "track": "bit supplier (00-19)", + "assignment_seed": 16, + "class": "all programs of single-source additive gates dest += src on the block's own registers realizing the exact integer transfer matrix; equivalently all legal nonnegative row/column subtraction paths to the identity", + "method": "6000 min-excess greedy reductions with random tie-breaks, 4000 uniform random legal trajectories (cap 90), then a width-6000 beam below the incumbent", + "seed_rule": "random.Random(20261013 + frame) per block (CPython Mersenne Twister)", + "stopping_rule": "all trajectories and the beam phase complete for every block; no adaptive stopping", + "coverage": "all ten phase-B blocks of the pinned tuned word", + "minimality_claimed": false + }, + "blocks": [ + { + "frame": 506, + "slice": [ + 102, + 128 + ], + "registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "original_gates": 26, + "new_gates": 21, + "gates": [ + [ + 506, + 52, + [ + 58 + ] + ], + [ + 506, + 52, + [ + 54 + ] + ], + [ + 506, + 47, + [ + 48 + ] + ], + [ + 506, + 58, + [ + 48 + ] + ], + [ + 506, + 48, + [ + 5 + ] + ], + [ + 506, + 47, + [ + 46 + ] + ], + [ + 506, + 5, + [ + 9 + ] + ], + [ + 506, + 52, + [ + 56 + ] + ], + [ + 506, + 52, + [ + 6 + ] + ], + [ + 506, + 9, + [ + 6 + ] + ], + [ + 506, + 46, + [ + 56 + ] + ], + [ + 506, + 52, + [ + 5 + ] + ], + [ + 506, + 52, + [ + 47 + ] + ], + [ + 506, + 56, + [ + 52 + ] + ], + [ + 506, + 5, + [ + 52 + ] + ], + [ + 506, + 54, + [ + 52 + ] + ], + [ + 506, + 58, + [ + 52 + ] + ], + [ + 506, + 47, + [ + 52 + ] + ], + [ + 506, + 9, + [ + 52 + ] + ], + [ + 506, + 46, + [ + 54 + ] + ], + [ + 506, + 48, + [ + 9 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 21, + 6000 + ], + [ + 26, + 4 + ], + [ + 27, + 6 + ], + [ + 28, + 11 + ], + [ + 29, + 14 + ], + [ + 30, + 31 + ], + [ + 31, + 50 + ], + [ + 32, + 68 + ], + [ + 33, + 87 + ], + [ + 34, + 110 + ], + [ + 35, + 126 + ], + [ + 36, + 174 + ], + [ + 37, + 177 + ], + [ + 38, + 212 + ], + [ + 39, + 224 + ], + [ + 40, + 229 + ], + [ + 41, + 206 + ], + [ + 42, + 219 + ], + [ + 43, + 162 + ], + [ + 44, + 131 + ], + [ + 45, + 108 + ], + [ + 46, + 70 + ], + [ + 47, + 39 + ], + [ + 48, + 32 + ], + [ + 49, + 23 + ], + [ + 50, + 10 + ], + [ + 51, + 4 + ], + [ + 52, + 4 + ], + [ + 53, + 3 + ] + ], + "dead_ends": 1466, + "beam_states": 1129511 + }, + { + "frame": 507, + "slice": [ + 128, + 163 + ], + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "original_gates": 35, + "new_gates": 24, + "gates": [ + [ + 507, + 3, + [ + 62 + ] + ], + [ + 507, + 465, + [ + 69 + ] + ], + [ + 507, + 69, + [ + 62 + ] + ], + [ + 507, + 68, + [ + 11 + ] + ], + [ + 507, + 68, + [ + 63 + ] + ], + [ + 507, + 63, + [ + 0 + ] + ], + [ + 507, + 69, + [ + 11 + ] + ], + [ + 507, + 61, + [ + 72 + ] + ], + [ + 507, + 61, + [ + 0 + ] + ], + [ + 507, + 62, + [ + 3 + ] + ], + [ + 507, + 11, + [ + 3 + ] + ], + [ + 507, + 465, + [ + 63 + ] + ], + [ + 507, + 63, + [ + 72 + ] + ], + [ + 507, + 68, + [ + 61 + ] + ], + [ + 507, + 62, + [ + 69 + ] + ], + [ + 507, + 61, + [ + 62 + ] + ], + [ + 507, + 63, + [ + 62 + ] + ], + [ + 507, + 3, + [ + 68 + ] + ], + [ + 507, + 62, + [ + 68 + ] + ], + [ + 507, + 69, + [ + 68 + ] + ], + [ + 507, + 465, + [ + 3 + ] + ], + [ + 507, + 72, + [ + 3 + ] + ], + [ + 507, + 11, + [ + 69 + ] + ], + [ + 507, + 0, + [ + 69 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 24, + 1 + ], + [ + 26, + 3081 + ], + [ + 27, + 2329 + ], + [ + 28, + 468 + ], + [ + 29, + 137 + ], + [ + 30, + 17 + ], + [ + 31, + 33 + ], + [ + 32, + 59 + ], + [ + 33, + 89 + ], + [ + 34, + 149 + ], + [ + 35, + 141 + ], + [ + 36, + 169 + ], + [ + 37, + 121 + ], + [ + 38, + 112 + ], + [ + 39, + 99 + ], + [ + 40, + 61 + ], + [ + 41, + 41 + ], + [ + 42, + 29 + ], + [ + 43, + 21 + ], + [ + 44, + 5 + ], + [ + 45, + 3 + ], + [ + 46, + 1 + ], + [ + 47, + 2 + ] + ], + "dead_ends": 2833, + "beam_states": 1135275 + }, + { + "frame": 519, + "slice": [ + 163, + 205 + ], + "registers": [ + 15, + 23, + 30, + 41, + 49, + 53, + 59, + 70, + 75, + 82, + 91, + 96 + ], + "original_gates": 42, + "new_gates": 27, + "gates": [ + [ + 519, + 49, + [ + 75 + ] + ], + [ + 519, + 49, + [ + 41 + ] + ], + [ + 519, + 30, + [ + 49 + ] + ], + [ + 519, + 59, + [ + 53 + ] + ], + [ + 519, + 53, + [ + 41 + ] + ], + [ + 519, + 41, + [ + 82 + ] + ], + [ + 519, + 53, + [ + 75 + ] + ], + [ + 519, + 59, + [ + 30 + ] + ], + [ + 519, + 15, + [ + 91 + ] + ], + [ + 519, + 30, + [ + 75 + ] + ], + [ + 519, + 96, + [ + 23 + ] + ], + [ + 519, + 82, + [ + 70 + ] + ], + [ + 519, + 59, + [ + 82 + ] + ], + [ + 519, + 75, + [ + 82 + ] + ], + [ + 519, + 82, + [ + 96 + ] + ], + [ + 519, + 82, + [ + 15 + ] + ], + [ + 519, + 30, + [ + 82 + ] + ], + [ + 519, + 82, + [ + 53 + ] + ], + [ + 519, + 96, + [ + 59 + ] + ], + [ + 519, + 91, + [ + 59 + ] + ], + [ + 519, + 15, + [ + 96 + ] + ], + [ + 519, + 70, + [ + 15 + ] + ], + [ + 519, + 49, + [ + 15 + ] + ], + [ + 519, + 23, + [ + 15 + ] + ], + [ + 519, + 41, + [ + 15 + ] + ], + [ + 519, + 75, + [ + 70 + ] + ], + [ + 519, + 53, + [ + 49 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 27, + 99 + ], + [ + 28, + 416 + ], + [ + 29, + 632 + ], + [ + 30, + 847 + ], + [ + 31, + 971 + ], + [ + 39, + 1 + ], + [ + 40, + 5 + ], + [ + 41, + 11 + ], + [ + 42, + 15 + ], + [ + 43, + 13 + ], + [ + 44, + 20 + ], + [ + 45, + 26 + ], + [ + 46, + 28 + ], + [ + 47, + 30 + ], + [ + 48, + 28 + ], + [ + 49, + 18 + ], + [ + 50, + 9 + ], + [ + 51, + 14 + ], + [ + 52, + 12 + ], + [ + 53, + 5 + ], + [ + 54, + 1 + ], + [ + 55, + 1 + ] + ], + "dead_ends": 6798, + "beam_states": 2400139 + }, + { + "frame": 508, + "slice": [ + 205, + 242 + ], + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "original_gates": 37, + "new_gates": 21, + "gates": [ + [ + 508, + 43, + [ + 97 + ] + ], + [ + 508, + 74, + [ + 19 + ] + ], + [ + 508, + 35, + [ + 74 + ] + ], + [ + 508, + 35, + [ + 43 + ] + ], + [ + 508, + 66, + [ + 57 + ] + ], + [ + 508, + 89, + [ + 35 + ] + ], + [ + 508, + 89, + [ + 27 + ] + ], + [ + 508, + 66, + [ + 35 + ] + ], + [ + 508, + 43, + [ + 66 + ] + ], + [ + 508, + 66, + [ + 65 + ] + ], + [ + 508, + 65, + [ + 89 + ] + ], + [ + 508, + 27, + [ + 66 + ] + ], + [ + 508, + 97, + [ + 27 + ] + ], + [ + 508, + 43, + [ + 65 + ] + ], + [ + 508, + 35, + [ + 97 + ] + ], + [ + 508, + 57, + [ + 89 + ] + ], + [ + 508, + 97, + [ + 19 + ] + ], + [ + 508, + 35, + [ + 89 + ] + ], + [ + 508, + 74, + [ + 43 + ] + ], + [ + 508, + 466, + [ + 43 + ] + ], + [ + 508, + 43, + [ + 19 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 21, + 1 + ], + [ + 25, + 824 + ], + [ + 26, + 2735 + ], + [ + 27, + 954 + ], + [ + 33, + 1 + ], + [ + 34, + 6 + ], + [ + 35, + 7 + ], + [ + 36, + 11 + ], + [ + 37, + 21 + ], + [ + 38, + 31 + ], + [ + 39, + 48 + ], + [ + 40, + 60 + ], + [ + 41, + 82 + ], + [ + 42, + 102 + ], + [ + 43, + 126 + ], + [ + 44, + 135 + ], + [ + 45, + 117 + ], + [ + 46, + 129 + ], + [ + 47, + 133 + ], + [ + 48, + 126 + ], + [ + 49, + 122 + ], + [ + 50, + 91 + ], + [ + 51, + 65 + ], + [ + 52, + 52 + ], + [ + 53, + 49 + ], + [ + 54, + 26 + ], + [ + 55, + 26 + ], + [ + 56, + 13 + ], + [ + 57, + 15 + ], + [ + 58, + 5 + ], + [ + 59, + 3 + ], + [ + 60, + 2 + ], + [ + 61, + 2 + ], + [ + 62, + 2 + ] + ], + "dead_ends": 3879, + "beam_states": 1776921 + }, + { + "frame": 520, + "slice": [ + 242, + 283 + ], + "registers": [ + 21, + 26, + 36, + 44, + 51, + 55, + 64, + 71, + 80, + 84, + 94, + 102 + ], + "original_gates": 41, + "new_gates": 37, + "gates": [ + [ + 520, + 102, + [ + 21 + ] + ], + [ + 520, + 94, + [ + 84 + ] + ], + [ + 520, + 51, + [ + 80 + ] + ], + [ + 520, + 55, + [ + 44 + ] + ], + [ + 520, + 84, + [ + 36 + ] + ], + [ + 520, + 84, + [ + 64 + ] + ], + [ + 520, + 44, + [ + 94 + ] + ], + [ + 520, + 64, + [ + 51 + ] + ], + [ + 520, + 44, + [ + 26 + ] + ], + [ + 520, + 55, + [ + 71 + ] + ], + [ + 520, + 94, + [ + 55 + ] + ], + [ + 520, + 44, + [ + 102 + ] + ], + [ + 520, + 55, + [ + 84 + ] + ], + [ + 520, + 55, + [ + 51 + ] + ], + [ + 520, + 94, + [ + 36 + ] + ], + [ + 520, + 84, + [ + 44 + ] + ], + [ + 520, + 51, + [ + 36 + ] + ], + [ + 520, + 94, + [ + 64 + ] + ], + [ + 520, + 64, + [ + 36 + ] + ], + [ + 520, + 64, + [ + 44 + ] + ], + [ + 520, + 84, + [ + 80 + ] + ], + [ + 520, + 36, + [ + 80 + ] + ], + [ + 520, + 80, + [ + 26 + ] + ], + [ + 520, + 80, + [ + 102 + ] + ], + [ + 520, + 102, + [ + 94 + ] + ], + [ + 520, + 94, + [ + 21 + ] + ], + [ + 520, + 21, + [ + 26 + ] + ], + [ + 520, + 26, + [ + 51 + ] + ], + [ + 520, + 51, + [ + 44 + ] + ], + [ + 520, + 44, + [ + 36 + ] + ], + [ + 520, + 26, + [ + 102 + ] + ], + [ + 520, + 84, + [ + 71 + ] + ], + [ + 520, + 44, + [ + 55 + ] + ], + [ + 520, + 80, + [ + 55 + ] + ], + [ + 520, + 21, + [ + 94 + ] + ], + [ + 520, + 36, + [ + 44 + ] + ], + [ + 520, + 71, + [ + 51 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 37, + 1 + ], + [ + 40, + 3 + ], + [ + 41, + 4 + ], + [ + 42, + 4 + ], + [ + 43, + 6 + ], + [ + 44, + 11 + ], + [ + 45, + 19 + ], + [ + 46, + 5 + ], + [ + 47, + 6 + ], + [ + 48, + 4 + ], + [ + 49, + 2 + ], + [ + 50, + 1 + ], + [ + 51, + 2 + ] + ], + "dead_ends": 9932, + "beam_states": 2173010 + }, + { + "frame": 509, + "slice": [ + 283, + 314 + ], + "registers": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92, + 468 + ], + "original_gates": 31, + "new_gates": 21, + "gates": [ + [ + 509, + 87, + [ + 77 + ] + ], + [ + 509, + 87, + [ + 38 + ] + ], + [ + 509, + 468, + [ + 33 + ] + ], + [ + 509, + 38, + [ + 33 + ] + ], + [ + 509, + 77, + [ + 33 + ] + ], + [ + 509, + 87, + [ + 22 + ] + ], + [ + 509, + 87, + [ + 50 + ] + ], + [ + 509, + 87, + [ + 92 + ] + ], + [ + 509, + 87, + [ + 60 + ] + ], + [ + 509, + 87, + [ + 67 + ] + ], + [ + 509, + 468, + [ + 38 + ] + ], + [ + 509, + 33, + [ + 87 + ] + ], + [ + 509, + 17, + [ + 33 + ] + ], + [ + 509, + 33, + [ + 22 + ] + ], + [ + 509, + 92, + [ + 33 + ] + ], + [ + 509, + 38, + [ + 17 + ] + ], + [ + 509, + 67, + [ + 17 + ] + ], + [ + 509, + 77, + [ + 17 + ] + ], + [ + 509, + 60, + [ + 17 + ] + ], + [ + 509, + 468, + [ + 92 + ] + ], + [ + 509, + 50, + [ + 67 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 21, + 1 + ], + [ + 22, + 1427 + ], + [ + 23, + 4573 + ], + [ + 30, + 2 + ], + [ + 31, + 8 + ], + [ + 32, + 8 + ], + [ + 33, + 9 + ], + [ + 34, + 7 + ], + [ + 35, + 21 + ], + [ + 36, + 26 + ], + [ + 37, + 43 + ], + [ + 38, + 56 + ], + [ + 39, + 69 + ], + [ + 40, + 73 + ], + [ + 41, + 80 + ], + [ + 42, + 106 + ], + [ + 43, + 93 + ], + [ + 44, + 108 + ], + [ + 45, + 119 + ], + [ + 46, + 130 + ], + [ + 47, + 122 + ], + [ + 48, + 126 + ], + [ + 49, + 105 + ], + [ + 50, + 76 + ], + [ + 51, + 70 + ], + [ + 52, + 42 + ], + [ + 53, + 42 + ], + [ + 54, + 28 + ], + [ + 55, + 14 + ], + [ + 56, + 7 + ], + [ + 57, + 6 + ], + [ + 58, + 1 + ], + [ + 59, + 3 + ] + ], + "dead_ends": 2400, + "beam_states": 1423579 + }, + { + "frame": 521, + "slice": [ + 314, + 361 + ], + "registers": [ + 10, + 13, + 32, + 34, + 39, + 42, + 76, + 79, + 83, + 85, + 104, + 107 + ], + "original_gates": 47, + "new_gates": 30, + "gates": [ + [ + 521, + 10, + [ + 107 + ] + ], + [ + 521, + 13, + [ + 85 + ] + ], + [ + 521, + 76, + [ + 42 + ] + ], + [ + 521, + 79, + [ + 104 + ] + ], + [ + 521, + 79, + [ + 76 + ] + ], + [ + 521, + 79, + [ + 13 + ] + ], + [ + 521, + 83, + [ + 32 + ] + ], + [ + 521, + 83, + [ + 34 + ] + ], + [ + 521, + 83, + [ + 10 + ] + ], + [ + 521, + 83, + [ + 79 + ] + ], + [ + 521, + 10, + [ + 39 + ] + ], + [ + 521, + 39, + [ + 83 + ] + ], + [ + 521, + 104, + [ + 34 + ] + ], + [ + 521, + 34, + [ + 39 + ] + ], + [ + 521, + 104, + [ + 107 + ] + ], + [ + 521, + 76, + [ + 107 + ] + ], + [ + 521, + 107, + [ + 13 + ] + ], + [ + 521, + 107, + [ + 79 + ] + ], + [ + 521, + 32, + [ + 42 + ] + ], + [ + 521, + 79, + [ + 10 + ] + ], + [ + 521, + 13, + [ + 34 + ] + ], + [ + 521, + 34, + [ + 42 + ] + ], + [ + 521, + 42, + [ + 83 + ] + ], + [ + 521, + 10, + [ + 83 + ] + ], + [ + 521, + 85, + [ + 79 + ] + ], + [ + 521, + 32, + [ + 34 + ] + ], + [ + 521, + 76, + [ + 10 + ] + ], + [ + 521, + 34, + [ + 104 + ] + ], + [ + 521, + 104, + [ + 10 + ] + ], + [ + 521, + 107, + [ + 34 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 30, + 1 + ], + [ + 31, + 337 + ], + [ + 32, + 131 + ], + [ + 42, + 1 + ], + [ + 43, + 7 + ], + [ + 44, + 8 + ], + [ + 45, + 9 + ], + [ + 46, + 12 + ], + [ + 47, + 6 + ], + [ + 48, + 8 + ], + [ + 49, + 13 + ], + [ + 50, + 16 + ], + [ + 51, + 11 + ], + [ + 52, + 12 + ], + [ + 53, + 7 + ], + [ + 54, + 5 + ], + [ + 55, + 3 + ], + [ + 56, + 5 + ], + [ + 57, + 4 + ], + [ + 58, + 3 + ], + [ + 59, + 1 + ], + [ + 60, + 2 + ], + [ + 61, + 1 + ] + ], + "dead_ends": 9398, + "beam_states": 2657812 + }, + { + "frame": 522, + "slice": [ + 361, + 404 + ], + "registers": [ + 1, + 7, + 24, + 25, + 28, + 29, + 98, + 99, + 100, + 101, + 106, + 108 + ], + "original_gates": 43, + "new_gates": 29, + "gates": [ + [ + 522, + 101, + [ + 7 + ] + ], + [ + 522, + 29, + [ + 24 + ] + ], + [ + 522, + 29, + [ + 98 + ] + ], + [ + 522, + 29, + [ + 101 + ] + ], + [ + 522, + 1, + [ + 108 + ] + ], + [ + 522, + 29, + [ + 99 + ] + ], + [ + 522, + 28, + [ + 100 + ] + ], + [ + 522, + 7, + [ + 25 + ] + ], + [ + 522, + 7, + [ + 108 + ] + ], + [ + 522, + 108, + [ + 24 + ] + ], + [ + 522, + 108, + [ + 29 + ] + ], + [ + 522, + 29, + [ + 1 + ] + ], + [ + 522, + 100, + [ + 25 + ] + ], + [ + 522, + 29, + [ + 25 + ] + ], + [ + 522, + 108, + [ + 98 + ] + ], + [ + 522, + 108, + [ + 99 + ] + ], + [ + 522, + 106, + [ + 29 + ] + ], + [ + 522, + 29, + [ + 100 + ] + ], + [ + 522, + 25, + [ + 7 + ] + ], + [ + 522, + 28, + [ + 106 + ] + ], + [ + 522, + 1, + [ + 28 + ] + ], + [ + 522, + 98, + [ + 28 + ] + ], + [ + 522, + 24, + [ + 28 + ] + ], + [ + 522, + 100, + [ + 28 + ] + ], + [ + 522, + 99, + [ + 28 + ] + ], + [ + 522, + 25, + [ + 28 + ] + ], + [ + 522, + 101, + [ + 24 + ] + ], + [ + 522, + 7, + [ + 1 + ] + ], + [ + 522, + 108, + [ + 25 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 29, + 1534 + ], + [ + 41, + 2 + ], + [ + 42, + 7 + ], + [ + 43, + 12 + ], + [ + 44, + 15 + ], + [ + 45, + 12 + ], + [ + 46, + 18 + ], + [ + 47, + 27 + ], + [ + 48, + 18 + ], + [ + 49, + 17 + ], + [ + 50, + 27 + ], + [ + 51, + 25 + ], + [ + 52, + 26 + ], + [ + 53, + 25 + ], + [ + 54, + 18 + ], + [ + 55, + 13 + ], + [ + 56, + 7 + ], + [ + 57, + 7 + ], + [ + 58, + 6 + ], + [ + 59, + 5 + ], + [ + 60, + 2 + ], + [ + 62, + 2 + ], + [ + 63, + 1 + ], + [ + 64, + 1 + ], + [ + 66, + 1 + ] + ], + "dead_ends": 8172, + "beam_states": 2586714 + }, + { + "frame": 523, + "slice": [ + 404, + 449 + ], + "registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "original_gates": 45, + "new_gates": 26, + "gates": [ + [ + 523, + 18, + [ + 88 + ] + ], + [ + 523, + 93, + [ + 16 + ] + ], + [ + 523, + 93, + [ + 18 + ] + ], + [ + 523, + 2, + [ + 4 + ] + ], + [ + 523, + 2, + [ + 93 + ] + ], + [ + 523, + 14, + [ + 90 + ] + ], + [ + 523, + 20, + [ + 95 + ] + ], + [ + 523, + 103, + [ + 109 + ] + ], + [ + 523, + 103, + [ + 2 + ] + ], + [ + 523, + 20, + [ + 14 + ] + ], + [ + 523, + 2, + [ + 20 + ] + ], + [ + 523, + 20, + [ + 103 + ] + ], + [ + 523, + 95, + [ + 18 + ] + ], + [ + 523, + 4, + [ + 2 + ] + ], + [ + 523, + 14, + [ + 18 + ] + ], + [ + 523, + 93, + [ + 103 + ] + ], + [ + 523, + 109, + [ + 18 + ] + ], + [ + 523, + 90, + [ + 103 + ] + ], + [ + 523, + 18, + [ + 20 + ] + ], + [ + 523, + 93, + [ + 2 + ] + ], + [ + 523, + 20, + [ + 88 + ] + ], + [ + 523, + 14, + [ + 18 + ] + ], + [ + 523, + 109, + [ + 18 + ] + ], + [ + 523, + 88, + [ + 18 + ] + ], + [ + 523, + 95, + [ + 18 + ] + ], + [ + 523, + 16, + [ + 20 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 26, + 716 + ], + [ + 37, + 1 + ], + [ + 39, + 2 + ], + [ + 40, + 2 + ], + [ + 41, + 13 + ], + [ + 42, + 9 + ], + [ + 43, + 27 + ], + [ + 44, + 24 + ], + [ + 45, + 42 + ], + [ + 46, + 50 + ], + [ + 47, + 56 + ], + [ + 48, + 53 + ], + [ + 49, + 43 + ], + [ + 50, + 44 + ], + [ + 51, + 47 + ], + [ + 52, + 50 + ], + [ + 53, + 41 + ], + [ + 54, + 34 + ], + [ + 55, + 30 + ], + [ + 56, + 26 + ], + [ + 57, + 17 + ], + [ + 58, + 17 + ], + [ + 59, + 7 + ], + [ + 60, + 6 + ], + [ + 61, + 4 + ], + [ + 62, + 4 + ], + [ + 63, + 4 + ], + [ + 64, + 1 + ], + [ + 65, + 1 + ], + [ + 66, + 1 + ], + [ + 67, + 1 + ] + ], + "dead_ends": 8627, + "beam_states": 2884409 + }, + { + "frame": 524, + "slice": [ + 449, + 490 + ], + "registers": [ + 8, + 12, + 31, + 37, + 40, + 45, + 73, + 78, + 81, + 86, + 105, + 110 + ], + "original_gates": 41, + "new_gates": 26, + "gates": [ + [ + 524, + 8, + [ + 86 + ] + ], + [ + 524, + 8, + [ + 105 + ] + ], + [ + 524, + 110, + [ + 12 + ] + ], + [ + 524, + 12, + [ + 73 + ] + ], + [ + 524, + 73, + [ + 86 + ] + ], + [ + 524, + 40, + [ + 73 + ] + ], + [ + 524, + 105, + [ + 37 + ] + ], + [ + 524, + 110, + [ + 8 + ] + ], + [ + 524, + 40, + [ + 45 + ] + ], + [ + 524, + 31, + [ + 78 + ] + ], + [ + 524, + 73, + [ + 8 + ] + ], + [ + 524, + 31, + [ + 81 + ] + ], + [ + 524, + 31, + [ + 37 + ] + ], + [ + 524, + 78, + [ + 31 + ] + ], + [ + 524, + 110, + [ + 31 + ] + ], + [ + 524, + 31, + [ + 40 + ] + ], + [ + 524, + 73, + [ + 31 + ] + ], + [ + 524, + 45, + [ + 110 + ] + ], + [ + 524, + 40, + [ + 110 + ] + ], + [ + 524, + 12, + [ + 110 + ] + ], + [ + 524, + 81, + [ + 40 + ] + ], + [ + 524, + 37, + [ + 40 + ] + ], + [ + 524, + 78, + [ + 40 + ] + ], + [ + 524, + 8, + [ + 40 + ] + ], + [ + 524, + 86, + [ + 40 + ] + ], + [ + 524, + 105, + [ + 78 + ] + ] + ], + "all_registers_touched": true, + "histogram": [ + [ + 26, + 1 + ], + [ + 27, + 267 + ], + [ + 28, + 2260 + ], + [ + 29, + 3473 + ], + [ + 34, + 1 + ], + [ + 35, + 1 + ], + [ + 37, + 1 + ], + [ + 38, + 6 + ], + [ + 39, + 5 + ], + [ + 40, + 16 + ], + [ + 41, + 13 + ], + [ + 42, + 24 + ], + [ + 43, + 30 + ], + [ + 44, + 38 + ], + [ + 45, + 36 + ], + [ + 46, + 45 + ], + [ + 47, + 37 + ], + [ + 48, + 44 + ], + [ + 49, + 37 + ], + [ + 50, + 37 + ], + [ + 51, + 27 + ], + [ + 52, + 31 + ], + [ + 53, + 17 + ], + [ + 54, + 8 + ], + [ + 55, + 7 + ], + [ + 56, + 10 + ], + [ + 57, + 4 + ], + [ + 58, + 2 + ], + [ + 59, + 3 + ], + [ + 60, + 1 + ], + [ + 61, + 3 + ], + [ + 64, + 1 + ] + ], + "dead_ends": 3515, + "beam_states": 2357916 + } + ] +} diff --git a/research/r439-bsection-multwrite/CERTIFICATE.json b/research/r439-bsection-multwrite/CERTIFICATE.json new file mode 100644 index 0000000000..ad0c40c333 --- /dev/null +++ b/research/r439-bsection-multwrite/CERTIFICATE.json @@ -0,0 +1,361 @@ +{ + "status": "PASS_R439_BSECTION_MULTWRITE", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "assignment_seed": 16, + "blocks": [ + { + "frame": 506, + "slice": [ + 102, + 128 + ], + "registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "original_gates": 26, + "new_gates": 21, + "boolean_inputs_checked": 1024, + "forward_integer_sha256": "3a753476d03618495a38142694ca45b0aefb0d446812bd87598ccba69bccfdd7", + "reverse_old_total": 89, + "reverse_new_total": 65, + "reverse_entrywise_dominated": false + }, + { + "frame": 507, + "slice": [ + 128, + 163 + ], + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "original_gates": 35, + "new_gates": 24, + "boolean_inputs_checked": 1024, + "forward_integer_sha256": "092a132d3ad8cc9617fdb389d1fa47147ecb7ffeeb02aaa74f7596366bf820c7", + "reverse_old_total": 174, + "reverse_new_total": 82, + "reverse_entrywise_dominated": true + }, + { + "frame": 519, + "slice": [ + 163, + 205 + ], + "registers": [ + 15, + 23, + 30, + 41, + 49, + 53, + 59, + 70, + 75, + 82, + 91, + 96 + ], + "original_gates": 42, + "new_gates": 27, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "e15c9a30d0d0e44daf32d2b4125f9b69263d48e7487b0b91b49e7e9ba9397648", + "reverse_old_total": 407, + "reverse_new_total": 145, + "reverse_entrywise_dominated": false + }, + { + "frame": 508, + "slice": [ + 205, + 242 + ], + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "original_gates": 37, + "new_gates": 21, + "boolean_inputs_checked": 2048, + "forward_integer_sha256": "21ec3c5628db324d406f10bdd4fb28c61d14a41ab7f42e509ccdc38231a652e2", + "reverse_old_total": 169, + "reverse_new_total": 55, + "reverse_entrywise_dominated": false + }, + { + "frame": 520, + "slice": [ + 242, + 283 + ], + "registers": [ + 21, + 26, + 36, + 44, + 51, + 55, + 64, + 71, + 80, + 84, + 94, + 102 + ], + "original_gates": 41, + "new_gates": 37, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "61daed3b32c4e46b352205c2aa1034b7288f297857471c2dfc5d18fed3e033e5", + "reverse_old_total": 368, + "reverse_new_total": 830, + "reverse_entrywise_dominated": false + }, + { + "frame": 509, + "slice": [ + 283, + 314 + ], + "registers": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92, + 468 + ], + "original_gates": 31, + "new_gates": 21, + "boolean_inputs_checked": 2048, + "forward_integer_sha256": "fcfbd9158c9dd5b1c963e2db42d9065fb89e144a436e120dd3de7c2fee7110fb", + "reverse_old_total": 94, + "reverse_new_total": 52, + "reverse_entrywise_dominated": true + }, + { + "frame": 521, + "slice": [ + 314, + 361 + ], + "registers": [ + 10, + 13, + 32, + 34, + 39, + 42, + 76, + 79, + 83, + 85, + 104, + 107 + ], + "original_gates": 47, + "new_gates": 30, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "3aca7fadf5d79b1dac43414e6dd7e9035c1be97afd39b8ceeb9436f5f5370d99", + "reverse_old_total": 405, + "reverse_new_total": 147, + "reverse_entrywise_dominated": false + }, + { + "frame": 522, + "slice": [ + 361, + 404 + ], + "registers": [ + 1, + 7, + 24, + 25, + 28, + 29, + 98, + 99, + 100, + 101, + 106, + 108 + ], + "original_gates": 43, + "new_gates": 29, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "2ed5aba7410132ceb6d54d465892600c6665da60fdb78bf7c842c4effdd6cd7c", + "reverse_old_total": 319, + "reverse_new_total": 129, + "reverse_entrywise_dominated": false + }, + { + "frame": 523, + "slice": [ + 404, + 449 + ], + "registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "original_gates": 45, + "new_gates": 26, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "ec4919a2b7ba73cc9b25fd99b7d64d5bc7a8b0d38a1185078a61fb9a19feaa63", + "reverse_old_total": 229, + "reverse_new_total": 81, + "reverse_entrywise_dominated": false + }, + { + "frame": 524, + "slice": [ + 449, + 490 + ], + "registers": [ + 8, + 12, + 31, + 37, + 40, + 45, + 73, + 78, + 81, + 86, + 105, + 110 + ], + "original_gates": 41, + "new_gates": 26, + "boolean_inputs_checked": 4096, + "forward_integer_sha256": "ec348a4eebe4a9fb7e13c63a47d0cc4da12cbcd47ce9d5980e1f0baf5b7a181d", + "reverse_old_total": 233, + "reverse_new_total": 73, + "reverse_entrywise_dominated": true + } + ], + "columns": 661, + "closed_frames": 636, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "identical_register_frame_paths": 661, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "conclusion": { + "U_block_form": true, + "J_identity": true, + "K_equals_D": true, + "C_is_U_inverse": true + }, + "before": { + "records": 27234, + "adds": 24305, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 49347, + "reverse_positive_bound": 1113070, + "payload_bits": 93, + "record_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + "after": { + "records": 26982, + "adds": 24053, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 26653, + "reverse_positive_bound": 776006, + "payload_bits": 90, + "record_sha256": "060abdd63a8c5b119b84d076eb906a0da2a6bca524aa7de74e4a97399b1944ab" + }, + "adds_saved": 252, + "new_kappa_claim": false, + "candidate_content_sha256": "838f889fd0b430f9ce2f3528f2579f5fe1a81f9442db59be78368489879c3a17", + "negative_controls": [ + "mutated_source", + "dropped_gate", + "illegal_frame", + "swapped_block", + "omitted_cleanup", + "missing_gate_matching_cleanup", + "illegal_frame_word", + "stale_cleanup" + ], + "search": { + "track": "bit supplier (00-19)", + "assignment_seed": 16, + "class": "all programs of single-source additive gates dest += src on the block's own registers realizing the exact integer transfer matrix; equivalently all legal nonnegative row/column subtraction paths to the identity", + "method": "6000 min-excess greedy reductions with random tie-breaks, 4000 uniform random legal trajectories (cap 90), then a width-6000 beam below the incumbent", + "seed_rule": "random.Random(20261013 + frame) per block (CPython Mersenne Twister)", + "stopping_rule": "all trajectories and the beam phase complete for every block; no adaptive stopping", + "coverage": "all ten phase-B blocks of the pinned tuned word", + "minimality_claimed": false + } +} diff --git a/research/r439-bsection-multwrite/CLAIM.md b/research/r439-bsection-multwrite/CLAIM.md new file mode 100644 index 0000000000..89bbc92b5c --- /dev/null +++ b/research/r439-bsection-multwrite/CLAIM.md @@ -0,0 +1,51 @@ +# Sprint scope claim (recorded locally) + +No pinned sprint coordination issue exists (checked 2026-10-13; open issues +#650 and #913 are unrelated), so the scope claim is recorded here, per the +sprint protocol. + +- Track and seed: **bit supplier (00-19)**, OS random seed **16** (drawn from + `System.Security.Cryptography.RandomNumberGenerator`). +- Base commit: `007664306fff84fbb1c9a1b4053b69f439764034` (origin/main at + sprint start; selected #890/#869/#870 with #589 on #555, conditional kappa + 0.001661957774647029). +- Three narrow candidates evaluated during orientation: (a) exact class + minimality for the frame-521 factorization of merged PR #884; (b) the + multi-write shear class on frame 523, where the best recorded program (39, + PR #891) is only a single-write class minimum and PR #857's factor search + stopped at 40; (c) cheaper synthesis of the literal reverse cleanup + section C. Seed `16 mod 3 = 1` selected candidate (b). +- Exact object: the phase-B block schedule of PR589's tuned punctured R439 + word (`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`), + section B at frames 506-509 and 519-524. Because the search is per-block + and generic over the schedule, the claimed scope widened from frame 523 to + all ten blocks of this one frame schedule, which the track allows ("one + specific circuit, frame schedule"). +- Method: deterministic three-phase search (6,000 min-excess greedy + reductions with random tie-breaks, 4,000 uniform random legal + trajectories capped at 90, one width-6,000 beam below the incumbent) over + the full multi-write shear class = legal nonnegative row/column + subtraction paths from each block's transfer matrix to the identity. + Seeds `20261013 + frame` per block; all trials complete; no adaptive + stopping. +- Parameter range: all ten phase-B blocks of the pinned word; all ten + spliced into the verified word. +- Expected deliverable: one verified research package + (`research/r439-bsection-multwrite/`) with per-block replacement programs, + a spliced word, exact bills and bounds, and scoped search-coverage + statements; no new kappa. +- Overlap check at claim time (2026-10-13, before the search ran): open PRs + #857/#873/#880/#884/#906/#908/#914/#923 hold per-block claims on frames + 507/508/519/520/521/522/523/524; merged PR #891 holds the single-write + minima for 506/508/523. All use bounded randomized or fixed-factor + classes; none claims a class minimum in the full multi-write class and + none covers all ten blocks with one search. A second, independent method + on the same schedule is intended: complete-class coverage and strictly + shorter programs, with every competitor's number reproduced only as a + comparison row. +- Status: completed in session; branch `research/agent-10-bit-seed16`, commit + `8f878062`; submitted as + https://github.com/CrocSwap/integer-mult-bounds/pull/1015. Result: + 388 -> 262 phase-B gates; 24,305 -> 24,053 complete local ADDs; nine of + ten blocks improve on every recorded claim, frame 520 does not beat open + PR #923. See README.md and VALIDATION.md. diff --git a/research/r439-bsection-multwrite/NOTICE.md b/research/r439-bsection-multwrite/NOTICE.md new file mode 100644 index 0000000000..727d5b5862 --- /dev/null +++ b/research/r439-bsection-multwrite/NOTICE.md @@ -0,0 +1,14 @@ +# Notice + +R439 phase-B multi-write block programs, 2026. + +Built on the PR555/PR589 R439 supplier and its retained notices (eumemic, +DreamingOfClouds, Dylan Crow, Zhihao Chen and predecessors). The verifier +uses the repository's pinned owning interface checker and record exporter. +Block-level comparison credit: PR #891 (Aaron Wang), PR #880 (Krishnendu +Purohit), PR #884 (martin Rv), PRs #857/#873/#906/#908/#914/#923 and the +prefix-resynthesis line #904/#936/#952; none of their implementations or +savings is imported. + +Prepared with help from opencode. New files are offered under the +repository's Apache-2.0 license. No independent human review is claimed. diff --git a/research/r439-bsection-multwrite/README.md b/research/r439-bsection-multwrite/README.md new file mode 100644 index 0000000000..e200b4cb1f --- /dev/null +++ b/research/r439-bsection-multwrite/README.md @@ -0,0 +1,156 @@ +# R439 phase-B schedule: multi-write shear programs for all ten blocks + +**Finite bit-circuit construction; no new kappa.** This replaces every +phase-B block of the selected PR589 tuned punctured R439 word +(`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`) with a +shorter exact program on the same registers at the same frame, found by one +deterministic search in the full multi-write shear class. The complete +exported local word falls **24,305 -> 24,053 ADDs** (252 complete ADDs: +126 forward gates and their 126 literal reverse-cleanup gates). + +| quantity | before | after | +|---|---:|---:| +| phase-B block gates (all ten) | 388 | **262** | +| complete ADD records | 24,305 | **24,053** | +| all scalar records | 27,234 | 26,982 | +| forward positive bound | 49,347 | **26,653** | +| composed reverse positive bound | 1,113,070 | **776,006** | +| local payload | 93 bits | **90 bits** (cap 104) | +| paid profile / rank mass | `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` / 5,129 | unchanged | +| nine rank-seven COPY/ERASE pairs | 9 / 9 | 9 / 9 | +| bit saving / kappa | conditional, complex-bound | unchanged, no new kappa | + +All 661 register frame paths are identical before and after (every block +register is touched by its replacement program), so the frozen hosting and +paid profile carry over unchanged. Each replacement block has exactly the +same integer transfer matrix as the block it replaces, so the programs agree +over every commutative coefficient ring and on arbitrary dirty F2 inputs; the +exact F2 endpoint holds on all 661 dirty-input columns and the inherited +H1-H5 interface conclusions of the pinned `xcheck_p.py` hold on the spliced +word. + +## Per-block results against the recorded state of the art + +| frame | slice | word | this search | best previously recorded | +|---|---|---:|---:|---| +| 506 | `B[102:128)` | 26 | **21** | 24: PR #891 single-write class minimum; open PR #1001 independently claims 21 | +| 507 | `B[128:163)` | 35 | **24** | 30: PR #880 fixed two-factor splits; PR #884's README records an unpublished 24-gate orientation candidate | +| 519 | `B[163:205)` | 42 | **27** | 32: open PR #908 by title | +| 508 | `B[205:242)` | 37 | **21** | 30: PR #873 whole-block schedule, PR #891 class minimum | +| 520 | `B[242:283)` | 41 | 37 | 29: open PR #923 — **not beaten here** | +| 509 | `B[283:314)` | 31 | **21** | PR #891: infeasible in the single-write class; open PR #973 independently claims 21 | +| 521 | `B[314:361)` | 47 | **30** | 31: merged PR #884 factorization (no minimality claimed) | +| 522 | `B[361:404)` | 43 | **29** | 33: open PR #906 trajectories | +| 523 | `B[404:449)` | 45 | **26** | 39: PR #891 single-write class minimum; 40: open PR #857 | +| 524 | `B[449:490)` | 41 | **26** | 27: open PR #914 by title | + +Nine of ten blocks improve on every recorded claim; frame 520 does not beat +open PR #923's claim and its local reverse total grows (368 -> 830) even +though the composed word-level reverse bound falls. No concurrent +implementation or saving is imported: every program here comes from the one +search below against the pinned word. The comparison rows for open PRs +#908/#914/#923 use their titles and bodies, not their code. + +**Overlap refreshed at submission (2026-10-13, after the search and +verification completed).** Open PR #1001 (frame 506 at 21) and PR #973 +(frame 509 at 21) independently reach the same counts as two blocks here; +that is convergent evidence from separate searches, and both are credited. +Open PR #989 composes the four blocks of PRs #880/#873/#908/#914 at +24,305 -> 24,233 ADDs; this search's programs on those same four frames +(507: 24, 508: 21, 519: 27, 524: 26) are strictly shorter than the counts +they compose (30/30/32/27), and this one word covers all ten blocks at +24,305 -> 24,053. The phase-A prefix-resynthesis line (#904/#936/#952/#980) +is a different mechanism and is not composed here. + +## Class and search + +A block is a sequence of single-source additive gates `dest += src` on its +own registers; its exact integer transfer matrix `M` satisfies `M >= I`. Any +replacement program of such gates is exactly a path of legal nonnegative row +or column subtractions from `M` to the identity (row = peel a last-applied +gate, column = peel a first-applied gate). The class is therefore **all** +multi-write shear programs on the block's own registers: shared intermediate +rows and mid-construction reads are inside it. It strictly contains PR +#891's whole-block single-write class and PR #880's fixed factor splits, and +equals the subtraction class sampled by PRs #884 and #906. Programs that use +registers outside the block, or non-additive gates, are outside the class. + +`search.py` runs, per block, with `random.Random(20261013 + frame)`: + +1. 6,000 min-excess greedy reductions with random tie-breaks; +2. 4,000 uniform random legal trajectories (path cap 90); +3. one width-6,000 beam search for a path strictly below the incumbent. + +The stopping rule is complete: all 10,000 trajectories and the beam phase +finish for every block; there is no adaptive stopping. Coverage is all ten +phase-B blocks of the pinned word, once each. The search is deterministic; +`search.py` regenerates `CANDIDATE.json` byte for byte (about ten minutes +with one worker per block). **"Best found" is not a minimality result**: no +block has a certified class minimum here, and shorter programs may exist. +As weak context only, `rank(M - I)` (an admissible lower bound on any shear +program) is 8 for frame 506, 11 for frame 521 and 10 for frame 523. + +## Reproduce + +Standard-library Python 3.11+ from the repository root: + +```sh +python3 -I -B research/r439-bsection-multwrite/verify.py +``` + +Expected (about two minutes): + +```text +PASS_R439_BSECTION_MULTWRITE gates=388->262 ADDs=24305->24053 columns=661 controls=8 rank_mass=5129 kappa=unchanged +``` + +`search.py` (about ten minutes, parallel) regenerates `CANDIDATE.json` and +prints `PASS_R439_BSECTION_MULTWRITE_SEARCH ... gates=388->262`. + +## Verification + +`verify.py` imports no search code. It checks the source SHA-256 pins; each +block's register binding, gate shape, exact integer transfer matrix and all +2^10-2^12 Boolean block truth tables; the ten-way splice (applied from the +end of B backwards) and the rebuilt literal reverse cleanup; all 661 +register frame paths; the exact F2 endpoint on all 661 arbitrary dirty-input +columns; the H1-H5 interface via the pinned `xcheck_p.py`; the paid profile +and rank mass; and the exported bills and positive/payload bounds via the +pinned `export_records.py`. Eight mutation controls must be rejected (mutated +source, dropped gate, illegal frame, swapped block, omitted cleanup gate, +deleted gate with matching cleanup, illegal frame in the spliced word, stale +cleanup). The exact report is pinned in `CERTIFICATE.json` and compared on +every run. + +## Scope and obligations + +Only `research/r439-bsection-multwrite/` is added. `upstream/`, the selected +certificate and every consumed supplier source are unchanged. This is a +conditional finite construction and a completed bounded search, not a Lean +proof and not a new kappa: the bit side does not bind the selected witness +(kappa is complex-bound at 0.001661957774647029 at the base commit), so the +result is bit headroom only. The class excludes scratch registers outside each block and +non-additive gates; the D-prefix substitution candidates (#915/#926/#941) +are a different, not-adopted mechanism whose savings are not composed here. +The C++ native legality and 5/9/11-stage replays, the hosted invoice, the +global assembly, the selected cold replay, Lean formalization and remote CI +are not run here. All inherited all-size/compiler, common-label/mutable-source, +whole-call hosting, precision/tape and analytic assumptions remain. The +spliced word is a research witness; it is not proposed as the selected +frontier. + +## Credit + +The word and its generators, checkers and pricing pipelines are eumemic's +(PR #543/#555, on #510's nine-stage chain and #545's punctured unit), with +DreamingOfClouds (PR #589 tuning), Dylan Crow (record exporter), Zhihao Chen +and the retained supplier lineage. The phase-B whole-block framing is PR +#891's (Aaron Wang), the fixed-factor framing is PR #880's (Krishnendu +Purohit), the factorization/subtraction searches are PRs #857/#884/#906's, +and the independent-verifier pattern follows PR #884 (martin Rv); their +objects and savings are compared above but not imported. Concurrent claims +from PRs #908/#914/#923, the convergent per-block claims #973/#1001, the +four-block composition #989, and the four/five/six-wire prefix line +(#904/#936/#952/#980) are credited and not composed. Prepared with help +from opencode. +Apache-2.0. No independent human review is claimed. diff --git a/research/r439-bsection-multwrite/SOURCES.json b/research/r439-bsection-multwrite/SOURCES.json new file mode 100644 index 0000000000..64af8cf107 --- /dev/null +++ b/research/r439-bsection-multwrite/SOURCES.json @@ -0,0 +1,19 @@ +{ + "schema": "sha256-source-pins/1", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "files": { + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + "predecessors": { + "PR589_reviewed_head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "PR555": "selected R439 construction (eumemic)", + "PR884": "frame-521 factorization search and independent-verifier pattern (martin Rv)", + "PR891": "whole-block single-write survey of all ten phase-B blocks (Aaron Wang)", + "PR873": "whole-block scheduling class for frame 508", + "PR880": "fixed two-factor splits for frame 507", + "PR906": "row-subtraction trajectories for frame 522", + "PR857": "factorization search for frame 523" + } +} diff --git a/research/r439-bsection-multwrite/VALIDATION.md b/research/r439-bsection-multwrite/VALIDATION.md new file mode 100644 index 0000000000..b756dccdb0 --- /dev/null +++ b/research/r439-bsection-multwrite/VALIDATION.md @@ -0,0 +1,71 @@ +# Validation record + +All commands below ran on Windows 11 with CPython 3.13 from the repository +root of branch `research/agent-10-bit-seed16`, base +`007664306fff84fbb1c9a1b4053b69f439764034`. Prepared with help from +opencode. + +## Completed runs + +1. Discovery run (scratch prototype) on frames 506/521/523: greedy + min-excess reduction found 21/31/26 gates in minutes; plain uniform + random trajectories found only 41 on frame 521 in 3,000 trials, + reproducing the weakness of earlier bounded random searches. This was the + evidence pivot from "another random search" to the deterministic + three-phase search. +2. Ten-block search (`search.py`, one process per block): reproduced the + scratch bests exactly and completed all 10,000 trajectories plus the + beam phase on every block. Output: `PASS_R439_BSECTION_MULTWRITE_SEARCH + frames=506,507,519,508,520,509,521,522,523,524 gates=388->262`. + Every candidate's forward matrix was re-derived from its gate list and + compared with the block map inside the search as well. +3. `verify.py --record-certificate`: `PASS_R439_BSECTION_MULTWRITE + gates=388->262 ADDs=24305->24053 columns=661 controls=8 rank_mass=5129 + kappa=unchanged`. The report is pinned in `CERTIFICATE.json`: + - forward positive bound 49,347 -> 26,653; + - composed reverse positive bound 1,113,070 -> 776,006; + - payload 93 -> 90 bits (cap 104); + - records 27,234 -> 26,982; COPY/ERASE pairs 9/9 unchanged; + - paid profile and rank mass 5,129 unchanged; 636 closed frames; + - nine rank-seven copy totals retained. +4. `verify.py` again against the pinned certificate: same PASS line + (certificate match). This is the reproduction command in README.md. +5. `search.py` regeneration reproduced `CANDIDATE.json` identically to the + discovery run's candidates (same seeds, same phases, byte-for-byte gate + lists). + +## Mutation controls (all rejected) + +`mutated_source`, `dropped_gate`, `illegal_frame`, `swapped_block` +(frame-520's program in frame 508's slice), `omitted_cleanup`, +`missing_gate_matching_cleanup`, `illegal_frame_word`, `stale_cleanup`. + +The stale-cleanup control is deliberately informative: the original cleanup +still restores the **F2** endpoint after the splice (every shear is an F2 +involution, so any cleanup inverse to the block's F2 map restores), and is +rejected only by the H4 literal-cleanup comparison. Endpoint checks alone +cannot detect a non-literal cleanup; the two checks are complementary. + +## Development defects caught before the committed runs + +1. The column-subtraction legality test was written with the comparison in + the wrong direction (allowing column growth instead of column + subtraction); caught by hand-checking a two-register case before any + search run. No candidate was produced under the wrong rule. +2. The first draft of the splice replaced B slices in ascending order, which + shifts later slice indices after a shrinking replacement; fixed to + replace from the end of B backwards before the verification run. +3. The negative-control inventory check compared a sorted frame list with + the unsorted B-order list and would have failed on a valid candidate; + fixed before the run. + +## Scope of the evidence + +The finite checks cover the exact integer maps, the complete Boolean block +tables, the full-word F2 endpoint on all 661 dirty-input columns, the H1-H5 +interface of the pinned checker, and the exporter's record bills and +positive/payload bounds. They do not run the C++ native legality or +5/9/11-stage checkers, do not rebuild hosted emission, precision invoices, +supplier bindings or the outer assembly, and do not formalize anything in +Lean. The search is completed coverage of its stated trajectories and beam, +not an impossibility theorem; no block minimum is claimed. diff --git a/research/r439-bsection-multwrite/search.py b/research/r439-bsection-multwrite/search.py new file mode 100644 index 0000000000..0ea75623e6 --- /dev/null +++ b/research/r439-bsection-multwrite/search.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Discovery search for multi-write shear programs on the ten phase-B blocks of +PR589's tuned punctured R439 word. + +Class (strictly larger than the whole-block single-write class of PR #873/#891 +and of PR #880's fixed factor splits, and equal to PR #884/#906's subtraction +class): any program of single-source additive gates `dest += src` on the +block's own registers that realizes the block's exact integer transfer matrix. +Equivalently, any path of legal nonnegative row or column subtractions from +the transfer matrix to the identity. Multi-write interleavings and shared +intermediate rows are inside the class. Programs using registers outside the +block are outside the class. + +Three deterministic phases per block, one Mersenne Twister seeded +`20261013 + frame`: + 1. 6,000 min-excess greedy reductions with random tie-breaks; + 2. 4,000 uniform random legal trajectories (path cap 90); + 3. a width-6,000 beam searching strictly below the incumbent length. + +The stopping rule is complete: all 10,000 trajectories and the beam phase run +to completion for every block; there is no adaptive stopping. "Best found" is +not an impossibility theorem and no minimality is claimed. + +Writes CANDIDATE.json. Deterministic; standard library only. Prepared with +help from opencode. Apache-2.0. +""" +import gzip +import json +import random +from concurrent.futures import ProcessPoolExecutor +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + +# The ten phase-B blocks of the tuned word: frame, first B index, last B index +# (inclusive), in B order. +BLOCKS = [ + (506, 102, 127), + (507, 128, 162), + (519, 163, 204), + (508, 205, 241), + (520, 242, 282), + (509, 283, 313), + (521, 314, 360), + (522, 361, 403), + (523, 404, 448), + (524, 449, 489), +] +GREEDY_TRIALS = 6000 +RANDOM_TRIALS = 4000 +RANDOM_CAP = 90 +BEAM_WIDTH = 6000 +SEED_BASE = 20261013 + + +def load_block(first, last): + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + blk = word["B"][first:last + 1] + assert all(len(ss) == 1 for _, _, ss in blk) + regs = sorted({t for _, t, _ in blk} | {s for _, _, ss in blk for s in ss}) + index = {r: i for i, r in enumerate(regs)} + n = len(regs) + ops = [(index[t], index[ss[0]]) for _, t, ss in blk] + cols = [] + for c in range(n): + x = [int(i == c) for i in range(n)] + for a, b in ops: + x[a] += x[b] + cols.append(x) + matrix = [list(r) for r in zip(*cols)] + return regs, ops, matrix + + +def is_identity(mat): + n = len(mat) + return all(mat[i][j] == (1 if i == j else 0) for i in range(n) for j in range(n)) + + +def excess(mat): + n = len(mat) + return sum(mat[i][j] - (1 if i == j else 0) for i in range(n) for j in range(n)) + + +def legal_moves(mat): + """(kind, t, s): subtract row s from row t ('r'), or column t from + column s ('c'). Both keep the matrix nonnegative and both peel exactly + one gate `t += s`.""" + n = len(mat) + out = [] + for t in range(n): + for s in range(n): + if s == t: + continue + if any(mat[s][j] > 0 for j in range(n)) and all(mat[s][j] <= mat[t][j] for j in range(n)): + out.append(("r", t, s)) + if any(mat[i][t] > 0 for i in range(n)) and all(mat[i][t] <= mat[i][s] for i in range(n)): + out.append(("c", t, s)) + return out + + +def apply_move(mat, move): + kind, t, s = move + n = len(mat) + new = [row[:] for row in mat] + if kind == "r": + for j in range(n): + new[t][j] -= mat[s][j] + else: + for i in range(n): + new[i][s] -= mat[i][t] + return new + + +def greedy(matrix, rng): + cur = matrix + path = [] + while not is_identity(cur): + moves = legal_moves(cur) + if not moves: + return None + scored = [] + for move in moves: + nxt = apply_move(cur, move) + scored.append((excess(nxt), rng.random(), move)) + scored.sort(key=lambda x: (x[0], x[1])) + move = scored[0][2] + cur = apply_move(cur, move) + path.append(move) + if len(path) > 90: + return None + return path + + +def random_traj(matrix, rng, limit): + cur = matrix + path = [] + while not is_identity(cur): + if len(path) >= limit: + return None + moves = legal_moves(cur) + if not moves: + return None + move = moves[rng.randrange(len(moves))] + cur = apply_move(cur, move) + path.append(move) + return path + + +def beam_search(matrix, rng, width, depth_cap): + def key(m): + return tuple(x for row in m for x in row) + layer = [(matrix, [])] + seen = {key(matrix)} + for depth in range(1, depth_cap + 1): + cand = [] + for state, path in layer: + for move in legal_moves(state): + nxt = apply_move(state, move) + k = key(nxt) + if k in seen: + continue + seen.add(k) + cand.append((excess(nxt) + rng.random() * 0.01, nxt, path + [move])) + if not cand: + break + cand.sort(key=lambda x: x[0]) + layer = [(state, p) for _, state, p in cand[:width]] + for state, p in layer: + if is_identity(state): + return depth, p, len(seen) + return None, None, len(seen) + + +def path_to_gates(path): + """Unpeel a reduction path into an apply-order gate list: iterate the path + in reverse; a row peel appends its gate, a column peel prepends it.""" + gates = [] + for kind, t, s in reversed(path): + if kind == "r": + gates.append((t, s)) + else: + gates.insert(0, (t, s)) + return gates + + +def check(matrix, path): + n = len(matrix) + gates = path_to_gates(path) + cols = [] + for c in range(n): + x = [int(i == c) for i in range(n)] + for a, b in gates: + x[a] += x[b] + cols.append(x) + return [list(r) for r in zip(*cols)] == matrix, gates + + +def run_block(spec): + frame, first, last = spec + regs, ops, matrix = load_block(first, last) + rng = random.Random(SEED_BASE + frame) + best = None + hist = {} + dead = 0 + for _ in range(GREEDY_TRIALS): + path = greedy(matrix, rng) + if path is None: + dead += 1 + continue + hist[len(path)] = hist.get(len(path), 0) + 1 + if best is None or len(path) < len(best): + best = path + for _ in range(RANDOM_TRIALS): + path = random_traj(matrix, rng, RANDOM_CAP) + if path is None: + dead += 1 + continue + hist[len(path)] = hist.get(len(path), 0) + 1 + if best is None or len(path) < len(best): + best = path + beam_states = 0 + if best is not None: + _depth, path, beam_states = beam_search(matrix, rng, BEAM_WIDTH, len(best) - 1) + if path is not None: + best = path + hist[len(path)] = hist.get(len(path), 0) + 1 + if best is None: + return {"frame": frame, "slice": [first, last + 1], "registers": regs, + "original_gates": len(ops), "new_gates": None, "dead_ends": dead} + ok, gates = check(matrix, best) + assert ok, frame + touched = sorted({regs[t] for t, _ in gates} | {regs[s] for _, s in gates}) + return { + "frame": frame, + "slice": [first, last + 1], + "registers": regs, + "original_gates": len(ops), + "new_gates": len(best), + "gates": [[frame, regs[t], [regs[s]]] for t, s in gates], + "all_registers_touched": touched == regs, + "histogram": sorted(hist.items()), + "dead_ends": dead, + "beam_states": beam_states, + } + + +def main(): + with ProcessPoolExecutor(max_workers=len(BLOCKS)) as pool: + results = list(pool.map(run_block, BLOCKS)) + results.sort(key=lambda b: b["slice"][0]) + out = { + "schema": "r439-bsection-multwrite/1", + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "source": WORD, + "search": { + "track": "bit supplier (00-19)", + "assignment_seed": 16, + "class": "all programs of single-source additive gates dest += src on the block's own registers realizing the exact integer transfer matrix; equivalently all legal nonnegative row/column subtraction paths to the identity", + "method": f"{GREEDY_TRIALS} min-excess greedy reductions with random tie-breaks, {RANDOM_TRIALS} uniform random legal trajectories (cap {RANDOM_CAP}), then a width-{BEAM_WIDTH} beam below the incumbent", + "seed_rule": f"random.Random({SEED_BASE} + frame) per block (CPython Mersenne Twister)", + "stopping_rule": "all trajectories and the beam phase complete for every block; no adaptive stopping", + "coverage": "all ten phase-B blocks of the pinned tuned word", + "minimality_claimed": False, + }, + "blocks": results, + } + (HERE / "CANDIDATE.json").write_text(json.dumps(out, indent=1) + "\n", encoding="utf-8") + total_old = total_new = 0 + for b in results: + print(b["frame"], b["original_gates"], "->", b["new_gates"], + "touched", b.get("all_registers_touched"), flush=True) + total_old += b["original_gates"] + total_new += b["new_gates"] or b["original_gates"] + print("PASS_R439_BSECTION_MULTWRITE_SEARCH", + f"frames={','.join(str(b['frame']) for b in results)}", + f"gates={total_old}->{total_new}") + + +if __name__ == "__main__": + main() diff --git a/research/r439-bsection-multwrite/verify.py b/research/r439-bsection-multwrite/verify.py new file mode 100644 index 0000000000..16df26084e --- /dev/null +++ b/research/r439-bsection-multwrite/verify.py @@ -0,0 +1,374 @@ +#!/usr/bin/env python3 +"""Independent exact finite verification of the ten multi-write R439 phase-B +block programs. + +The verifier does not import search.py. It pins every consumed source, +re-derives each block's integer transfer map and Boolean truth tables, splices +all ten candidates into one word, rebuilds the literal reverse cleanup, and +rechecks the complete word: frame paths, all 661 arbitrary dirty-input +endpoint columns, the inherited H1-H5 interface, the paid profile and rank +mass, and the exported record bills and positive/payload bounds, with eight +mutation controls. + +Prepared with help from opencode; Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +import struct +import subprocess +import sys +import tempfile +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +CHECKER = "research/e8-bit-p111-tuned/code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + +# frame, first B index, last B index (inclusive) +BLOCKS = [ + (506, 102, 127), + (507, 128, 162), + (519, 163, 204), + (508, 205, 241), + (520, 242, 282), + (509, 283, 313), + (521, 314, 360), + (522, 361, 403), + (523, 404, 448), + (524, 449, 489), +] +EXPECTED_PROFILE = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} +EXPECTED_RANK_MASS = 5129 +EXPECTED_ADDS_BEFORE = 24305 +EXPECTED_ADDS_AFTER = 24053 +EXPECTED_COLUMNS = 661 + + +class Reject(Exception): + pass + + +def need(ok, msg): + if not ok: + raise Reject(msg) + + +def canonical(v): + return json.dumps(v, sort_keys=True, separators=(",", ":")).encode() + + +def digest(v): + return hashlib.sha256(canonical(v)).hexdigest() + + +def matrix(ops, n): + cols = [] + for c in range(n): + x = [int(i == c) for i in range(n)] + for a, b in ops: + need(type(a) is int and type(b) is int and 0 <= a < n and 0 <= b < n and a != b, + "invalid operation") + x[a] += x[b] + cols.append(x) + return [list(r) for r in zip(*cols)] + + +def pins(): + s = json.loads((HERE / "SOURCES.json").read_text()) + need(s["base_commit"] == "007664306fff84fbb1c9a1b4053b69f439764034", "base pin") + for p, h in s["files"].items(): + need(hashlib.sha256((ROOT / p).read_bytes()).hexdigest() == h, "source pin: " + p) + + +def bind_block(word, entry): + frame, first, last = entry["_block"] + need(entry["frame"] == frame and entry["slice"] == [first, last + 1], "block binding") + old = word["B"][first:last + 1] + need(all(f == frame and len(ss) == 1 for f, _, ss in old), "source block") + regs = sorted({t for _, t, _ in old} | {s for _, _, ss in old for s in ss}) + need(entry["registers"] == regs, "register binding") + need(entry["original_gates"] == len(old), "original gate count") + index = {r: i for i, r in enumerate(regs)} + n = len(regs) + old_ops = [(index[t], index[ss[0]]) for _, t, ss in old] + newg = entry["gates"] + need(type(entry["new_gates"]) is int and len(newg) == entry["new_gates"] < len(old), + "candidate gate count") + need(all(f == frame and d in index and len(ss) == 1 and ss[0] in index and d != ss[0] + for f, d, ss in newg), "candidate shape") + new_ops = [(index[d], index[ss[0]]) for _, d, ss in newg] + mo, mn = matrix(old_ops, n), matrix(new_ops, n) + need(mo == mn, "integer map " + str(frame)) + for val in range(1 << n): + a = [(val >> i) & 1 for i in range(n)] + b = list(a) + for ops, state in ((old_ops, a), (new_ops, b)): + for d, s in ops: + state[d] ^= state[s] + need(a == b, "F2 table " + str(frame)) + ro, rn = matrix(old_ops[::-1], n), matrix(new_ops[::-1], n) + touched = sorted({regs[t] for t, _ in new_ops} | {regs[s] for _, s in new_ops}) + need(touched == regs and entry["all_registers_touched"] is True, + "all registers touched " + str(frame)) + return { + "frame": frame, + "slice": [first, last + 1], + "registers": regs, + "original_gates": len(old_ops), + "new_gates": len(new_ops), + "boolean_inputs_checked": 1 << n, + "forward_integer_sha256": digest(mo), + "reverse_old_total": sum(map(sum, ro)), + "reverse_new_total": sum(map(sum, rn)), + "reverse_entrywise_dominated": all(x <= y for p, q in zip(rn, ro) for x, y in zip(p, q)), + } + + +def cleanup(w): + full = next(i for i, f in enumerate(w["frames"]) if len(f) == w["v"]) + return [[full, d, list(ss)] for _, d, ss in reversed(w["A"] + w["B"]) if d < w["v"] or d >= 2 * w["v"]] + + +def candidate_word(word, cand): + w = copy.deepcopy(word) + for entry in sorted(cand["blocks"], key=lambda b: b["slice"][0], reverse=True): + first, last = entry["slice"] + w["B"][first:last] = copy.deepcopy(entry["gates"]) + w["C"] = cleanup(w) + return w + + +def paths(w): + fs = list(map(set, w["frames"])) + ps = [[f] for f in w["start"]] + + def move(r, f): + if ps[r][-1] != f: + need(fs[ps[r][-1]] < fs[f], "illegal frame move") + ps[r].append(f) + + for k in "DABC": + for f, d, ss in w[k]: + for r in [d, *ss]: + move(r, f) + for r, f in enumerate(w["final"]): + move(r, f) + return ps + + +def endpoint(w): + n = 2 * w["v"] + w["R"] + v = w["v"] + state = [{i} for i in range(n)] + + def run(k): + for _, d, ss in w[k]: + for s in ss: + state[d].symmetric_difference_update(state[s]) + + run("D") + run("A") + snap = [state[r].copy() for r in w["ret"]] + for t, reads in enumerate(w["scatter"]): + for k in reads: + state[v + t].symmetric_difference_update(snap[k]) + run("B") + run("C") + for r, x in enumerate(state): + need(x == ({r, r - v} if v <= r < 2 * v else {r}), "endpoint register " + str(r)) + return n + + +def checker(): + s = importlib.util.spec_from_file_location("r439_owner_checker", ROOT / CHECKER) + m = importlib.util.module_from_spec(s) + s.loader.exec_module(m) + return m + + +def bill(w, out): + out.mkdir(parents=True) + wp = out / "word.json.gz" + wp.write_bytes(gzip.compress(canonical(w), mtime=0)) + subprocess.run([sys.executable, "-I", "-B", str(ROOT / EXPORTER), str(wp), str(out / "records")], + check=True, capture_output=True, text=True) + raw = (out / "records/249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "record alignment") + rec = list(struct.iter_unpack("<6i", raw)) + n = 2 * w["v"] + w["R"] + bounds = [] + for rev in (False, True): + norms = [1] * (n + 1) + maximum = 1 + opened = False + for op, a, b, c, _, _ in (reversed(rec) if rev else rec): + if op == 0: + continue + if rev and op in (2, 3): + op = 5 - op + if op == 1: + norms[a] += abs(c) * norms[b] + maximum = max(maximum, norms[a]) + elif op == 2: + need(not opened, "nested copy") + norms[b] = norms[a] + opened = True + elif op == 3: + need(opened, "erase without copy") + norms[b] = 0 + opened = False + else: + raise Reject("record opcode") + need(not opened, "unclosed copy") + bounds.append(maximum) + payload = 64 * bounds[0] ** 3 * bounds[1] ** 2 + need(payload < 1 << 104, "payload cap") + return {"records": len(rec), + "adds": sum(x[0] == 1 for x in rec), + "copies": sum(x[0] == 2 for x in rec), + "erasures": sum(x[0] == 3 for x in rec), + "forward_positive_bound": bounds[0], + "reverse_positive_bound": bounds[1], + "payload_bits": payload.bit_length(), + "record_sha256": hashlib.sha256(raw).hexdigest()}, rec + + +def reject(name, fn): + try: + fn() + except Reject: + return name + raise Reject("negative control accepted: " + name) + + +def verify(out): + pins() + cand = json.loads((HERE / "CANDIDATE.json").read_text()) + need(cand["base_commit"] == "007664306fff84fbb1c9a1b4053b69f439764034", "candidate base pin") + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + by_frame = {} + for spec in BLOCKS: + entry = dict(cand["blocks"][[b["frame"] for b in cand["blocks"]].index(spec[0])]) + entry["_block"] = spec + by_frame[spec[0]] = entry + need(set(by_frame) == {b[0] for b in BLOCKS} and len(cand["blocks"]) == len(BLOCKS), + "block inventory") + blocks = [bind_block(word, by_frame[frame]) for frame, _, _ in BLOCKS] + w = candidate_word(word, cand) + need(all(w[k] == word[k] for k in word if k not in ("B", "C")), "unrelated field") + need(w["C"] == cleanup(w), "literal cleanup") + p0, p1 = paths(word), paths(w) + need(p0 == p1, "frame paths") + endpoint(word) + columns = endpoint(w) + need(columns == EXPECTED_COLUMNS, "column count") + dim, labels, flow, hyp, con, _ = checker().check(w) + need(all(hyp.values()) and all(con.values()), "H1-H5 interface") + profile = Counter(dim.fdim[b] - dim.fdim[a] for p in p1 for a, b in itertools.pairwise(p)) + profile.update(t["rank"] for t in flow["totals"]) + need(dict(sorted(profile.items())) == EXPECTED_PROFILE, "profile") + need(sum(k * v for k, v in profile.items()) == EXPECTED_RANK_MASS, "rank mass") + before, r0 = bill(word, out / "before") + after, r1 = bill(w, out / "after") + need((before["adds"], after["adds"]) == (EXPECTED_ADDS_BEFORE, EXPECTED_ADDS_AFTER), "ADD bill") + need(before["copies"] == after["copies"] == 9 and before["erasures"] == after["erasures"] == 9, + "copy bill") + need(Counter(x for x in r0 if x[0] != 1) == Counter(x for x in r1 if x[0] != 1), "non-ADD events") + need(after["forward_positive_bound"] <= before["forward_positive_bound"], "forward bound") + need(after["payload_bits"] <= 104, "payload bits") + controls = [] + bad = copy.deepcopy(cand) + regs0 = bad["blocks"][0]["registers"] + cur = bad["blocks"][0]["gates"][0][2][0] + bad["blocks"][0]["gates"][0][2] = [next(r for r in regs0 if r not in (cur, bad["blocks"][0]["gates"][0][1]))] + controls.append(reject("mutated_source", lambda: bind_block(word, self_bind(bad["blocks"][0], BLOCKS[0])))) + bad = copy.deepcopy(cand) + bad["blocks"][1]["gates"].pop() + bad["blocks"][1]["new_gates"] -= 1 + controls.append(reject("dropped_gate", lambda: bind_block(word, self_bind(bad["blocks"][1], BLOCKS[1])))) + bad = copy.deepcopy(cand) + bad["blocks"][2]["gates"][0][0] = 0 + controls.append(reject("illegal_frame", lambda: bind_block(word, self_bind(bad["blocks"][2], BLOCKS[2])))) + bad = copy.deepcopy(cand) + bad["blocks"][3]["gates"], bad["blocks"][3]["new_gates"] = bad["blocks"][4]["gates"], bad["blocks"][4]["new_gates"] + controls.append(reject("swapped_block", lambda: bind_block(word, self_bind(bad["blocks"][3], BLOCKS[3])))) + bad = copy.deepcopy(w) + bad["C"].pop() + controls.append(reject("omitted_cleanup", lambda: endpoint(bad))) + first, last = BLOCKS[0][1], BLOCKS[0][2] + bad = copy.deepcopy(w) + del bad["B"][first] + bad["C"] = cleanup(bad) + controls.append(reject("missing_gate_matching_cleanup", lambda: endpoint(bad))) + bad = copy.deepcopy(w) + bad["B"][first][0] = 0 + controls.append(reject("illegal_frame_word", lambda: paths(bad))) + stale = copy.deepcopy(w) + stale["C"] = word["C"] + endpoint(stale) + controls.append(reject("stale_cleanup", lambda: need(stale["C"] == cleanup(stale), "H4"))) + return { + "status": "PASS_R439_BSECTION_MULTWRITE", + "base_commit": cand["base_commit"], + "assignment_seed": 16, + "blocks": blocks, + "columns": columns, + "closed_frames": labels["frames"], + "copy_ranks": [t["rank"] for t in flow["totals"]], + "paid_profile": {str(k): v for k, v in sorted(profile.items())}, + "rank_mass": EXPECTED_RANK_MASS, + "identical_register_frame_paths": len(p1), + "hypotheses": hyp, + "conclusion": con, + "before": before, + "after": after, + "adds_saved": before["adds"] - after["adds"], + "new_kappa_claim": False, + "candidate_content_sha256": digest(w), + "negative_controls": controls, + "search": cand["search"], + } + + +def self_bind(entry, spec): + entry = dict(entry) + entry["_block"] = spec + return entry + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--out", type=Path) + ap.add_argument("--record-certificate", action="store_true") + a = ap.parse_args() + if a.out: + need(not a.out.exists(), "output exists") + out = a.out + else: + tmp = tempfile.TemporaryDirectory(prefix="r439-bsec-") + out = Path(tmp.name) + report = verify(out) + cert = HERE / "CERTIFICATE.json" + if a.record_certificate: + need(not cert.exists(), "certificate exists") + cert.write_text(json.dumps(report, indent=2) + "\n", encoding="utf-8") + else: + need(report == json.loads(cert.read_text()), "certificate mismatch") + print("PASS_R439_BSECTION_MULTWRITE", + "gates=%d->%d ADDs=%d->%d columns=%d controls=%d rank_mass=%d kappa=unchanged" % ( + sum(b["original_gates"] for b in report["blocks"]), + sum(b["new_gates"] for b in report["blocks"]), + report["before"]["adds"], report["after"]["adds"], + report["columns"], len(report["negative_controls"]), report["rank_mass"])) + + +if __name__ == "__main__": + main()