diff --git a/research/r439-bsection-survey/CANDIDATES.json b/research/r439-bsection-survey/CANDIDATES.json new file mode 100644 index 0000000000..7e7d3d1731 --- /dev/null +++ b/research/r439-bsection-survey/CANDIDATES.json @@ -0,0 +1,1703 @@ +{ + "source": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "source_content_sha256": "5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b", + "blocks": [ + { + "frame": 506, + "slice": [ + 102, + 128 + ], + "registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "original_gates": 26, + "forward_sha256": "3a753476d03618495a38142694ca45b0aefb0d446812bd87598ccba69bccfdd7", + "diagonal": [ + 2, + 1, + 2, + 2, + 2, + 2, + 1, + 2, + 2, + 2 + ], + "class_covered": true, + "minimum": 24, + "saving": 2, + "candidate_gates": [ + [ + 506, + 52, + [ + 5 + ] + ], + [ + 506, + 52, + [ + 6 + ] + ], + [ + 506, + 52, + [ + 9 + ] + ], + [ + 506, + 52, + [ + 46 + ] + ], + [ + 506, + 52, + [ + 47 + ] + ], + [ + 506, + 52, + [ + 48 + ] + ], + [ + 506, + 52, + [ + 54 + ] + ], + [ + 506, + 52, + [ + 56 + ] + ], + [ + 506, + 52, + [ + 58 + ] + ], + [ + 506, + 5, + [ + 9 + ] + ], + [ + 506, + 5, + [ + 52 + ] + ], + [ + 506, + 9, + [ + 6 + ] + ], + [ + 506, + 9, + [ + 52 + ] + ], + [ + 506, + 47, + [ + 46 + ] + ], + [ + 506, + 47, + [ + 48 + ] + ], + [ + 506, + 47, + [ + 52 + ] + ], + [ + 506, + 54, + [ + 52 + ] + ], + [ + 506, + 46, + [ + 54 + ] + ], + [ + 506, + 46, + [ + 56 + ] + ], + [ + 506, + 58, + [ + 48 + ] + ], + [ + 506, + 58, + [ + 52 + ] + ], + [ + 506, + 48, + [ + 5 + ] + ], + [ + 506, + 48, + [ + 6 + ] + ], + [ + 506, + 56, + [ + 52 + ] + ] + ], + "local_gates": [ + [ + 6, + 0 + ], + [ + 6, + 1 + ], + [ + 6, + 2 + ], + [ + 6, + 3 + ], + [ + 6, + 4 + ], + [ + 6, + 5 + ], + [ + 6, + 7 + ], + [ + 6, + 8 + ], + [ + 6, + 9 + ], + [ + 0, + 2 + ], + [ + 0, + 6 + ], + [ + 2, + 1 + ], + [ + 2, + 6 + ], + [ + 4, + 3 + ], + [ + 4, + 5 + ], + [ + 4, + 6 + ], + [ + 7, + 6 + ], + [ + 3, + 7 + ], + [ + 3, + 8 + ], + [ + 9, + 5 + ], + [ + 9, + 6 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 8, + 6 + ] + ], + "realization_order": [ + 52, + 5, + 6, + 9, + 47, + 54, + 46, + 58, + 48, + 56 + ], + "donors": { + "52": [ + 5, + 6, + 9, + 46, + 47, + 48, + 54, + 56, + 58 + ], + "5": [ + 9, + 52 + ], + "6": [], + "9": [ + 6, + 52 + ], + "47": [ + 46, + 48, + 52 + ], + "54": [ + 52 + ], + "46": [ + 54, + 56 + ], + "58": [ + 48, + 52 + ], + "48": [ + 5, + 6 + ], + "56": [ + 52 + ] + }, + "touched_registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "all_registers_touched": true, + "states": 1024, + "state_destination_pairs": 5120, + "feasible_edges": 1795, + "distances_sha256": "592bd1814910e3d6047ced3cbe23fd65d74340c45d925f1aac8d96baed21655b" + }, + { + "frame": 507, + "slice": [ + 128, + 163 + ], + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "original_gates": 35, + "forward_sha256": "092a132d3ad8cc9617fdb389d1fa47147ecb7ffeeb02aaa74f7596366bf820c7", + "diagonal": [ + 2, + 1, + 3, + 1, + 3, + 1, + 1, + 1, + 2, + 1 + ], + "class_covered": false, + "supply_witness": { + "row": 3, + "col": 4, + "demand": 3, + "supply": 1 + } + }, + { + "frame": 519, + "slice": [ + 163, + 205 + ], + "registers": [ + 15, + 23, + 30, + 41, + 49, + 53, + 59, + 70, + 75, + 82, + 91, + 96 + ], + "original_gates": 42, + "forward_sha256": "e15c9a30d0d0e44daf32d2b4125f9b69263d48e7487b0b91b49e7e9ba9397648", + "diagonal": [ + 1, + 2, + 1, + 2, + 2, + 2, + 1, + 2, + 2, + 1, + 1, + 1 + ], + "class_covered": false, + "supply_witness": { + "row": 2, + "col": 8, + "demand": 2, + "supply": 1 + } + }, + { + "frame": 508, + "slice": [ + 205, + 242 + ], + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "original_gates": 37, + "forward_sha256": "21ec3c5628db324d406f10bdd4fb28c61d14a41ab7f42e509ccdc38231a652e2", + "diagonal": [ + 1, + 1, + 3, + 3, + 1, + 1, + 1, + 3, + 1, + 2, + 1 + ], + "class_covered": true, + "minimum": 30, + "saving": 7, + "candidate_gates": [ + [ + 508, + 66, + [ + 19 + ] + ], + [ + 508, + 66, + [ + 35 + ] + ], + [ + 508, + 66, + [ + 43 + ] + ], + [ + 508, + 66, + [ + 57 + ] + ], + [ + 508, + 66, + [ + 65 + ] + ], + [ + 508, + 66, + [ + 74 + ] + ], + [ + 508, + 66, + [ + 97 + ] + ], + [ + 508, + 89, + [ + 19 + ] + ], + [ + 508, + 89, + [ + 27 + ] + ], + [ + 508, + 89, + [ + 35 + ] + ], + [ + 508, + 89, + [ + 43 + ] + ], + [ + 508, + 89, + [ + 74 + ] + ], + [ + 508, + 89, + [ + 97 + ] + ], + [ + 508, + 466, + [ + 43 + ] + ], + [ + 508, + 466, + [ + 66 + ] + ], + [ + 508, + 466, + [ + 89 + ] + ], + [ + 508, + 466, + [ + 97 + ] + ], + [ + 508, + 43, + [ + 19 + ] + ], + [ + 508, + 43, + [ + 66 + ] + ], + [ + 508, + 43, + [ + 89 + ] + ], + [ + 508, + 43, + [ + 97 + ] + ], + [ + 508, + 74, + [ + 43 + ] + ], + [ + 508, + 35, + [ + 27 + ] + ], + [ + 508, + 35, + [ + 74 + ] + ], + [ + 508, + 35, + [ + 97 + ] + ], + [ + 508, + 27, + [ + 66 + ] + ], + [ + 508, + 57, + [ + 89 + ] + ], + [ + 508, + 65, + [ + 89 + ] + ], + [ + 508, + 97, + [ + 19 + ] + ], + [ + 508, + 97, + [ + 27 + ] + ] + ], + "local_gates": [ + [ + 6, + 0 + ], + [ + 6, + 2 + ], + [ + 6, + 3 + ], + [ + 6, + 4 + ], + [ + 6, + 5 + ], + [ + 6, + 7 + ], + [ + 6, + 9 + ], + [ + 8, + 0 + ], + [ + 8, + 1 + ], + [ + 8, + 2 + ], + [ + 8, + 3 + ], + [ + 8, + 7 + ], + [ + 8, + 9 + ], + [ + 10, + 3 + ], + [ + 10, + 6 + ], + [ + 10, + 8 + ], + [ + 10, + 9 + ], + [ + 3, + 0 + ], + [ + 3, + 6 + ], + [ + 3, + 8 + ], + [ + 3, + 9 + ], + [ + 7, + 3 + ], + [ + 2, + 1 + ], + [ + 2, + 7 + ], + [ + 2, + 9 + ], + [ + 1, + 6 + ], + [ + 4, + 8 + ], + [ + 5, + 8 + ], + [ + 9, + 0 + ], + [ + 9, + 1 + ] + ], + "realization_order": [ + 19, + 66, + 89, + 466, + 43, + 74, + 35, + 27, + 57, + 65, + 97 + ], + "donors": { + "19": [], + "66": [ + 19, + 35, + 43, + 57, + 65, + 74, + 97 + ], + "89": [ + 19, + 27, + 35, + 43, + 74, + 97 + ], + "466": [ + 43, + 66, + 89, + 97 + ], + "43": [ + 19, + 66, + 89, + 97 + ], + "74": [ + 43 + ], + "35": [ + 27, + 74, + 97 + ], + "27": [ + 66 + ], + "57": [ + 89 + ], + "65": [ + 89 + ], + "97": [ + 19, + 27 + ] + }, + "touched_registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "all_registers_touched": true, + "states": 2048, + "state_destination_pairs": 11264, + "feasible_edges": 1616, + "distances_sha256": "535c32b15e7f6491093e7d92326184d15cb18d35376038a237d9420bbed3044e" + }, + { + "frame": 520, + "slice": [ + 242, + 283 + ], + "registers": [ + 21, + 26, + 36, + 44, + 51, + 55, + 64, + 71, + 80, + 84, + 94, + 102 + ], + "original_gates": 41, + "forward_sha256": "61daed3b32c4e46b352205c2aa1034b7288f297857471c2dfc5d18fed3e033e5", + "diagonal": [ + 2, + 1, + 3, + 2, + 1, + 1, + 1, + 1, + 2, + 2, + 1, + 1 + ], + "class_covered": false, + "supply_witness": { + "row": 9, + "col": 9, + "demand": 1, + "supply": 0 + } + }, + { + "frame": 509, + "slice": [ + 283, + 314 + ], + "registers": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92, + 468 + ], + "original_gates": 31, + "forward_sha256": "fcfbd9158c9dd5b1c963e2db42d9065fb89e144a436e120dd3de7c2fee7110fb", + "diagonal": [ + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 2, + 1, + 2, + 1 + ], + "class_covered": false, + "supply_witness": null + }, + { + "frame": 521, + "slice": [ + 314, + 361 + ], + "registers": [ + 10, + 13, + 32, + 34, + 39, + 42, + 76, + 79, + 83, + 85, + 104, + 107 + ], + "original_gates": 47, + "forward_sha256": "3aca7fadf5d79b1dac43414e6dd7e9035c1be97afd39b8ceeb9436f5f5370d99", + "diagonal": [ + 2, + 2, + 2, + 3, + 1, + 2, + 2, + 1, + 1, + 2, + 2, + 3 + ], + "class_covered": false, + "supply_witness": null + }, + { + "frame": 522, + "slice": [ + 361, + 404 + ], + "registers": [ + 1, + 7, + 24, + 25, + 28, + 29, + 98, + 99, + 100, + 101, + 106, + 108 + ], + "original_gates": 43, + "forward_sha256": "2ed5aba7410132ceb6d54d465892600c6665da60fdb78bf7c842c4effdd6cd7c", + "diagonal": [ + 2, + 2, + 2, + 3, + 1, + 1, + 2, + 2, + 2, + 2, + 1, + 3 + ], + "class_covered": false, + "supply_witness": { + "row": 5, + "col": 3, + "demand": 2, + "supply": 1 + } + }, + { + "frame": 523, + "slice": [ + 404, + 449 + ], + "registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "original_gates": 45, + "forward_sha256": "ec4919a2b7ba73cc9b25fd99b7d64d5bc7a8b0d38a1185078a61fb9a19feaa63", + "diagonal": [ + 1, + 2, + 2, + 2, + 2, + 1, + 3, + 1, + 3, + 2, + 1, + 2 + ], + "class_covered": true, + "minimum": 39, + "saving": 6, + "candidate_gates": [ + [ + 523, + 103, + [ + 2 + ] + ], + [ + 523, + 103, + [ + 4 + ] + ], + [ + 523, + 103, + [ + 16 + ] + ], + [ + 523, + 103, + [ + 18 + ] + ], + [ + 523, + 103, + [ + 88 + ] + ], + [ + 523, + 103, + [ + 93 + ] + ], + [ + 523, + 103, + [ + 109 + ] + ], + [ + 523, + 2, + [ + 4 + ] + ], + [ + 523, + 2, + [ + 14 + ] + ], + [ + 523, + 2, + [ + 16 + ] + ], + [ + 523, + 2, + [ + 18 + ] + ], + [ + 523, + 2, + [ + 20 + ] + ], + [ + 523, + 2, + [ + 88 + ] + ], + [ + 523, + 2, + [ + 90 + ] + ], + [ + 523, + 2, + [ + 93 + ] + ], + [ + 523, + 2, + [ + 95 + ] + ], + [ + 523, + 4, + [ + 2 + ] + ], + [ + 523, + 20, + [ + 14 + ] + ], + [ + 523, + 20, + [ + 88 + ] + ], + [ + 523, + 20, + [ + 90 + ] + ], + [ + 523, + 20, + [ + 95 + ] + ], + [ + 523, + 20, + [ + 103 + ] + ], + [ + 523, + 93, + [ + 2 + ] + ], + [ + 523, + 93, + [ + 16 + ] + ], + [ + 523, + 93, + [ + 18 + ] + ], + [ + 523, + 93, + [ + 88 + ] + ], + [ + 523, + 93, + [ + 103 + ] + ], + [ + 523, + 88, + [ + 18 + ] + ], + [ + 523, + 88, + [ + 20 + ] + ], + [ + 523, + 14, + [ + 18 + ] + ], + [ + 523, + 14, + [ + 88 + ] + ], + [ + 523, + 14, + [ + 90 + ] + ], + [ + 523, + 16, + [ + 20 + ] + ], + [ + 523, + 95, + [ + 18 + ] + ], + [ + 523, + 95, + [ + 88 + ] + ], + [ + 523, + 109, + [ + 18 + ] + ], + [ + 523, + 109, + [ + 88 + ] + ], + [ + 523, + 18, + [ + 20 + ] + ], + [ + 523, + 90, + [ + 103 + ] + ] + ], + "local_gates": [ + [ + 10, + 0 + ], + [ + 10, + 1 + ], + [ + 10, + 3 + ], + [ + 10, + 4 + ], + [ + 10, + 6 + ], + [ + 10, + 8 + ], + [ + 10, + 11 + ], + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 7 + ], + [ + 0, + 8 + ], + [ + 0, + 9 + ], + [ + 1, + 0 + ], + [ + 5, + 2 + ], + [ + 5, + 6 + ], + [ + 5, + 7 + ], + [ + 5, + 9 + ], + [ + 5, + 10 + ], + [ + 8, + 0 + ], + [ + 8, + 3 + ], + [ + 8, + 4 + ], + [ + 8, + 6 + ], + [ + 8, + 10 + ], + [ + 6, + 4 + ], + [ + 6, + 5 + ], + [ + 2, + 4 + ], + [ + 2, + 6 + ], + [ + 2, + 7 + ], + [ + 3, + 5 + ], + [ + 9, + 4 + ], + [ + 9, + 6 + ], + [ + 11, + 4 + ], + [ + 11, + 6 + ], + [ + 4, + 5 + ], + [ + 7, + 10 + ] + ], + "realization_order": [ + 103, + 2, + 4, + 20, + 93, + 88, + 14, + 16, + 95, + 109, + 18, + 90 + ], + "donors": { + "103": [ + 2, + 4, + 16, + 18, + 88, + 93, + 109 + ], + "2": [ + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95 + ], + "4": [ + 2 + ], + "20": [ + 14, + 88, + 90, + 95, + 103 + ], + "93": [ + 2, + 16, + 18, + 88, + 103 + ], + "88": [ + 18, + 20 + ], + "14": [ + 18, + 88, + 90 + ], + "16": [ + 20 + ], + "95": [ + 18, + 88 + ], + "109": [ + 18, + 88 + ], + "18": [ + 20 + ], + "90": [ + 103 + ] + }, + "touched_registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "all_registers_touched": true, + "states": 4096, + "state_destination_pairs": 24576, + "feasible_edges": 1152, + "distances_sha256": "6e08d3d04e056aa4838cce87b4a5ac72b9f5338d5de2c7ea6970bacf6352db31" + }, + { + "frame": 524, + "slice": [ + 449, + 490 + ], + "registers": [ + 8, + 12, + 31, + 37, + 40, + 45, + 73, + 78, + 81, + 86, + 105, + 110 + ], + "original_gates": 41, + "forward_sha256": "ec348a4eebe4a9fb7e13c63a47d0cc4da12cbcd47ce9d5980e1f0baf5b7a181d", + "diagonal": [ + 2, + 2, + 1, + 2, + 1, + 1, + 2, + 3, + 2, + 3, + 2, + 1 + ], + "class_covered": false, + "supply_witness": { + "row": 6, + "col": 9, + "demand": 3, + "supply": 2 + } + } + ] +} diff --git a/research/r439-bsection-survey/CERTIFICATE.json b/research/r439-bsection-survey/CERTIFICATE.json new file mode 100644 index 0000000000..da069b0a64 --- /dev/null +++ b/research/r439-bsection-survey/CERTIFICATE.json @@ -0,0 +1,735 @@ +{ + "schema": "r439-bsection-survey/1", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_sha256": { + "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" + }, + "blocks": [ + { + "section": "B", + "frame": 506, + "slice": [ + 102, + 128 + ], + "registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "original_gates": 26, + "spliced": true, + "status": "class-minimum", + "minimum": 24, + "gates": [ + [ + 506, + 52, + [ + 5 + ] + ], + [ + 506, + 52, + [ + 6 + ] + ], + [ + 506, + 52, + [ + 9 + ] + ], + [ + 506, + 52, + [ + 46 + ] + ], + [ + 506, + 52, + [ + 47 + ] + ], + [ + 506, + 52, + [ + 48 + ] + ], + [ + 506, + 52, + [ + 54 + ] + ], + [ + 506, + 52, + [ + 56 + ] + ], + [ + 506, + 52, + [ + 58 + ] + ], + [ + 506, + 5, + [ + 9 + ] + ], + [ + 506, + 5, + [ + 52 + ] + ], + [ + 506, + 9, + [ + 6 + ] + ], + [ + 506, + 9, + [ + 52 + ] + ], + [ + 506, + 47, + [ + 46 + ] + ], + [ + 506, + 47, + [ + 48 + ] + ], + [ + 506, + 47, + [ + 52 + ] + ], + [ + 506, + 54, + [ + 52 + ] + ], + [ + 506, + 46, + [ + 54 + ] + ], + [ + 506, + 46, + [ + 56 + ] + ], + [ + 506, + 58, + [ + 48 + ] + ], + [ + 506, + 58, + [ + 52 + ] + ], + [ + 506, + 48, + [ + 5 + ] + ], + [ + 506, + 48, + [ + 6 + ] + ], + [ + 506, + 56, + [ + 52 + ] + ] + ] + }, + { + "section": "B", + "frame": 507, + "slice": [ + 128, + 163 + ], + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "original_gates": 35, + "spliced": false, + "status": "infeasible", + "witness": { + "row": 3, + "col": 4, + "demand": 3, + "supply": 1 + } + }, + { + "section": "B", + "frame": 519, + "slice": [ + 163, + 205 + ], + "registers": [ + 15, + 23, + 30, + 41, + 49, + 53, + 59, + 70, + 75, + 82, + 91, + 96 + ], + "original_gates": 42, + "spliced": false, + "status": "infeasible", + "witness": { + "row": 2, + "col": 8, + "demand": 2, + "supply": 1 + } + }, + { + "section": "B", + "frame": 508, + "slice": [ + 205, + 242 + ], + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "original_gates": 37, + "spliced": false, + "status": "class-minimum", + "minimum": 30 + }, + { + "section": "B", + "frame": 520, + "slice": [ + 242, + 283 + ], + "registers": [ + 21, + 26, + 36, + 44, + 51, + 55, + 64, + 71, + 80, + 84, + 94, + 102 + ], + "original_gates": 41, + "spliced": false, + "status": "infeasible", + "witness": { + "row": 9, + "col": 9, + "demand": 1, + "supply": 0 + } + }, + { + "section": "B", + "frame": 509, + "slice": [ + 283, + 314 + ], + "registers": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92, + 468 + ], + "original_gates": 31, + "spliced": false, + "status": "infeasible", + "witness": null + }, + { + "section": "B", + "frame": 521, + "slice": [ + 314, + 361 + ], + "registers": [ + 10, + 13, + 32, + 34, + 39, + 42, + 76, + 79, + 83, + 85, + 104, + 107 + ], + "original_gates": 47, + "spliced": false, + "status": "infeasible", + "witness": null + }, + { + "section": "B", + "frame": 522, + "slice": [ + 361, + 404 + ], + "registers": [ + 1, + 7, + 24, + 25, + 28, + 29, + 98, + 99, + 100, + 101, + 106, + 108 + ], + "original_gates": 43, + "spliced": false, + "status": "infeasible", + "witness": { + "row": 5, + "col": 3, + "demand": 2, + "supply": 1 + } + }, + { + "section": "B", + "frame": 523, + "slice": [ + 404, + 449 + ], + "registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "original_gates": 45, + "spliced": true, + "status": "class-minimum", + "minimum": 39, + "gates": [ + [ + 523, + 103, + [ + 2 + ] + ], + [ + 523, + 103, + [ + 4 + ] + ], + [ + 523, + 103, + [ + 16 + ] + ], + [ + 523, + 103, + [ + 18 + ] + ], + [ + 523, + 103, + [ + 88 + ] + ], + [ + 523, + 103, + [ + 93 + ] + ], + [ + 523, + 103, + [ + 109 + ] + ], + [ + 523, + 2, + [ + 4 + ] + ], + [ + 523, + 2, + [ + 14 + ] + ], + [ + 523, + 2, + [ + 16 + ] + ], + [ + 523, + 2, + [ + 18 + ] + ], + [ + 523, + 2, + [ + 20 + ] + ], + [ + 523, + 2, + [ + 88 + ] + ], + [ + 523, + 2, + [ + 90 + ] + ], + [ + 523, + 2, + [ + 93 + ] + ], + [ + 523, + 2, + [ + 95 + ] + ], + [ + 523, + 4, + [ + 2 + ] + ], + [ + 523, + 20, + [ + 14 + ] + ], + [ + 523, + 20, + [ + 88 + ] + ], + [ + 523, + 20, + [ + 90 + ] + ], + [ + 523, + 20, + [ + 95 + ] + ], + [ + 523, + 20, + [ + 103 + ] + ], + [ + 523, + 93, + [ + 2 + ] + ], + [ + 523, + 93, + [ + 16 + ] + ], + [ + 523, + 93, + [ + 18 + ] + ], + [ + 523, + 93, + [ + 88 + ] + ], + [ + 523, + 93, + [ + 103 + ] + ], + [ + 523, + 88, + [ + 18 + ] + ], + [ + 523, + 88, + [ + 20 + ] + ], + [ + 523, + 14, + [ + 18 + ] + ], + [ + 523, + 14, + [ + 88 + ] + ], + [ + 523, + 14, + [ + 90 + ] + ], + [ + 523, + 16, + [ + 20 + ] + ], + [ + 523, + 95, + [ + 18 + ] + ], + [ + 523, + 95, + [ + 88 + ] + ], + [ + 523, + 109, + [ + 18 + ] + ], + [ + 523, + 109, + [ + 88 + ] + ], + [ + 523, + 18, + [ + 20 + ] + ], + [ + 523, + 90, + [ + 103 + ] + ] + ] + }, + { + "section": "B", + "frame": 524, + "slice": [ + 449, + 490 + ], + "registers": [ + 8, + 12, + 31, + 37, + 40, + 45, + 73, + 78, + 81, + 86, + 105, + 110 + ], + "original_gates": 41, + "spliced": false, + "status": "infeasible", + "witness": { + "row": 6, + "col": 9, + "demand": 3, + "supply": 2 + } + } + ] +} diff --git a/research/r439-bsection-survey/CLAIM.md b/research/r439-bsection-survey/CLAIM.md new file mode 100644 index 0000000000..a5ef521742 --- /dev/null +++ b/research/r439-bsection-survey/CLAIM.md @@ -0,0 +1,39 @@ +# Sprint scope claim (recorded locally) + +No pinned sprint coordination issue exists (checked 2026-10-13; the only open +issue is #650, unrelated), so the scope claim is recorded here, per the sprint +protocol. + +- Track and seed: **bit supplier (00-19), OS random seed 8**. +- Base commit: `f567884aeb8851b6e794af1184119a3bfbe1e631` (origin/main at + sprint start; selected PR799/PR589, conditional kappa + 0.001661634653669567). +- 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 + runs at frames 506-509 and 519-524. +- Method: whole-block single-write class (PR #873's formulation) searched by + a realized-subset dynamic program with meet-in-the-middle donor sums; + class-infeasibility by two independent exhaustive recursions plus + order-independent per-row donor-supply certificates. +- Parameter range: all ten phase-B blocks of the word; constructions spliced + only for frames 506 and 523. +- Expected deliverable: one verified research package + (`research/r439-bsection-survey/`) with two block shortenings (24,305 -> + 24,289 local ADDs), certified class minima for the feasible blocks, and + scoped infeasibility certificates for the rest; no new kappa. +- Overlap check at claim time (2026-10-13): open PRs #873 (block 508), + #843 (block 509), #844 (block 520), #857 (block 523) cover four claimed + blocks with other mechanisms; #728/#792 cover phase-A mini-nodes. No open + PR changes frames 506/507/519/521/522/524. Blocks 508/509/520/523 appear + here only as cross-checks (and frame 523 as a strictly shorter independent + witness than #857's published 40-gate program). +- Overlap refreshed before submission (2026-10-13): PR #880 (frame 507, + fixed-factor class, 35 -> 30) and PR #884 (frame 521, factorization class, + 47 -> 31) landed on two surveyed blocks after the search completed; both + use mechanisms outside the single-write class and are disclosed as + complementary evidence in README.md. Frames 506 and 523 remain uncovered + by any open PR except #857's weaker 523 witness. +- Status: completed in session; submitted as + https://github.com/CrocSwap/integer-mult-bounds/pull/891 (branch + `research/agent-04-bit-seed08`, commit `bdff756c`). See README.md and + VALIDATION.md. diff --git a/research/r439-bsection-survey/EXPECTED.json b/research/r439-bsection-survey/EXPECTED.json new file mode 100644 index 0000000000..fe2b38cb39 --- /dev/null +++ b/research/r439-bsection-survey/EXPECTED.json @@ -0,0 +1,327 @@ +{ + "bill_after": { + "adds": 24289, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 49347, + "payload_bits": 93, + "record_sha256": "ebc8fd69144216f36df9311c7b2af1e1fb163db59ce43bda9887ce99e514550e", + "records": 27218, + "reverse_positive_bound": 1090494 + }, + "bill_before": { + "adds": 24305, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 49347, + "payload_bits": 93, + "record_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a", + "records": 27234, + "reverse_positive_bound": 1113070 + }, + "spliced_frames": [ + 506, + 523 + ], + "survey": { + "506": { + "backward_optimality": { + "backward_distances_sha256": "03a48a831303b72e4cfd0f66e54bd4f71e67242c58cadf28eae7ff5040148c00", + "feasible_edges": 2370, + "minimum": 24, + "state_destination_pairs": 5120, + "states": 1024 + }, + "boolean_inputs_checked": 1024, + "minimum": 24, + "original_gates": 26, + "registers": [ + 5, + 6, + 9, + 46, + 47, + 48, + 52, + 54, + 56, + 58 + ], + "reverse_entrywise_dominated": true, + "reverse_larger_entries": 0, + "reverse_strictly_smaller_entries": 5 + }, + "507": { + "backward_optimality": { + "backward_distances_sha256": "4ed29d0df19476a94b1b8a739be28173c0de62a5588693e023eaa31c842e6e84", + "feasible_edges": 924, + "minimum": null, + "state_destination_pairs": 5120, + "states": 1024 + }, + "original_gates": 35, + "registers": [ + 0, + 3, + 11, + 61, + 62, + 63, + 68, + 69, + 72, + 465 + ], + "supply_witness": { + "col": 4, + "demand": 3, + "recomputed_demand": 3, + "recomputed_supply": 1, + "row": 3, + "supply": 1 + } + }, + "508": { + "backward_optimality": { + "backward_distances_sha256": "939856f3366b7012aeb1e08a2038bb7deef926a85c0155891a186fa036a49b5e", + "feasible_edges": 4376, + "minimum": 30, + "state_destination_pairs": 11264, + "states": 2048 + }, + "minimum": 30, + "original_gates": 37, + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ] + }, + "509": { + "backward_optimality": { + "backward_distances_sha256": "43439ddebf453f959cd2dd23fa13e1c557c658526e8fa1bbbc551c72f19be51c", + "feasible_edges": 5204, + "minimum": null, + "state_destination_pairs": 11264, + "states": 2048 + }, + "original_gates": 31, + "registers": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92, + 468 + ], + "supply_witness": null + }, + "519": { + "backward_optimality": { + "backward_distances_sha256": "63561aebc03a97dbb1bac65067cdbc01fa2d9247639bc0140b63d226a59721d5", + "feasible_edges": 6753, + "minimum": null, + "state_destination_pairs": 24576, + "states": 4096 + }, + "original_gates": 42, + "registers": [ + 15, + 23, + 30, + 41, + 49, + 53, + 59, + 70, + 75, + 82, + 91, + 96 + ], + "supply_witness": { + "col": 8, + "demand": 2, + "recomputed_demand": 2, + "recomputed_supply": 1, + "row": 2, + "supply": 1 + } + }, + "520": { + "backward_optimality": { + "backward_distances_sha256": "ff3c849afd121ab2fb17b45b97ded11c0dcbe867680f64afe17ae3399b140c8d", + "feasible_edges": 5584, + "minimum": null, + "state_destination_pairs": 24576, + "states": 4096 + }, + "original_gates": 41, + "registers": [ + 21, + 26, + 36, + 44, + 51, + 55, + 64, + 71, + 80, + 84, + 94, + 102 + ], + "supply_witness": { + "col": 9, + "demand": 1, + "recomputed_demand": 1, + "recomputed_supply": 0, + "row": 9, + "supply": 0 + } + }, + "521": { + "backward_optimality": { + "backward_distances_sha256": "975892804349a175a49ec4d8140856a333443fea466c8b9faa13c43134b62fc2", + "feasible_edges": 4779, + "minimum": null, + "state_destination_pairs": 24576, + "states": 4096 + }, + "original_gates": 47, + "registers": [ + 10, + 13, + 32, + 34, + 39, + 42, + 76, + 79, + 83, + 85, + 104, + 107 + ], + "supply_witness": null + }, + "522": { + "backward_optimality": { + "backward_distances_sha256": "be039e6860ead96b53176932c6bce4eb6f95fa32e8e518153fe6802a490059ce", + "feasible_edges": 6917, + "minimum": null, + "state_destination_pairs": 24576, + "states": 4096 + }, + "original_gates": 43, + "registers": [ + 1, + 7, + 24, + 25, + 28, + 29, + 98, + 99, + 100, + 101, + 106, + 108 + ], + "supply_witness": { + "col": 3, + "demand": 2, + "recomputed_demand": 2, + "recomputed_supply": 1, + "row": 5, + "supply": 1 + } + }, + "523": { + "backward_optimality": { + "backward_distances_sha256": "7b99c0d267f1f3202f0a9d77454c375b15b5463aedba3cb827101d34ccb56f92", + "feasible_edges": 7500, + "minimum": 39, + "state_destination_pairs": 24576, + "states": 4096 + }, + "boolean_inputs_checked": 4096, + "minimum": 39, + "original_gates": 45, + "registers": [ + 2, + 4, + 14, + 16, + 18, + 20, + 88, + 90, + 93, + 95, + 103, + 109 + ], + "reverse_entrywise_dominated": false, + "reverse_larger_entries": 13, + "reverse_strictly_smaller_entries": 16 + }, + "524": { + "backward_optimality": { + "backward_distances_sha256": "f82428c8c960250093b30e1f8415d805bc2e952dde6aad475fe38b441d257036", + "feasible_edges": 7348, + "minimum": null, + "state_destination_pairs": 24576, + "states": 4096 + }, + "original_gates": 41, + "registers": [ + 8, + 12, + 31, + 37, + 40, + 45, + 73, + 78, + 81, + 86, + 105, + 110 + ], + "supply_witness": { + "col": 9, + "demand": 3, + "recomputed_demand": 3, + "recomputed_supply": 2, + "row": 6, + "supply": 2 + } + } + }, + "survey_frames": [ + 506, + 507, + 508, + 509, + 519, + 520, + 521, + 522, + 523, + 524 + ] +} diff --git a/research/r439-bsection-survey/README.md b/research/r439-bsection-survey/README.md new file mode 100644 index 0000000000..c9f117d991 --- /dev/null +++ b/research/r439-bsection-survey/README.md @@ -0,0 +1,180 @@ +# R439 phase-B whole-block survey: two shortenings and seven class boundaries + +Finite bit-supplier result for the punctured R439 word of PR #555/#589 +(`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`), against base +commit `f567884aeb8851b6e794af1184119a3bfbe1e631` (selected PR799/PR589, +conditional kappa 0.001661634653669567). **No new kappa.** All phase-B blocks +of the word are self-contained integer-linear programs over their own +registers; this note searches each of the ten of them in one class, splices +the two shortenings it finds into one verified word, and certifies why the +class cannot shorten the other seven. + +## Result + +The complete exported local word falls **24,305 -> 24,289 ADDs** (8 forward +gates and their 8 literal reverse-cleanup gates): + +| quantity | before | after | +|---|---:|---:| +| block 506 additions (`B[102:128)`) | 26 | **24** | +| block 523 additions (`B[404:449)`) | 45 | **39** | +| complete exported ADDs | 24,305 | **24,289** | +| exported records | 27,234 | 27,218 | +| forward positive bound | 49,347 | 49,347 (equal) | +| composed reverse positive bound | 1,113,070 | **1,090,494** | +| payload | 93 bits | 93 bits (cap 104) | +| local paid profile / rank mass | `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` / 5,129 | unchanged | +| 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. Forward integer maps of both replaced +blocks are exactly equal; the exact F2 endpoint holds on all 661 dirty-input +columns; the inherited H1-H5 interface conclusions of the pinned +`xcheck_p.py` hold on the spliced word. + +## Survey of all ten phase-B blocks + +Class: the **whole-block single-write class** of open PR #873 (block 508), +with the neighboring framings of PR #844 (fixed two-factor splits) and PR +#857 (integer factorization): each register's final integer row is realized +once, in some realization order, as its entry singleton plus a subset of +donors, where each donor is either the completed final row of a register +realized earlier or the entry singleton of a register realized later, and +each donor is used at most once per row. A row with `k` donors costs `k` +additions. Programs that consume a register mid-construction (multi-write +interleavings) are **outside** the class and are not searched. + +| frame | slice | gates | class minimum | status | +|---|---|---:|---:|---| +| 506 | `B[102:128)` | 26 | **24** | construction, spliced | +| 507 | `B[128:163)` | 35 | none | infeasible; donor-supply witness (row 3, col 4: demand 3 > supply 1) | +| 508 | `B[205:242)` | 37 | 30 | cross-check: reproduces PR #873's certified minimum exactly | +| 509 | `B[283:314)` | 31 | none | infeasible in class (global; no per-row witness) | +| 519 | `B[163:205)` | 42 | none | infeasible; donor-supply witness (row 2, col 8: 2 > 1) | +| 520 | `B[242:283)` | 41 | none | infeasible; donor-supply witness (row 9, col 9: 1 > 0) | +| 521 | `B[314:361)` | 47 | none | infeasible in class (global; no per-row witness) | +| 522 | `B[361:404)` | 43 | none | infeasible; donor-supply witness (row 5, col 3: 2 > 1) | +| 523 | `B[404:449)` | 45 | **39** | construction, spliced; beats open PR #857's 40-gate witness | +| 524 | `B[449:490)` | 41 | none | infeasible; donor-supply witness (row 6, col 9: 3 > 2) | + +Row/column indices of the witnesses are local to the block's sorted register +list; the witness rows carry the wire numbers too. A donor of a row must fit +the row's goal entrywise (all values nonnegative), so summing **every** fitting +donor, including mutually exclusive singleton/row pairs, over-approximates +the achievable column supply. A demand above that sum rules out the row for +every realization order at once: an order-independent certificate that needs +no trust in the dynamic program. Blocks 509 and 521 have no such row; their +infeasibility is a joint order obstruction certified only by the two +exhaustive dynamic programs (`search.py` forward, `verify.py` backward, whose +distances are pinned in `EXPECTED.json`). + +The infeasibility results are scoped statements about this class. They are +not impossibility theorems for the blocks: blocks 509 and 520 have published +shorter programs in other classes (PRs #843 and #844), which use exactly the +mechanisms (shared partial sums, fixed-factor decompositions) this class +excludes. The survey therefore also explains why those claimed-block methods +do not transfer to the unclaimed blocks. + +Two concurrent PRs landed on unclaimed blocks after this survey's search +completed, both in factor-split classes: open PR #880 (frame 507, 35 -> 30 +via two fixed positive factors) and open PR #884 (frame 521, 47 -> 31 via a +bounded factorization search). The certificates here show their objects are +exactly two of the blocks with no whole-block single-write program: a +shorter program for frames 507 and 521 must use factor-level intermediate +donors or multi-write interleavings, which is what those constructions do. +This is independent structural evidence for their mechanisms; their +implementations and savings are not imported and are not part of the spliced +word. + +## Method + +`search.py` (discovery) runs a dynamic program over realized-register +subsets; each transition realizes one row with a minimum donor subset found by +meet-in-the-middle subset sums. It writes `CANDIDATES.json` (full search +record) and `CERTIFICATE.json` (bindings, candidate gates, source pins). +Deterministic, no randomness, standard library only. + +`verify.py` (independent) imports no search code. It re-derives every class +minimum or infeasibility with a backward Bellman recursion and its own +iterative-deepening donor enumeration, rechecks the donor-supply certificates +by direct counting, and for the spliced word recomputes forward/reverse +integer maps, all 1,024/4,096 block Boolean truth tables, the literal cleanup +reversal, register frame paths, the exact F2 endpoint on all 661 columns, the +H1-H5 interface via the pinned `xcheck_p.py`, and the exported bills and +positive/payload bounds via the pinned `export_records.py`. Twelve mutation +controls must be rejected. Three real defects during development (a reversed +subtraction in the backward donor recursion, a left-to-right splice that +shifted block 523's indices, and a no-op mutation control) were each caught +by one of these checks; see `VALIDATION.md`. + +## Block 523: relation to open PR #857 + +PR #857 (seed 18) replaces the same block with a 40-gate program found by a +bounded randomized integer-factorization search, reporting "no shorter +reverse-dominated candidate" in their search and allowing reverse growth to +1,228,514 with a 94-bit payload. The 39-gate witness here is a different +mechanism: a certified minimum of the single-write class, with the minimum +re-derived by an independent recursion. Its local reverse map is not +entrywise dominated (16 entries strictly shrink, a few grow), but the +composed exported reverse bound of the whole word **drops** to 1,090,494 and +the payload stays at 93 bits. Their implementation and savings are not +imported; both results should be credited to their authors. + +## Reproduce + +Standard-library Python 3.11+ from the repository root: + +```sh +python3 -I -B research/r439-bsection-survey/search.py +python3 -I -B research/r439-bsection-survey/verify.py +``` + +Expected (verify, ~90 s): + +```text +"status": "PASS_R439_BSECTION_SURVEY" +"columns": 661 +"survey_frames": [506, 507, 508, 509, 519, 520, 521, 522, 523, 524] +"spliced_frames": [506, 523] +bill_before.adds = 24305, bill_after.adds = 24289 +bill_before.forward_positive_bound = bill_after.forward_positive_bound = 49347 +bill_after.reverse_positive_bound = 1090494 +bill_after.payload_bits = 93 +12 negative controls rejected +``` + +`search.py` regenerates `CANDIDATES.json` and `CERTIFICATE.json` byte for +byte (checked across runs). `verify.py` needs no third-party packages; the +exporter and interface checker are used unmodified from their pinned +locations. + +## Scope and obligations + +Only `research/r439-bsection-survey/` is added. `upstream/`, the selected +certificate and every consumed supplier source are unchanged. This is a +conditional finite construction and a scoped class-infeasibility survey, not +a Lean proof and not a new kappa: the bit side does not bind the selected +witness (kappa is complex-bound at 0.001661634653669567), so the result is +bit headroom and certified search coverage only. The minima are certified +only inside the single-write class; multi-write interleavings and shared +partial sums are not excluded, and "no class program exists" is not an +impossibility theorem. 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, Dylan Crow (record exporter), Zhihao Chen and the retained +supplier lineage. The whole-block single-write class and the +independent-recursion verification pattern follow open PR #873 (block 508) +with attribution; the fixed-factor framing is PR #844's and the factorization +search is PR #857's (both objects and savings not imported). The four +claimed blocks' cross-checks (508/509/520/523) are recorded so the survey is +complete. Prepared with help from opencode. Apache-2.0. No independent human +review is claimed. diff --git a/research/r439-bsection-survey/SOURCES.json b/research/r439-bsection-survey/SOURCES.json new file mode 100644 index 0000000000..0f9d89f3ed --- /dev/null +++ b/research/r439-bsection-survey/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema": "r439-bsection-survey/sources/1", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "base_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "selected_result": { + "record": "certificates/selected-result.json", + "pr799_with_pr589": true, + "conditional_kappa": "1661634653669567/1000000000000000000", + "changed_by_this_work": false + }, + "consumed_sources": { + "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": { + "PR543/PR555 (eumemic)": "punctured R439 word, generator, checkers, pricing pipelines, package structure", + "PR510/PR545/PR589 (DreamingOfClouds and lineage)": "nine-stage chain, punctured unit, bit headroom; supplier head a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "export_records.py (Dylan Crow)": "record exporter used unmodified", + "PR873 (open, seed 05)": "whole-block single-write class on block 508 and the independent-recursion verification pattern; its certified minimum 30 is reproduced as a cross-check; its implementation is not imported", + "PR857 (open, seed 18)": "object of the block-523 cross-check: 40-gate factorization witness; its implementation and savings are not imported", + "PR844 (open)": "fixed two-factor framing of block 520; implementation not imported", + "PR843 (open, seed 07)": "block-509 partial-sum reuse; implementation not imported", + "PR728/PR792 (open)": "phase-A mini-node mechanisms (different section; no conflict)" + }, + "overlap_refresh": "open PR titles and bodies re-read 2026-10-13 before submission, including arrivals after the initial claim: PR880 (frame 507, fixed-factor class), PR884 (frame 521, factorization class) and PR886 (frame assignment) postdate the survey search and are disclosed in README.md; no open PR changes blocks 506 or 523 other than PR857's 40-gate witness at 523", + "environment": { + "os": "Windows 11 x64", + "python": "3.12.14 (python3.12.exe, -I -B)", + "third_party_packages": "none required by search.py or verify.py" + } +} diff --git a/research/r439-bsection-survey/VALIDATION.md b/research/r439-bsection-survey/VALIDATION.md new file mode 100644 index 0000000000..2bcfbf578f --- /dev/null +++ b/research/r439-bsection-survey/VALIDATION.md @@ -0,0 +1,85 @@ +# Validation record + +Environment: Windows 11 x64, Python 3.12.14 (`python3.12.exe`), no +third-party packages. All commands from the repository root at base commit +`f567884aeb8851b6e794af1184119a3bfbe1e631`, run with `-I -B`. + +## Commands and outcomes + +1. `python3 -I -B research/r439-bsection-survey/search.py` + Prints the ten per-block results (frames 506..524, minima 24/30/39, + five donor-supply witnesses, two global infeasibilities) and + `spliced frames: [506, 523] forward gates saved: 8 -> full word ADDs + 24289`. Regenerates `CANDIDATES.json` and `CERTIFICATE.json`; both files + were byte-identical (SHA-256) across repeated runs. + +2. `python3 -I -B research/r439-bsection-survey/verify.py` + Exit 0, wall time 87.5 s, prints `"status": "PASS_R439_BSECTION_SURVEY"` + with columns 661, survey all ten frames, spliced `[506, 523]`, bills + `adds 24305 -> 24289`, forward positive bound 49,347 (equal), composed + reverse positive bound `1,113,070 -> 1,090,494`, payload 93 bits, + rank mass 5,129, identical frame paths for all 661 registers, H1-H5 + hypotheses and conclusions all true, and 12 rejected negative controls. + +3. Receipt red test: `EXPECTED.json` tampered (block 523 minimum set to 40); + the same command failed with `Reject: survey receipts differ` in 85.7 s, + exit 1. Receipts restored from backup; the green run above followed. + +## Checks recomputed by `verify.py` + +- Source pins (base commit and three consumed files) and certificate schema. +- Per block: binding (frame, slice, registers, original bill), forward + integer map by independent column propagation. +- Class minima and infeasibilities by a backward Bellman recursion over + realized-register subsets with its own iterative-deepening donor + enumeration (written independently of `search.py`; the two agreed on all + ten blocks). +- Donor-supply infeasibility certificates by direct recounting of fitting + donors and their column totals. +- Spliced blocks: forward map equality, reverse maps (entrywise comparison + recorded per block), exhaustive Boolean truth tables (1,024 inputs at frame + 506, 4,096 at frame 523). +- Whole word: splice lengths, unrelated fields unchanged, literal cleanup + reversal (H4), register frame paths (nesting-legal and identical to the + original on all 661 registers), exact F2 endpoint on all 661 dirty-input + columns before and after. +- Pinned `xcheck_p.py` interface check: H1-H5 hypotheses and all four + conclusions hold on the spliced word. +- Paid profile `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` and rank + mass 5,129 recomputed from frame paths and retained copy ranks. +- Pinned `export_records.py` bills on both words: ADD/copys/erasure counts, + non-ADD event inventory, forward and reverse positive bounds by exact + record replay, payload bits against the unchanged 104-bit cap. + +## Negative controls (all rejected) + +`mutated_candidate_source_506`, `unpaid_gate_506`, +`mutated_candidate_source_523`, `unpaid_gate_523`, +`inverted_domination_506`, `forged_domination_523`, `omitted_cleanup`, +`missing_gate_with_matching_cleanup`, `illegal_frame_descent`, +`stale_cleanup_literal_H4` (positive semantic control, rejected only by the +literal H4 guard), `wrong_slice_binding`, `forged_supply_witness`. + +## Defects found by these checks during development + +1. The backward donor recursion subtracted value-minus-goal instead of + goal-minus-value, silently reporting infeasible for multi-donor rows. + Caught by the cross-implementation disagreement with the forward DP + (block 506), then fixed; both implementations now agree on all ten blocks. +2. The word builder spliced replacements left to right, so the 26 -> 24 + change at `B[102:128)` shifted block 523's indices by two and spliced the + wrong gates. Caught by the whole-word F2 endpoint check at register 112. +3. The first mutation control changed a gate's source to its existing source + (a no-op) and was correctly reported as "negative control accepted". + Fixed to mutate to a distinct wire. + +Each defect was observed as a failure before the fix; the final green run +above is after all three. + +## Not run + +C++ native legality and 5/9/11-stage replays, hosted invoice, global +assembly, selected cold replay (`make frontier799-verify`), `make verify`, +Lean builds and remote CI. Forward-map equality plus the recomputed exported +bills carry the cost claims; an independent native replay remains to confirm +them, as in the neighboring block PRs. diff --git a/research/r439-bsection-survey/search.py b/research/r439-bsection-survey/search.py new file mode 100644 index 0000000000..d38fd63239 --- /dev/null +++ b/research/r439-bsection-survey/search.py @@ -0,0 +1,304 @@ +#!/usr/bin/env python3 +"""Discovery search for whole-block programs on the ten phase-B blocks of +PR589's tuned punctured R439 word, covering the six unclaimed blocks and four +cross-checks against the blocks changed by open PRs. + +Class (the whole-block single-write class of open PR #873, Gautam Gupta's +fixed-factor framing in #844 and #857's factorization search): each register's +final integer row is realized once, in some realization order, as its entry +singleton plus a subset of donors, where each donor is either the completed +final row of a register realized earlier or the entry singleton of a register +realized later, and each donor is used at most once per row. The number of +additions of a row is its donor count. The search is a dynamic program over +realized-register subsets with meet-in-the-middle subset sums. For blocks no +program in the class realizes, a per-row donor-supply obstruction is reported +when one exists. + +No optimality outside this class is claimed: programs that consume a register +mid-construction (multi-write interleavings) are not searched here. + +Writes CANDIDATES.json and CERTIFICATE.json. Deterministic; no randomness; +standard library only. Prepared with help from opencode. Apache-2.0. +""" +import gzip +import hashlib +import itertools +import json +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). Frames 506/507/519/521/522/524 are unclaimed; frames 508, 509, +# 520 and 523 are cross-checks against the objects of open PRs #873, #843, +# #844 and #857. Only 506 and 523 are spliced into the verified word. +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), +] +SPLICED = {506, 523} + + +def canon(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canon(value)).hexdigest() + + +def block_model(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[s[0]]) for _, t, s in blk] + forward = [[int(i == j) for j in range(n)] for i in range(n)] + for t, s in ops: + for j in range(n): + forward[t][j] += forward[s][j] + return regs, ops, forward + + +def subset_min(donors, goal): + """Minimum donor count whose values sum to goal exactly (each donor at + most once); None when unreachable. Meet in the middle.""" + k = len(donors) + half = k // 2 + first, second = donors[:half], donors[half:] + + def sums(part): + zero = tuple(0 for _ in goal) + table = {zero: 0} + for value in part: + for total, count in list(table.items()): + merged = tuple(a + b for a, b in zip(total, value)) + if all(a <= b for a, b in zip(merged, goal)): + if merged not in table or count + 1 < table[merged]: + table[merged] = count + 1 + return table + + left, right = sums(first), sums(second) + best = None + for total, count in left.items(): + rest = tuple(b - a for a, b in zip(total, goal)) + if rest in right: + cost = count + right[rest] + if best is None or cost < best: + best = cost + return best + + +def search(forward): + """Minimum donor-addition count and an attaining realization; also the + dynamic-program statistics for the record.""" + n = len(forward) + goal = [] + for i in range(n): + row = list(forward[i]) + row[i] -= 1 + if min(row) < 0: + return None + goal.append(tuple(row)) + infinity = 10 ** 9 + size = 1 << n + dist = [infinity] * size + parent = [None] * size + dist[0] = 0 + edges = 0 + for mask in range(size): + if dist[mask] >= infinity: + continue + for dst in range(n): + if mask >> dst & 1: + continue + donors = [] + for src in range(n): + if src == dst: + continue + value = tuple(forward[src]) if mask >> src & 1 else tuple(int(j == src) for j in range(n)) + if all(a <= b for a, b in zip(value, goal[dst])): + donors.append((src, value)) + best = subset_min([v for _, v in donors], goal[dst]) + if best is None: + continue + edges += 1 + nxt = mask | (1 << dst) + if dist[mask] + best < dist[nxt]: + dist[nxt] = dist[mask] + best + parent[nxt] = (mask, dst) + if dist[size - 1] >= infinity: + return None + # Reconstruct the realization order and the donor subset of each row. + chain = [] + mask = size - 1 + while mask: + prev, dst = parent[mask] + chain.append(dst) + mask = prev + chain.reverse() + donors_of = {} + for step, dst in enumerate(chain): + mask = sum(1 << r for r in chain[:step]) + goal_row = goal[dst] + candidates = [] + for src in range(n): + if src == dst: + continue + value = tuple(forward[src]) if mask >> src & 1 else tuple(int(j == src) for j in range(n)) + if all(a <= b for a, b in zip(value, goal_row)): + candidates.append((src, value)) + chosen = recover(candidates, goal_row) + donors_of[dst] = chosen + gates = [(dst, src) for dst in chain for src in donors_of[dst]] + return { + "minimum": dist[size - 1], + "realization_order": chain, + "donors": {str(k): v for k, v in donors_of.items()}, + "gates": gates, + "states": size, + "state_destination_pairs": n * (1 << (n - 1)), + "feasible_edges": edges, + "distances_sha256": digest(dist), + } + + +def recover(candidates, goal): + """One minimum donor subset summing to goal (same recursion as + subset_min, with the chosen subset returned).""" + k = len(candidates) + half = k // 2 + first, second = candidates[:half], candidates[half:] + + def sums(part): + zero = tuple(0 for _ in goal) + table = {zero: (0, [])} + for idx, (src, value) in enumerate(part): + for total, (count, chosen) in list(table.items()): + merged = tuple(a + b for a, b in zip(total, value)) + if all(a <= b for a, b in zip(merged, goal)): + if merged not in table or count + 1 < table[merged][0]: + table[merged] = (count + 1, chosen + [src]) + return table + + left, right = sums(first), sums(second) + best = None + for total, (count, chosen) in left.items(): + rest = tuple(b - a for a, b in zip(total, goal)) + if rest in right: + cost = count + right[rest][0] + if best is None or cost < best[0]: + best = (cost, chosen + right[rest][1]) + assert best is not None + return sorted(best[1]) + + +def supply_witness(forward): + """First per-row donor-supply obstruction, or None. + + A donor of row i is an entry singleton or a completed final row and must + fit the row's goal entrywise. Summing every fitting donor (including + mutually exclusive singleton/row pairs) over-approximates the achievable + column supply, so a column whose demand exceeds it certifies that no + program in the class realizes the row, independent of realization order. + """ + n = len(forward) + for i in range(n): + goal = [forward[i][j] - (1 if j == i else 0) for j in range(n)] + supply = [0] * n + for k in range(n): + if k == i: + continue + for value in ([1 if j == k else 0 for j in range(n)], list(forward[k])): + if all(a <= b for a, b in zip(value, goal)): + for j in range(n): + supply[j] += value[j] + for j in range(n): + if goal[j] > supply[j]: + return {"row": i, "col": j, "demand": goal[j], "supply": supply[j]} + return None + + +def main(): + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + out = {"source": WORD, + "source_content_sha256": digest(json.loads(gzip.decompress((ROOT / WORD).read_bytes()))), + "blocks": []} + certificate = { + "schema": "r439-bsection-survey/1", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_sha256": { + WORD: hashlib.sha256((ROOT / WORD).read_bytes()).hexdigest(), + "research/e8-bit-p111-tuned/code/xcheck_p.py": + hashlib.sha256((ROOT / "research/e8-bit-p111-tuned/code/xcheck_p.py").read_bytes()).hexdigest(), + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": + hashlib.sha256((ROOT / "research/e8-bit-carrier-skeleton/code/bit/export_records.py").read_bytes()).hexdigest(), + }, + "blocks": [], + } + for frame, first, last in BLOCKS: + blk = word["B"][first:last + 1] + assert all(f == frame and len(ss) == 1 for f, t, ss in blk), (frame, first, last) + regs, ops, forward = block_model(blk) + found = search(forward) + witness = supply_witness(forward) if found is None else None + entry = { + "frame": frame, + "slice": [first, last + 1], + "registers": regs, + "original_gates": len(ops), + "forward_sha256": digest(forward), + "diagonal": [forward[i][i] for i in range(len(regs))], + } + cert = {"section": "B", "frame": frame, "slice": [first, last + 1], + "registers": regs, "original_gates": len(ops), "spliced": False} + if found is None: + entry["class_covered"] = False + entry["supply_witness"] = witness + cert["status"] = "infeasible" + cert["witness"] = witness + else: + touched = sorted({regs[t] for t, _ in found["gates"]} | {regs[s] for _, s in found["gates"]}) + entry.update({ + "class_covered": True, + "minimum": found["minimum"], + "saving": len(ops) - found["minimum"], + "candidate_gates": [[frame, regs[t], [regs[s]]] for t, s in found["gates"]], + "local_gates": found["gates"], + "realization_order": [regs[i] for i in found["realization_order"]], + "donors": {str(regs[int(k)]): [regs[i] for i in v] for k, v in found["donors"].items()}, + "touched_registers": touched, + "all_registers_touched": touched == regs, + "states": found["states"], + "state_destination_pairs": found["state_destination_pairs"], + "feasible_edges": found["feasible_edges"], + "distances_sha256": found["distances_sha256"], + }) + cert["status"] = "class-minimum" + cert["minimum"] = found["minimum"] + if frame in SPLICED: + assert touched == regs, ("spliced block breaks frame paths", frame) + cert["spliced"] = True + cert["gates"] = entry["candidate_gates"] + out["blocks"].append(entry) + certificate["blocks"].append(cert) + print(frame, entry.get("original_gates"), "->", entry.get("minimum"), + "witness:", witness) + (HERE / "CANDIDATES.json").write_text(json.dumps(out, indent=1) + "\n", encoding="utf-8") + (HERE / "CERTIFICATE.json").write_text(json.dumps(certificate, indent=1) + "\n", encoding="utf-8") + total = sum(b["original_gates"] - b["minimum"] for b in certificate["blocks"] if b["spliced"]) + print("spliced frames:", sorted(SPLICED), "forward gates saved:", total, + "-> full word ADDs", 24305 - 2 * total, "(forward + literal reverse cleanup)") + + +if __name__ == "__main__": + main() diff --git a/research/r439-bsection-survey/verify.py b/research/r439-bsection-survey/verify.py new file mode 100644 index 0000000000..eb79ba3da1 --- /dev/null +++ b/research/r439-bsection-survey/verify.py @@ -0,0 +1,535 @@ +#!/usr/bin/env python3 +"""Exact finite verification for the R439 phase-B whole-block survey. + +Independent of search.py: the class minima are rechecked here with a backward +Bellman recursion over realized-register subsets (the opposite recursion +direction to the discovery DP) and its own donor-subset enumeration; the +per-row donor-supply infeasibility certificates are rechecked by direct +counting; the spliced blocks' forward integer maps, reverse positive maps, +Boolean truth tables, splice, register frame paths, paid profile, exact F2 +endpoint on all columns, inherited H1-H5 interface, exported scalar bills and +positive/payload bounds are all recomputed. + +The owning geometry/interface checker is eumemic's PR555/PR589 xcheck_p.py and +the record exporter is Dylan Crow's export_records.py; both are pinned by +SHA-256 in CERTIFICATE.json and used unmodified. + +The whole-block single-write class is that of open PR #873 (with PR #844's and +PR #857's neighboring framings); the verification structure adapts #873's +r439-block508-schedule verifier with attribution. No optimality outside the +class is claimed. + +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" + + +class Reject(Exception): + pass + + +def need(ok, message): + if not ok: + raise Reject(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def pins(certificate): + need(certificate["schema"] == "r439-bsection-survey/1", "unknown schema") + need(certificate["base_commit"] == "f567884aeb8851b6e794af1184119a3bfbe1e631", + "certificate built against a different base") + for path, expected in certificate["source_sha256"].items(): + actual = hashlib.sha256((ROOT / path).read_bytes()).hexdigest() + need(actual == expected, "source pin mismatch: " + path) + + +def integer_map(ops, n): + """Propagate each integer basis column independently (fresh implementation).""" + columns = [] + for column in range(n): + values = [1 if i == column else 0 for i in range(n)] + for dst, src in ops: + need(type(dst) is int and type(src) is int and 0 <= dst < n and 0 <= src < n + and dst != src, "invalid block operation") + values[dst] += values[src] + columns.append(values) + return [list(row) for row in zip(*columns)] + + +def dominated(new, old): + return all(x <= y for a, b in zip(new, old) for x, y in zip(a, b)) + + +def supply_certificate(forward, row, col): + """Independent recheck of a per-row donor-supply obstruction. + + In the whole-block single-write class, the donors of a row are entry + singletons or completed final rows, each at most once, and every donor + must fit the row's goal entrywise (all values are nonnegative). Returns + the pair (demand, supply) where supply over-approximates every feasible + donor combination by summing all fitting donors, including mutually + exclusive singleton/row pairs. demand > supply is an order-independent + infeasibility certificate for that row. + """ + n = len(forward) + goal = [forward[row][j] - (1 if j == row else 0) for j in range(n)] + need(min(goal) >= 0, "row has no e_i base") + supply = [0] * n + for k in range(n): + if k == row: + continue + for value in ([1 if j == k else 0 for j in range(n)], list(forward[k])): + if all(a <= b for a, b in zip(value, goal)): + for j in range(n): + supply[j] += value[j] + return goal[col], supply[col] + + +def row_cost(forward, goal_row, done, dst): + """Minimum donor count realizing row dst from realized set `done`, or + None. Iterative deepening over donor subsets with exact integer sums and + entrywise pruning; donors are completed rows of `done` and entry + singletons of the registers not yet realized (each donor at most once).""" + n = len(forward) + donors = [] + for src in range(n): + if src == dst: + continue + value = list(forward[src]) if done >> src & 1 else [1 if j == src else 0 for j in range(n)] + if all(a <= b for a, b in zip(value, goal_row)): + donors.append(value) + donors.sort(key=lambda value: -sum(value)) + + def extend(start, remaining, depth): + if not any(remaining): + return True + if depth == 0: + return False + for index in range(start, len(donors)): + value = donors[index] + if all(a <= b for a, b in zip(value, remaining)): + rest = [a - b for a, b in zip(remaining, value)] + if extend(index + 1, rest, depth - 1): + return True + return False + + if not any(goal_row): + return 0 + for depth in range(1, len(donors) + 1): + if extend(0, goal_row, depth): + return depth + return None + + +def backward_minimum(forward): + """Backward Bellman recursion over realized-register subsets; written + independently of search.py's forward dynamic program. Returns None when + no program in the class realizes the map.""" + n = len(forward) + need(all(forward[i][i] >= 1 for i in range(n)), "missing diagonal") + goal = [[forward[i][j] - (1 if j == i else 0) for j in range(n)] for i in range(n)] + size = 1 << n + infinity = 10 ** 9 + dist = [infinity] * size + dist[size - 1] = 0 + feasible = 0 + for done in range(size - 2, -1, -1): + for dst in range(n): + if done >> dst & 1: + continue + cost = row_cost(forward, goal[dst], done, dst) + if cost is None: + continue + feasible += 1 + nxt = done | (1 << dst) + if cost + dist[nxt] < dist[done]: + dist[done] = cost + dist[nxt] + return {"minimum": None if dist[0] >= infinity else dist[0], + "states": size, + "state_destination_pairs": n * (1 << (n - 1)), + "feasible_edges": feasible, + "backward_distances_sha256": digest(dist)} + + +def block_model(blk, regs): + index = {r: i for i, r in enumerate(regs)} + n = len(regs) + need(all(len(ss) == 1 and t in index and ss[0] in index and ss[0] != t for _, t, ss in blk), + "block leaves the single-wire block class") + return [(index[t], index[s]) for _, t, (s,) in blk], n + + +def bind_block(word, entry): + need(entry["section"] == "B", "wrong section") + first, last = entry["slice"] + blk = word["B"][first:last] + need(len(blk) == entry["original_gates"], "wrong original bill") + need(all(f == entry["frame"] and len(ss) == 1 for f, t, ss in blk), "source block changed") + regs = sorted({t for _, t, _ in blk} | {s for _, _, ss in blk for s in ss}) + need(regs == entry["registers"], "block touches undeclared wires") + ops, n = block_model(blk, regs) + forward = integer_map(ops, n) + return blk, ops, forward, n + + +def rebuild_cleanup(word): + full = next(i for i, frame in enumerate(word["frames"]) if len(frame) == word["v"]) + return [[full, d, list(ss)] for _, d, ss in reversed(word["A"] + word["B"]) + if d < word["v"] or d >= 2 * word["v"]] + + +def build_word(word, certificate): + result = copy.deepcopy(word) + # Right to left: a shorter replacement shifts later B indices. + for entry in sorted((e for e in certificate["blocks"] if e["spliced"]), + key=lambda e: -e["slice"][0]): + first, last = entry["slice"] + need(len(entry["gates"]) == entry["minimum"], "gate count differs from certified minimum") + result["B"][first:last] = copy.deepcopy(entry["gates"]) + result["C"] = rebuild_cleanup(result) + return result + + +def frame_paths(word): + frames = [set(f) for f in word["frames"]] + paths = [[f] for f in word["start"]] + + def move(r, f): + if paths[r][-1] != f: + need(frames[paths[r][-1]] < frames[f], "illegal frame descent or lateral move") + paths[r].append(f) + for section in "DABC": + for f, d, ss in word[section]: + for r in [d, *ss]: + move(r, f) + for r, f in enumerate(word["final"]): + move(r, f) + return paths + + +def whole_endpoint(word): + n, v = 2 * word["v"] + word["R"], word["v"] + state = [{i} for i in range(n)] + + def run(section): + for _, d, sources in word[section]: + for s in sources: + state[d].symmetric_difference_update(state[s]) + run("D") + run("A") + snapshots = [state[r].copy() for r in word["ret"]] + for t, reads in enumerate(word["scatter"]): + for k in reads: + state[v + t].symmetric_difference_update(snapshots[k]) + run("B") + run("C") + for r, actual in enumerate(state): + expected = {r, r - v} if v <= r < 2 * v else {r} + need(actual == expected, "dirty-input endpoint mismatch at register %d" % r) + return n + + +def boolean_tables(ops_old, ops_new, n): + hits = 0 + for value in range(1 << n): + state_old = [(value >> i) & 1 for i in range(n)] + state_new = list(state_old) + for ops, state in ((ops_old, state_old), (ops_new, state_new)): + for dst, src in ops: + state[dst] ^= state[src] + need(state_old == state_new, "Boolean input counterexample: %d" % value) + hits += 1 + return hits + + +def load_checker(): + spec = importlib.util.spec_from_file_location("bsection_survey_xcheck", ROOT / CHECKER) + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + return checker + + +def export_and_bound(word, out): + out.mkdir(parents=True, exist_ok=True) + path = out / "word.json.gz" + path.write_bytes(gzip.compress(canonical(word), mtime=0)) + subprocess.run([sys.executable, "-I", "-B", str(ROOT / EXPORTER), + str(path), str(out / "records")], + check=True, capture_output=True, text=True) + raw = (out / "records/249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "misaligned exporter records") + records = list(struct.iter_unpack("<6i", raw)) + n = 2 * word["v"] + word["R"] + bounds = [] + for reverse in (False, True): + norms, maximum, opened = [1] * (n + 1), 1, False + for op, a, b, coefficient, _, _ in (reversed(records) if reverse else records): + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + norms[a] += abs(coefficient) * norms[b] + maximum = max(maximum, norms[a]) + elif op == 2: + need(not opened, "nested retained copy") + norms[b], opened = norms[a], True + elif op == 3: + need(opened, "unmatched retained erase") + norms[b], opened = 0, False + else: + raise Reject("unknown record opcode") + need(not opened, "unclosed retained copy") + bounds.append(maximum) + payload = 64 * bounds[0] ** 3 * bounds[1] ** 2 + need(payload < 1 << 104, "positive-prefix cap exceeded") + return {"records": len(records), "adds": sum(r[0] == 1 for r in records), + "copies": sum(r[0] == 2 for r in records), + "erasures": sum(r[0] == 3 for r in records), + "forward_positive_bound": bounds[0], "reverse_positive_bound": bounds[1], + "payload_bits": payload.bit_length(), + "record_sha256": hashlib.sha256(raw).hexdigest()}, records + + +def must_reject(name, action): + try: + action() + except Reject: + return name + raise Reject("negative control accepted: " + name) + + +def verify(out): + certificate = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + pins(certificate) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) \ + if (HERE / "EXPECTED.json").exists() else None + if expected is None and not globals().get("EXPECTED_MISSING_OK"): + raise Reject("EXPECTED.json receipts missing") + + survey = {} + spliced = {} + for entry in certificate["blocks"]: + blk, ops, forward, n = bind_block(word, entry) + record = {"original_gates": entry["original_gates"], "registers": entry["registers"]} + if entry["status"] == "infeasible": + optimality = backward_minimum(forward) + need(optimality["minimum"] is None, "class program exists for a block certified infeasible") + record["backward_optimality"] = optimality + witness = entry.get("witness") + if witness is not None: + demand, supply = supply_certificate(forward, witness["row"], witness["col"]) + need((demand, supply) == (witness["demand"], witness["supply"]) + and demand > supply, + "donor-supply certificate does not hold") + record["supply_witness"] = dict(witness, recomputed_demand=demand, + recomputed_supply=supply) + else: + record["supply_witness"] = None + survey[entry["frame"]] = record + continue + need(entry["status"] == "class-minimum", "unknown status: " + entry["status"]) + optimality = backward_minimum(forward) + need(optimality["minimum"] == entry["minimum"], "class minimum receipt differs") + record["backward_optimality"] = optimality + record["minimum"] = entry["minimum"] + if entry["spliced"]: + need(entry["frame"] == entry["gates"][0][0] and + all(f == entry["frame"] and len(ss) == 1 and t in entry["registers"] + and ss[0] in entry["registers"] and ss[0] != t for f, t, ss in entry["gates"]), + "candidate leaves the single-wire block class") + local, m = block_model(entry["gates"], entry["registers"]) + need(m == n, "candidate register count differs") + forward_new = integer_map(local, n) + need(forward_new == forward, "forward integer map differs") + reverse_old = integer_map(ops[::-1], n) + reverse_new = integer_map(local[::-1], n) + record["reverse_entrywise_dominated"] = dominated(reverse_new, reverse_old) + record["reverse_strictly_smaller_entries"] = sum( + 1 for a, b in zip(reverse_new, reverse_old) for x, y in zip(a, b) if x < y) + record["reverse_larger_entries"] = sum( + 1 for a, b in zip(reverse_new, reverse_old) for x, y in zip(a, b) if x > y) + record["boolean_inputs_checked"] = boolean_tables(ops, local, n) + spliced[entry["frame"]] = record + survey[entry["frame"]] = record + + frames = sorted(survey) + receipts = {str(f): survey[f] for f in frames} + if expected is not None: + need(frames == expected["survey_frames"], "survey frame set differs") + need(receipts == expected["survey"], "survey receipts differ") + + candidate = build_word(word, certificate) + need(len(candidate["B"]) == len(word["B"]) - sum( + e["original_gates"] - e["minimum"] for e in certificate["blocks"] if e["spliced"]), + "B length differs from the spliced gate counts") + need(all(candidate[k] == word[k] for k in word if k not in ("B", "C")), "unrelated field changed") + need(candidate["C"] == rebuild_cleanup(candidate), "literal cleanup reversal fails") + before_paths, after_paths = frame_paths(word), frame_paths(candidate) + need(before_paths == after_paths, "register frame path changed") + whole_endpoint(word) + columns = whole_endpoint(candidate) + checker = load_checker() + dimensions, labels, flow, hypotheses, conclusion, _ = checker.check(candidate) + need(all(hypotheses.values()) and all(conclusion.values()), "inherited interface guard fails") + profile = Counter(dimensions.fdim[b] - dimensions.fdim[a] + for path in after_paths for a, b in itertools.pairwise(path)) + profile.update(t["rank"] for t in flow["totals"]) + need(dict(sorted(profile.items())) == {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, + "paid profile changed") + need(sum(k * v for k, v in profile.items()) == 5129, "rank mass changed") + + tmp = Path(out) if out else Path(tempfile.mkdtemp(prefix="bsection-survey-")) + before_bill, before_records = export_and_bound(word, tmp / "before") + after_bill, after_records = export_and_bound(candidate, tmp / "after") + if expected is not None: + need(before_bill == expected["bill_before"], "before bill differs from receipt") + need(after_bill == expected["bill_after"], "after bill differs from receipt") + saved = sum(entry["original_gates"] - entry["minimum"] + for entry in certificate["blocks"] if entry["spliced"]) + need(before_bill["adds"] - after_bill["adds"] == 2 * saved == 16, + "ADD saving does not match the spliced gate counts") + need(before_bill["copies"] == after_bill["copies"] == 9, "retained copy count changed") + need(before_bill["erasures"] == after_bill["erasures"] == 9, "retained erasure count changed") + need(after_bill["forward_positive_bound"] == before_bill["forward_positive_bound"] == 49347, + "forward positive bound changed") + need(after_bill["reverse_positive_bound"] < before_bill["reverse_positive_bound"] == 1113070, + "composed reverse positive bound not reduced") + need(after_bill["payload_bits"] == before_bill["payload_bits"] == 93, "payload bits changed") + need(Counter(r for r in before_records if r[0] != 1) + == Counter(r for r in after_records if r[0] != 1), "non-ADD event inventory changed") + + controls = [] + for entry in certificate["blocks"]: + if not entry["spliced"]: + continue + bad = copy.deepcopy(entry["gates"]) + target = next(r for r in entry["registers"] + if r != bad[0][1] and r != bad[0][2][0]) + need(target != bad[0][2][0], "no distinct mutation target") + bad[0][2] = [target] + controls.append(must_reject( + "mutated_candidate_source_%d" % entry["frame"], + lambda bad=bad, entry=entry: bind_block_check(word, entry, bad))) + controls.append(must_reject( + "unpaid_gate_%d" % entry["frame"], + lambda entry=entry: bind_block_check(word, entry, entry["gates"][:-1]))) + first_splice = next(entry for entry in certificate["blocks"] if entry["spliced"]) + for entry in certificate["blocks"]: + if not entry["spliced"]: + continue + blk, ops, forward, n = bind_block(word, entry) + local, _ = block_model(entry["gates"], entry["registers"]) + reverse_old = integer_map(ops[::-1], n) + reverse_new = integer_map(local[::-1], n) + if dominated(reverse_new, reverse_old): + controls.append(must_reject( + "inverted_domination_%d" % entry["frame"], + lambda ro=reverse_old, rn=reverse_new: need(dominated(ro, rn), + "inverted domination holds"))) + else: + controls.append(must_reject( + "forged_domination_%d" % entry["frame"], + lambda ro=reverse_old, rn=reverse_new: need(dominated(rn, ro), + "forged domination claim holds"))) + bad_word = copy.deepcopy(candidate) + bad_word["C"].pop() + controls.append(must_reject("omitted_cleanup", lambda: whole_endpoint(bad_word))) + bad_word = copy.deepcopy(candidate) + first, last = first_splice["slice"] + del bad_word["B"][first] + bad_word["C"] = rebuild_cleanup(bad_word) + controls.append(must_reject("missing_gate_with_matching_cleanup", lambda: whole_endpoint(bad_word))) + bad_word = copy.deepcopy(candidate) + bad_word["B"][first][0] = 0 + controls.append(must_reject("illegal_frame_descent", lambda: frame_paths(bad_word))) + stale = copy.deepcopy(candidate) + stale["C"] = word["C"] + whole_endpoint(stale) # Positive semantic control; rejected only by literal H4. + controls.append(must_reject("stale_cleanup_literal_H4", + lambda: need(stale["C"] == rebuild_cleanup(stale), "H4 fails"))) + bad_cert = copy.deepcopy(certificate) + bad_cert["blocks"][0] = dict(certificate["blocks"][0], + slice=[certificate["blocks"][0]["slice"][0] + 1, + certificate["blocks"][0]["slice"][1] + 1]) + controls.append(must_reject("wrong_slice_binding", + lambda: bind_block(word, bad_cert["blocks"][0]))) + # A forged donor-supply certificate must be rejected by the counting recheck. + forged = dict(next(entry["witness"] for entry in certificate["blocks"] + if entry.get("witness")), demand=1, supply=2) + infeasible_entry = next(entry for entry in certificate["blocks"] if entry.get("witness")) + blk, ops, forward, n = bind_block(word, infeasible_entry) + controls.append(must_reject( + "forged_supply_witness", + lambda: need(supply_certificate(forward, forged["row"], forged["col"]) + == (forged["demand"], forged["supply"]), "forged certificate rejected"))) + + return {"status": "PASS_R439_BSECTION_SURVEY", "columns": columns, + "survey_frames": frames, "spliced_frames": sorted(spliced), + "survey_receipts": receipts, + "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": 5129, + "identical_register_frame_paths": len(after_paths), + "hypotheses": hypotheses, "conclusion": conclusion, + "bill_before": before_bill, "bill_after": after_bill, + "controls_rejected": controls} + + +def bind_block_check(word, entry, gates): + """Map equality for a proposed block replacement (negative-control path).""" + blk, ops, forward, n = bind_block(word, entry) + local, _ = block_model(gates, entry["registers"]) + need(integer_map(local, n) == forward, "forward integer map differs") + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--out", default=None) + parser.add_argument("--write-expected", action="store_true", + help="bootstrap EXPECTED.json receipts from this run") + args = parser.parse_args() + if args.write_expected: + global EXPECTED_MISSING_OK + EXPECTED_MISSING_OK = True + result = verify(args.out) + if args.write_expected: + expected = {"survey_frames": result["survey_frames"], + "spliced_frames": result["spliced_frames"], + "survey": result.pop("survey_receipts"), + "bill_before": result["bill_before"], + "bill_after": result["bill_after"]} + (HERE / "EXPECTED.json").write_text(json.dumps(expected, indent=1, sort_keys=True) + "\n", + encoding="utf-8") + print(json.dumps(result, indent=1, sort_keys=True)) + + +if __name__ == "__main__": + main()