diff --git a/research/r420-optimal-composed-pairs/CERTIFICATE.json b/research/r420-optimal-composed-pairs/CERTIFICATE.json new file mode 100644 index 0000000000..aad25199cd --- /dev/null +++ b/research/r420-optimal-composed-pairs/CERTIFICATE.json @@ -0,0 +1,129 @@ +{ + "status": "PASS_R420_OPTIMAL_COMPOSED_PAIRS", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "baseline": { + "semantic_word_sha256": "983aec23d244575ae6205c53ed8ccae2f4a2aa8171463eef71d64c6bfceafe40", + "scalar_stream_sha256": "6494f36ba4ce06ae142ab0f81c2178d91c6a1c0c812a57f40958e48635b1853c", + "binary_additions": 18378, + "D_binary_additions": 11562, + "D_grouped_gates": 634, + "forward_and_reverse": [ + { + "copies": 9, + "columns": 660 + }, + { + "copies": 9, + "columns": 660 + } + ], + "forward_prefix": 253149, + "reverse_prefix": 4334338, + "payload_prefix_upper": "19505369118995241654063407203584", + "payload_prefix_bits": 104, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "exported_records": 21336, + "record_sha256": "df920f588352d4d1d165d034655480c55f2182ae7fe4cee620d1a2c395c05b6b" + }, + "replacement": { + "semantic_word_sha256": "37e695efa7f5a941a63255a57fda688d28e84b38d9486f11ae47d64910f159f5", + "scalar_stream_sha256": "00db3567d098be8c5523191a75153fb053682d4bc5561b900e35509ae9b5c33c", + "binary_additions": 18362, + "D_binary_additions": 11546, + "D_grouped_gates": 638, + "forward_and_reverse": [ + { + "copies": 9, + "columns": 660 + }, + { + "copies": 9, + "columns": 660 + } + ], + "forward_prefix": 253149, + "reverse_prefix": 4334338, + "payload_prefix_upper": "19505369118995241654063407203584", + "payload_prefix_bits": 104, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "exported_records": 21320, + "record_sha256": "61331871038292444b4d8a2289e33da6ac999048c049cd9f86ea5fffcabef095" + }, + "saved_additions": 16, + "selected_ADDs": 26916, + "saved_from_selected": 8554, + "matching_optimum": { + "unordered_edges": 7140, + "oriented_edges": 14280, + "pairs": 58, + "saving": 1442, + "twice_dual_objective": 2884 + }, + "controls": [ + "omit helper preparation", + "omit target preparation", + "omit target restoration", + "omit helper restoration", + "omit middle read", + "D leaves frame zero", + "zero vertex prices", + "overlapping target pairs", + "feasible but nontight dual", + "inflated pair saving", + "certificate on original K", + "missing cleanup", + "neutral endpoint accepted and two ADDs charged" + ], + "PR733_matching_on_PR681_body": { + "semantic_word_sha256": "2f283fa62cfda57ee233604958ab02fbe5832899e18f0d10cd04b2623bc0b267", + "scalar_stream_sha256": "c23e94d72ff4cc878ca34ef500b52118e834ec1ffe521ab0a8415aaa68a0bce7", + "binary_additions": 18370, + "D_binary_additions": 11554, + "D_grouped_gates": 636, + "forward_and_reverse": [ + { + "copies": 9, + "columns": 660 + }, + { + "copies": 9, + "columns": 660 + } + ], + "forward_prefix": 253149, + "reverse_prefix": 4334338, + "payload_prefix_upper": "19505369118995241654063407203584", + "payload_prefix_bits": 104, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca" + }, + "saved_beyond_prior_matching_on_same_body": 8, + "inherited_PR733_ADDs": 18548, + "same_optimum_on_PR733_body_ADDs": 18540, + "literal_H2_claimed": false, + "semantic_D_columns": 660, + "no_new_kappa": true +} diff --git a/research/r420-optimal-composed-pairs/CLAIM.json b/research/r420-optimal-composed-pairs/CLAIM.json new file mode 100644 index 0000000000..f0f262d18e --- /dev/null +++ b/research/r420-optimal-composed-pairs/CLAIM.json @@ -0,0 +1,71 @@ +{ + "assignment_seed": 11, + "randomness": "One secrets.randbelow(100) draw, recorded before inspection", + "track": "bit supplier", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T05:29:14Z", + "claimed_utc": "2026-10-13T05:37:00Z", + "expected_finish_utc": "2026-10-13T06:20:00Z", + "object": "Exact disjoint target-pair optimum after the frozen PR694 helper basis, applied to PR681 composed body", + "method": "All 7140 unordered pair inequalities; integer vertex-price dual and exact finite circuit replay. Assignment seed 11 chooses target-pair optimality after inspecting three candidates.", + "deliverable": "One scoped optimum certificate and fully charged composed word, compared to selected PR543 and pending PR681/733; no new kappa.", + "candidates": [ + { + "task": "Certify target-pair optimum on KQ and apply to PR681", + "decision": "Selected. PR733 and PR681 use greedy matching, while PR716 certifies only the different original K matrix." + }, + { + "task": "Optimize the helper matching in PR694", + "decision": "Not selected. One probe improves helper-only gain from 6934 to 7002, but the simple vertex dual has a 146.5 gap and no exact optimum is claimed." + }, + { + "task": "Four-wire exact synthesis of R420 cleanup", + "decision": "Not selected. PR754 already exhausts the original disjoint-window class." + } + ], + "coordination": "No pinned sprint issue. GitHub search found one open issue, #650 about Discussions, so claim is local.", + "overlap": { + "open_PRs": 598, + "through_PR": 779, + "relevant": [ + 681, + 694, + 708, + 713, + 716, + 733, + 754, + 759, + 774 + ] + }, + "publication_status": "Complete local result; awaiting independent validation clearance", + "final_overlap": { + "through_PR": 799, + "new_relevant": { + "794": "6be7364e0245c5a1c931cb1c43b3da991b755850", + "789": "d1634f3b316f2c3a1bb5f93a6117c8ebab9ab011", + "790": "08b4a039ba4938dd4f4c89a69759f49ed21923ef" + }, + "PR681_and_PR733_heads_unchanged": true, + "main_unchanged": true + }, + "result": { + "local_ADDs": [ + 18378, + 18362 + ], + "fixed_helper_pair_optimum": 1442, + "native": "fresh 5/9/11-stage passed", + "hosted": "fresh parent/whole-owner/invoice passed", + "precision": "196 charged at 256; 432 charged at 512; unchanged from PR681", + "no_new_kappa": true, + "PR733_matching_on_same_PR681_body": 18370, + "new_ADD_saving_beyond_prior_matching": 8, + "emitted_local_invocation_events": [ + 6144768, + 6140160 + ], + "counter_scope": "288 expanded local streams; unchanged 69120 bridge ADDs and schedule/hosting work charged separately" + } +} diff --git a/research/r420-optimal-composed-pairs/HOSTED.json b/research/r420-optimal-composed-pairs/HOSTED.json new file mode 100644 index 0000000000..dc5fb2cc92 --- /dev/null +++ b/research/r420-optimal-composed-pairs/HOSTED.json @@ -0,0 +1,184 @@ +{ + "baseline": { + "parent_mutations": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ], + "hosted_audit": { + "status": "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT", + "template_sha256": "6a8436c8c33b88e3868086a124af88635bcd7f82e086a87d3159a7d5549fae66", + "emitted_program_sha256": "6d2c87e697b5b1a17efa0a34e815ebe5838c01151f15191d8b8d2f93f83e7edd", + "emitted_events": 6144768, + "profile": { + "1": 380160, + "2": 426624, + "4": 32640, + "5": 34560, + "6": 15360, + "7": 23040, + "8": 2592, + "42": 3456 + }, + "live": 30720, + "physical": 30729, + "hosted_residuals": 120960, + "bank_assignments": 0, + "rank_mass": 1956096, + "deficit": 9984, + "maxchild": 42, + "mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ] + }, + "bit_lower": "413456747036699736067/250000000000000000000000", + "bit_lower_decimal": "0.001653826988146798944268", + "invoice": { + "live": 30720, + "physical": 30729, + "maxchild": 42, + "rank_mass": 1956096, + "hosted_residuals": 120960, + "bank_assignments": 0, + "prefix_bits": 196, + "charged_prefix_bits": 256, + "coefficient_bits": 196, + "two_level_coefficient_bits": 432, + "charged_two_level_coefficient_bits": 512, + "row_coefficient": 18355, + "halving_depth": 2 + }, + "global_prefix_bound": "96186053138539774649262655619329340866394145487272925986816", + "bit_profile": { + "1": 380160, + "2": 426624, + "4": 32640, + "5": 34560, + "6": 15360, + "7": 23040, + "8": 2592, + "42": 3456 + }, + "local_additions": 18378 + }, + "replacement": { + "parent_mutations": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ], + "hosted_audit": { + "status": "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT", + "template_sha256": "528176278c3719970f984e5df9a28c970f73b5d6ac2ea6ea543deb4a9e9360c9", + "emitted_program_sha256": "b78f8e2dcb79f9d690b18e58cc2ba86972258dea487e1fd8700d5a4a28fb2f97", + "emitted_events": 6140160, + "profile": { + "1": 380160, + "2": 426624, + "4": 32640, + "5": 34560, + "6": 15360, + "7": 23040, + "8": 2592, + "42": 3456 + }, + "live": 30720, + "physical": 30729, + "hosted_residuals": 120960, + "bank_assignments": 0, + "rank_mass": 1956096, + "deficit": 9984, + "maxchild": 42, + "mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ] + }, + "bit_lower": "413456747036699736067/250000000000000000000000", + "bit_lower_decimal": "0.001653826988146798944268", + "invoice": { + "live": 30720, + "physical": 30729, + "maxchild": 42, + "rank_mass": 1956096, + "hosted_residuals": 120960, + "bank_assignments": 0, + "prefix_bits": 196, + "charged_prefix_bits": 256, + "coefficient_bits": 196, + "two_level_coefficient_bits": 432, + "charged_two_level_coefficient_bits": 512, + "row_coefficient": 18355, + "halving_depth": 2 + }, + "global_prefix_bound": "96186053138539774649262655619329340866394145487272925986816", + "bit_profile": { + "1": 380160, + "2": 426624, + "4": 32640, + "5": 34560, + "6": 15360, + "7": 23040, + "8": 2592, + "42": 3456 + }, + "local_additions": 18362 + } +} diff --git a/research/r420-optimal-composed-pairs/NATIVE.json b/research/r420-optimal-composed-pairs/NATIVE.json new file mode 100644 index 0000000000..94d759c4ec --- /dev/null +++ b/research/r420-optimal-composed-pairs/NATIVE.json @@ -0,0 +1,352 @@ +{ + "baseline": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 18378, + "containment_pairs_checked": 2460, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2940, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 671, + "paid_histogram": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5112, + "records": 21336, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "5": { + "bridge_controls_rejected": 6, + "receipt": { + "formal_columns_checked": 900, + "local_scalar_additions": 18378, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + }, + "9": { + "bridge_controls_rejected": 18, + "receipt": { + "formal_columns_checked": 1380, + "local_scalar_additions": 18378, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + }, + "11": { + "bridge_controls_rejected": 24, + "receipt": { + "formal_columns_checked": 1620, + "local_scalar_additions": 18378, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + } + } + }, + "replacement": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 18362, + "containment_pairs_checked": 2460, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2940, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 671, + "paid_histogram": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5112, + "records": 21320, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "5": { + "bridge_controls_rejected": 6, + "receipt": { + "formal_columns_checked": 900, + "local_scalar_additions": 18362, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + }, + "9": { + "bridge_controls_rejected": 18, + "receipt": { + "formal_columns_checked": 1380, + "local_scalar_additions": 18362, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + }, + "11": { + "bridge_controls_rejected": 24, + "receipt": { + "formal_columns_checked": 1620, + "local_scalar_additions": 18362, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "payload_prefix_bits": 104, + "payload_prefix_upper": "19505369118995241654063407203584", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "253149", + "reverse": false + }, + { + "bits": 23, + "cancellation_free_signed_row_l1_upper": "4334338", + "reverse": true + } + ] + } + } + } + } +} diff --git a/research/r420-optimal-composed-pairs/OPTIMUM.json b/research/r420-optimal-composed-pairs/OPTIMUM.json new file mode 100644 index 0000000000..19dcdf2da0 --- /dev/null +++ b/research/r420-optimal-composed-pairs/OPTIMUM.json @@ -0,0 +1,420 @@ +{ + "pairs": [ + [ + 208, + 214, + 27 + ], + [ + 222, + 219, + 46 + ], + [ + 144, + 149, + 35 + ], + [ + 236, + 234, + 42 + ], + [ + 161, + 164, + 3 + ], + [ + 198, + 178, + 26 + ], + [ + 139, + 141, + 39 + ], + [ + 228, + 226, + 10 + ], + [ + 188, + 150, + 11 + ], + [ + 157, + 155, + 16 + ], + [ + 133, + 131, + 35 + ], + [ + 134, + 128, + 31 + ], + [ + 184, + 175, + 15 + ], + [ + 170, + 189, + 31 + ], + [ + 159, + 167, + 8 + ], + [ + 217, + 220, + 28 + ], + [ + 172, + 190, + 11 + ], + [ + 218, + 223, + 18 + ], + [ + 229, + 227, + 27 + ], + [ + 162, + 135, + 24 + ], + [ + 154, + 205, + 25 + ], + [ + 225, + 231, + 36 + ], + [ + 207, + 202, + 24 + ], + [ + 235, + 237, + 25 + ], + [ + 171, + 186, + 22 + ], + [ + 216, + 221, + 22 + ], + [ + 169, + 187, + 19 + ], + [ + 213, + 215, + 20 + ], + [ + 174, + 173, + 35 + ], + [ + 123, + 126, + 19 + ], + [ + 124, + 122, + 24 + ], + [ + 151, + 146, + 24 + ], + [ + 233, + 239, + 42 + ], + [ + 156, + 200, + 34 + ], + [ + 181, + 196, + 32 + ], + [ + 136, + 142, + 25 + ], + [ + 199, + 179, + 26 + ], + [ + 152, + 158, + 24 + ], + [ + 211, + 209, + 23 + ], + [ + 201, + 160, + 14 + ], + [ + 132, + 129, + 7 + ], + [ + 193, + 194, + 34 + ], + [ + 182, + 176, + 33 + ], + [ + 143, + 137, + 41 + ], + [ + 204, + 165, + 10 + ], + [ + 238, + 232, + 24 + ], + [ + 197, + 180, + 17 + ], + [ + 230, + 224, + 40 + ], + [ + 168, + 177, + 14 + ], + [ + 163, + 166, + 20 + ], + [ + 145, + 148, + 44 + ], + [ + 185, + 191, + 32 + ], + [ + 212, + 210, + 23 + ], + [ + 183, + 195, + 20 + ], + [ + 203, + 206, + 11 + ], + [ + 138, + 140, + 28 + ], + [ + 127, + 121, + 11 + ], + [ + 120, + 125, + 35 + ] + ], + "gain": 1442, + "doubled_vertex_prices": [ + 35, + 9, + 44, + 31, + 4, + 35, + 7, + 13, + 18, + 0, + 0, + 70, + 14, + 0, + 44, + 38, + 12, + 78, + 50, + 50, + 6, + 28, + 38, + 4, + 60, + 6, + 22, + 0, + 82, + 10, + 10, + 26, + 48, + 0, + 42, + 32, + 8, + 0, + 0, + 0, + 28, + 0, + 10, + 5, + 6, + 20, + 35, + 16, + 12, + 22, + 4, + 14, + 20, + 16, + 54, + 12, + 4, + 16, + 42, + 22, + 16, + 34, + 62, + 16, + 18, + 8, + 30, + 16, + 12, + 58, + 2, + 56, + 0, + 22, + 46, + 24, + 30, + 18, + 10, + 30, + 60, + 0, + 48, + 0, + 0, + 8, + 22, + 0, + 23, + 16, + 22, + 30, + 24, + 10, + 31, + 30, + 10, + 24, + 21, + 22, + 32, + 34, + 70, + 15, + 22, + 0, + 18, + 18, + 2, + 36, + 58, + 72, + 48, + 77, + 41, + 9, + 43, + 41, + 0, + 7 + ], + "assignment_seed": 11, + "scope": "Target disjoint-pair substitutions on KQ with PR694 helper recipe fixed", + "nomination": "One scipy.optimize.milp nomination after random.Random(11) shuffles all 7140 unordered edges. Floating solvers nominate only; the integer dual is the proof." +} diff --git a/research/r420-optimal-composed-pairs/PACKAGE-TESTS.json b/research/r420-optimal-composed-pairs/PACKAGE-TESTS.json new file mode 100644 index 0000000000..54fa3b92e1 --- /dev/null +++ b/research/r420-optimal-composed-pairs/PACKAGE-TESTS.json @@ -0,0 +1,47 @@ +[ + { + "test": "relocated normal primary", + "exit_code": 0, + "tail": "PASS_R420_OPTIMAL_COMPOSED_PAIRS optimum=1442 pairs=58 edges=7140 ADDs=18378->18362 payload_bits=104 columns=660 controls=13 no_new_kappa" + }, + { + "test": "relocated optimized primary", + "exit_code": 0, + "tail": "PASS_R420_OPTIMAL_COMPOSED_PAIRS optimum=1442 pairs=58 edges=7140 ADDs=18378->18362 payload_bits=104 columns=660 controls=13 no_new_kappa" + }, + { + "test": "relocated independent", + "exit_code": 0, + "tail": "PASS_R420_COLUMN_MATCHING optimum=1442 coefficients=50400 edges=7140 boolean_columns=540 D_ADDs=11546 controls=4" + }, + { + "test": "recompressed identical source", + "exit_code": 0, + "tail": "PASS_R420_OPTIMAL_COMPOSED_PAIRS optimum=1442 pairs=58 edges=7140 ADDs=18378->18362 payload_bits=104 columns=660 controls=13 no_new_kappa" + }, + { + "test": "corrupt source payload", + "exit_code": 1, + "tail": "ValueError: base source changed: research/e8-bit-r420/data/bitE8mut-r420.json.gz" + }, + { + "test": "corrupt receipt", + "exit_code": 1, + "tail": "ValueError: committed certificate differs" + }, + { + "test": "corrupt matching score", + "exit_code": 1, + "tail": "ValueError: oriented matching price" + }, + { + "test": "existing output protected", + "exit_code": 1, + "tail": "ValueError: output already exists" + }, + { + "test": "missing source fails", + "exit_code": 1, + "tail": "FileNotFoundError: [Errno 2] No such file or directory: '/research/e8-bit-r420/data/bitE8mut-r420.json.gz'" + } +] diff --git a/research/r420-optimal-composed-pairs/README.md b/research/r420-optimal-composed-pairs/README.md new file mode 100644 index 0000000000..41dcb4e3a6 --- /dev/null +++ b/research/r420-optimal-composed-pairs/README.md @@ -0,0 +1,226 @@ +# An exact target-pair optimum for the composed R420 word + +This is a finite bit-circuit improvement and a restricted optimality certificate. +It replaces the greedy target matching in Alluri's pending PR681 composition +with 58 pairs that attain the exact optimum for that matching class. + +The complete local word falls from **18,378 to 18,362 binary ADDs**. Both positive +prefix maxima remain exactly **253,149 forward and 4,334,338 reverse**. The +payload bound remains +`64 * 253149^3 * 4334338^2 = 19505369118995241654063407203584 < 2^104`. +There is **no new kappa** and no global circuit-optimality claim. + +The new optimum saves **eight ADDs beyond PR733's existing pairing applied to +the same PR681 body**, whose complete cost is 18,370. The 16-ADD comparison is +against the actually published PR681 word, which uses a different greedy +matching. Both baselines are explicit in the verifier. + +The main contribution is the closed optimization gap. The fixed PR694 helper +basis permits at most **1,442** further ADD savings from disjoint target-pair +substitutions. The two pending greedy constructions attain 1,426 and 1,434. +`OPTIMUM.json` supplies an attaining matching and 120 nonnegative integer +prices. A solver-free checker verifies all 7,140 edge inequalities and equality +of the primal and dual totals. A separate column-incidence implementation +checks the same certificate without importing the first checker. + +## Exact comparisons + +All figures count preparation, helper reads, target mixing and restoration. +These are counts of scalar operations, not measured multiplication runtimes. + +| Construction | D ADDs | Complete local ADDs | Local payload bits | +| --- | ---: | ---: | ---: | +| Selected PR543 R420 | 19,922 | 26,916 | 100 | +| PR694 helper pairs | 12,988 | 19,982 | 102 | +| PR733 two-sided composition | 11,554 | 18,548 | 103 | +| PR681 composed word | 11,562 | 18,378 | 104 | +| PR733's existing matching on the same PR681 body | 11,554 | 18,370 | 104 | +| This matching on the PR681 body | 11,546 | 18,362 | 104 | + +The improvement over the actually published PR681 word is **16**; the gain +beyond the strongest prior fixed-KQ matching on the same body is **eight**. +The 8,554 figure is the cumulative reduction +from PR543 and includes all predecessors. Applying the same matching to PR733's +unchanged body gives a local count of 18,540, only eight below that predecessor. +The submitted native and hosted replay uses the PR681 body. No pending selected +frontier proposal is promoted or displaced. +The 18,370 same-body comparator is reconstructed from PR733's pinned 57-pair +recipe, with the identical helper-recipe hash, exact full endpoints, frame +paths and both prefix bounds checked. It has not received a separate third +hosted replay; the fresh native/hosted runs compare published PR681 with the +submitted word. + +Fresh hosted replay gives **6,144,768 -> 6,140,160 emitted local-invocation +events**, a further 4,608 reduction across 288 expanded calls. This counter +excludes separately charged bridge and schedule work, including 69,120 bridge +ADDs. Those charges are unchanged; no complete-machine instruction total is +claimed. Both versions need 196 raw prefix bits, +charged at **256**, and 432 two-level bits, charged at **512**. Those are +PR681's enlarged charges; this result does not recover the selected word's +192-bit prefix allocation. + +The final overlap refresh through PR799 found +[PR794](https://github.com/CrocSwap/integer-mult-bounds/pull/794) at +`6be7364e0245c5a1c931cb1c43b3da991b755850`. Its successive target-basis +factorization reports 19,037 local ADDs with a **192-bit** hosted prefix charge. +That is a different operation-count/precision tradeoff and a larger target +circuit class. This certificate does not supersede it. PR789/790 change other +phase-B blocks; they are not composed here. PR799's larger conditional kappa +uses different complex and bit suppliers and is outside this fixed R420 class. + +The PR681 baseline is reconstructed from its exact component recipes. Its +entire local bit receipt, including the canonical word, scalar stream, native +record digest, both prefix maxima and the complete paid profile, must equal +the original committed PR681 receipt before this checker accepts the comparison. + +## Reproduce + +From the repository root, Python 3.10 or later with the standard library: + +```sh +python3 -I -B research/r420-optimal-composed-pairs/verify.py +python3 -I -B research/r420-optimal-composed-pairs/independent_check.py +``` + +Expected final lines: + +```text +PASS_R420_OPTIMAL_COMPOSED_PAIRS optimum=1442 pairs=58 edges=7140 ADDs=18378->18362 payload_bits=104 columns=660 controls=13 no_new_kappa +PASS_R420_COLUMN_MATCHING optimum=1442 coefficients=50400 edges=7140 boolean_columns=540 D_ADDs=11546 controls=4 +``` + +`--out /absolute/fresh/directory` retains both words, original-exporter records +and `LOCAL.json`. Existing output directories are refused. Normal commands +compare the entire deterministic receipt with `CERTIFICATE.json`. The authoring +option `--record /fresh/file.json` writes a candidate receipt and deliberately +does not print a certificate PASS. + +For fresh unchanged C++17/Boost cohort checks, append `--native`. For the complete +nine-stage parent, hosted and invoice replay, use: + +```sh +BOOST_INCLUDE=/directory/containing/boost python3 -I -B research/r420-optimal-composed-pairs/verify.py --hosted --out /absolute/fresh/output +``` + +The hosted command also needs NumPy, SciPy and SymPy, as the retained PR543 chain +does. `native.py` and `hosted.py` are byte-for-byte PR681 drivers, credited there +to Alluri and Ali Romman. They compile the original checkers and consume the +actual new word. They do not substitute stored predecessor outputs. +The caller compares every deterministic native/hosted receipt field with the +shipped receipts, excluding only runtime seconds. It also rejects a missing +helper restoration with each of the three native column checkers. The hosted +driver's PR484 outer calculation is a historical arithmetic control, not a +fresh selected PR626 complex-supplier or outer-assembly replay. + +## The exact class and proof + +Write the accepted helper-to-target matrix as `K`. Fix all 201 oriented, +disjoint helper pairs from Greer Guthrie's PR694 recipe. Their temporary helper +change is `Q`, with `Q^-1 = Q`. The matrix read during the middle becomes +`M = KQ`. Preparing and restoring these helpers costs 402 ADDs. The direct +middle costs 12,586 ADDs, so the helper-only D cost is 12,988. + +For two distinct targets `a,b`, prepare `y_b += y_a`, inject `M_a` into target +`a` and `M_a XOR M_b` into target `b`, then restore `y_b += y_a`. Arbitrary +initial target values are preserved and the result adds `M_a,M_b` as required. +If `w_i` is the number of nonzero helper coefficients in row `i`, the net +saving in orientation `a -> b` is + +```text +g(a,b) = w_b - weight(M_a XOR M_b) - 2. +``` + +The two operations subtracted are the target preparation and restoration. +Disjoint target pairs do not alter one another's rows. Thus a pairing has +exactly the sum of its oriented savings. For each unordered edge define +`w_ab = max(0, g(a,b), g(b,a))`. + +Let the supplied integer prices be `q_i`. The checker verifies +`q_a + q_b >= 2*w_ab` on every one of the 7,140 unordered pairs, `q_i >= 0`, +and `sum(q_i) = 2,884`. For any disjoint matching, summing its inequalities +counts each price at most once, so its saving is at most `2,884/2 = 1,442`. +The 58 supplied oriented pairs attain 1,442. This proves the optimum even +when unmatched targets and either orientation are allowed. It is an exact +finite mathematical certificate, independent of a solver's reported gap. + +The charged new D cost is +`201 + 58 + 11028 + 58 + 201 = 11546`. +The middle is `PKQ`; keeping `PK` from an untransformed matrix is invalid. +The verifier executes the full D operator on arbitrary target and helper +inputs, then checks all 660 inputs of the whole word in both directions. +The independent checker builds columns, counts pair incidences and runs every +one of the 540 literal Boolean target/helper input columns of D separately. +The remaining 120 source inputs are untouched by D. + +The class fixes `Q`, the non-D circuit, direct middle-row injection and the +disjoint-pair recipe. It excludes different helper bases, overlapping pairs, +target trees, general XOR synthesis and changed frames or copied totals. +The dual bound ignores precision constraints, but the attaining word passes +the existing precision cap. Consequently it is also optimal in this exact +fixed-body pairing class subject to that cap. No optimum is claimed outside +that class or for the choice of the helper basis itself. + +## Scope, controls and provenance + +The temporary target/helper bases violate literal H2's helper-only D syntax. +The original H2 guard and literal K extractor still reject them. The canonical +body with the original D passes every H1-H5 hypothesis; exact equality of the +complete D boundary map supplies the semantic substitution. No predecessor +checker is edited or weakened. All frame paths, 420 helpers, nine COPY/ERASE +lifecycles and paid rank mass 5,112 are retained. + +Controls omit helper or target preparation/restoration, remove a middle read, +move D off frame zero, corrupt the dual or pair scores, reuse an original-K +certificate, and omit cleanup. A neutral pair is accepted as an endpoint but +charged two ADDs. The second checker separately rejects four certificate +mutations. Detailed native/hosted results and package-integrity tests are in +`VALIDATION.md`. + +Exact base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected assembly +remains PR626, `660de893d27bb7abd1d5b01b1640207528a5c851`, conditional kappa +`0.001635527380375392`, using PR543 +`2065fe4f72a914d907f1046603f5a36f17018535`. +The immediate composed source is PR681 +`e536f6fc8aad65adef8ac4682d13625598a5c3f9`; PR733 is +`dfe84e09298abc5c5e0074afda59a821e10abfb4`. +`SOURCES.json` pins the imported bytes and Git blobs and the inherited replay +files. Compressed main inputs are compared by decompressed payload. + +Assignment seed **11** came from one OS-random draw. `CLAIM.json` records the +three candidate scopes and overlap scan. SciPy/HiGHS nominated one matching +after seed-11 edge ordering, and a linear program nominated the vertex prices. +These floating computations are discovery only. The frozen integer certificate +checks the complete stated domain, with no search-based impossibility claim. +One earlier unseeded target probe and one helper-matching probe were discarded +before selecting the final artifact. The helper probe's solver optimum is not +certified or asserted here. There was no pinned coordination issue. + +The inherited all-size/compiler/common-label/mutable-basis, physical hosting, +precision/tape/exact-recovery and analytic assumptions remain. A finite replay +does not prove the full multiplication theorem. Full repository regeneration, +selected-frontier cold replay, Lean and remote CI are not claimed. The selected +frontier and `upstream/` are unchanged. + +## Credit + +Prepared for **Sagar Thakrar / @thakrarsagar**, with substantial **OpenAI Codex +assistance** in implementation, proof analysis, verification and writing. +There is no independent human-review claim. Apache-2.0 applies to the additions. + +This extends Alluri's [PR681](https://github.com/CrocSwap/integer-mult-bounds/pull/681) +composition. The helper basis is Greer Guthrie's +[PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694), following +PR686. The two-sided composition is Scott Woolsey Biggart's +[PR733](https://github.com/CrocSwap/integer-mult-bounds/pull/733), following his +PR713 target factoring and the earlier PR476/450 lineage. Sagar Thakrar's +[PR716](https://github.com/CrocSwap/integer-mult-bounds/pull/716) supplied the +vertex-price certificate method for the different original-K pairing problem. +No priority for these mechanisms or the certificate method is claimed. + +The fixed body retains yongjae321's PR670, x0hu's PR674, Ali Romman's PR688, +mtpsl's PR691 and Sagar Thakrar's PR708. The accepted supplier is eumemic's +PR543/493, with Dylan Crow's exporter/checker lineage, DreamingOfClouds' retained +totals and hosting chain, Zhihao Chen's scalar interface, and all contributors +credited in the original PR681 notice, retained unchanged under `vendor/`. +Concurrent PR754 cleanup synthesis and PR759/774 target forests concern larger +or different classes and are neither imported nor superseded. diff --git a/research/r420-optimal-composed-pairs/SOURCES.json b/research/r420-optimal-composed-pairs/SOURCES.json new file mode 100644 index 0000000000..8b5bebb2fa --- /dev/null +++ b/research/r420-optimal-composed-pairs/SOURCES.json @@ -0,0 +1,649 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "PR543": "2065fe4f72a914d907f1046603f5a36f17018535", + "PR626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "PR681": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "PR733": "dfe84e09298abc5c5e0074afda59a821e10abfb4", + "imported": { + "vendor/pr694-recipe.json": { + "source_path": "research/r420-compensation-basis/RECIPE.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "df48dd3b1c8d1d0f8894bb901043a9a8ba21777ecdacb21800c22fd71290d01e", + "git_blob": "d81608927fd166b166b873eaa4125d2cc63c38a1" + }, + "vendor/pr681-targets.json": { + "source_path": "research/supplier-circuit-consolidation/TARGET-RECIPE.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "ae21ad955134671fbf37ea9f9b1a0a2933fc521dbe4f8ab96b89c8fbc4e2d433", + "git_blob": "f102e89b0420fd98eab55be073a7b1461d43d3d5" + }, + "vendor/pr681-decoders.json": { + "source_path": "research/supplier-circuit-consolidation/DECODER-RECIPE.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "e3c8c9268f7325b298495ff63dc5b0d0e6f54026d313536dd94a6ac0072c9ca7", + "git_blob": "ad6bfff6c5661c76da346e3bafea17c7ff9650df" + }, + "vendor/pr691-quad.json": { + "source_path": "research/r420-quad13/WITNESS.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "444f9156ac2d359af45ce0f90e63c81c6400b81d57d36edb3f033a798269f354", + "git_blob": "6112423a46b7b8841ec5f4ca155b9969879e05ee" + }, + "vendor/pr670-block.json": { + "source_path": "research/r420-two-block-composition/vendor/pr670/candidate.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "56044254a15b52ae91ec166f37ba8a75c63df05d62f4e13fa594df86677ba3f8", + "git_blob": "325c18cd442bc97de6abc70e29270be369ae2fce" + }, + "vendor/pr674-block.json": { + "source_path": "research/r420-two-block-composition/vendor/pr674/certificate.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "8283275a39b5b7167e562af95a9cfe7cc4602385523ca653900b62f4da2a77fe", + "git_blob": "cc1657413365ba695f6d610186c761f64e160ef5" + }, + "vendor/pr681-expected.json": { + "source_path": "research/supplier-circuit-consolidation/EXPECTED.json", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "62dab37db906d36609b8ac9efeda83c10fd04b000acdc5ec2b93de38db85bf21", + "git_blob": "f2b4e8bd55bd93a02886b5831e29a1f8877ac958" + }, + "vendor/pr681-notice.md": { + "source_path": "research/supplier-circuit-consolidation/README.md", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "f5300e901f4fcb7a815b16b6f5002009c6fe78b63f5eff8a92d15ca65ff2e700", + "git_blob": "638ce1b8d8cda407b719809b2e7518dc66ebbeae" + }, + "native.py": { + "source_path": "research/supplier-circuit-consolidation/native.py", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "18d7641d8eb65d6653756d19812f7ee8ada1df4c5522386247263d2dbad759ce", + "git_blob": "e529444ac7ea0e1ea869d3753b0d8d7e0fbd3e47" + }, + "hosted.py": { + "source_path": "research/supplier-circuit-consolidation/hosted.py", + "source_commit": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "sha256": "060c2804d14fc2735271e18c284fcac81939a42abf8ef62d42539f74fb0dc3ab", + "git_blob": "79982c7bbe320c20c15a912ecc7535e36e295679" + }, + "vendor/pr733-targets.json": { + "source_path": "research/r420-two-sided-basis/RECIPE.json", + "source_commit": "dfe84e09298abc5c5e0074afda59a821e10abfb4", + "sha256": "c04a7e3acb6acbf23b52fda4a2a9109023a94307be6d978434a840d53b1cb08a", + "git_blob": "7c6acd2a105de8281324921c6b890faeef1982f7" + } + }, + "base_files": { + "research/e8-bit-r420/DEPENDS.json": { + "representation": "file-bytes", + "sha256": "fa9253078c444b8f4a57e849048f727c3c8233c3dc3c7f651bef2cf7bb0178c5" + }, + "research/e8-bit-r420/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d" + }, + "research/e8-bit-r420/LICENSE": { + "representation": "file-bytes", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + "research/e8-bit-r420/MANIFEST.sha256": { + "representation": "file-bytes", + "sha256": "e76447d8b457d3701c97f7f972b24779910cb6517af27f8b5e37d026de28c81f" + }, + "research/e8-bit-r420/NOTICE.md": { + "representation": "file-bytes", + "sha256": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811" + }, + "research/e8-bit-r420/README.md": { + "representation": "file-bytes", + "sha256": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f" + }, + "research/e8-bit-r420/SOURCE-pr510.json": { + "representation": "file-bytes", + "sha256": "5e84c26ba837ce029acd1b5089e5533d2ebde793deede84215322112e95e06f8" + }, + "research/e8-bit-r420/SOURCE-pr535.json": { + "representation": "file-bytes", + "sha256": "74254fde5cff5580d5c199b139ff3ce31a3defded3f653a3ba83cf0c9204ddc4" + }, + "research/e8-bit-r420/code/adapt11.py": { + "representation": "file-bytes", + "sha256": "46c205f6036bb8635a34ab6ef2c54a9e446bec1435fcc14ab55949a5dbee8aa4" + }, + "research/e8-bit-r420/code/cited.py": { + "representation": "file-bytes", + "sha256": "1770f4eb61e130e3cc6e23f67507d8bb7587baaf8391d749c2e7fe5c66089044" + }, + "research/e8-bit-r420/code/gen_l3.py": { + "representation": "file-bytes", + "sha256": "d5c802447c99255db1bdfcae62b2116bfc9612c9dc9000d41aa4f5f2fec9f2f2" + }, + "research/e8-bit-r420/code/mutants.py": { + "representation": "file-bytes", + "sha256": "e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594" + }, + "research/e8-bit-r420/code/mutrec_b.py": { + "representation": "file-bytes", + "sha256": "231cbf26bfe5e6824347e4556959941d8b4dea1efa06d7f88d7a73cca8b03158" + }, + "research/e8-bit-r420/code/nodeopt.py": { + "representation": "file-bytes", + "sha256": "6a5896f60b1fe05c41ab28ce822dff782c635e12d0c74fad20b5ce2a4010fa3f" + }, + "research/e8-bit-r420/code/planio.py": { + "representation": "file-bytes", + "sha256": "c0a687f61aed29455cea953d8a3e49a32136edb3cd4213c46880c146a6ca7fa3" + }, + "research/e8-bit-r420/code/provenance.py": { + "representation": "file-bytes", + "sha256": "aade757c1e4e2714207cbc80a9a60793d84b5f009de2cac79ee8d3239986fd2a" + }, + "research/e8-bit-r420/code/summary.py": { + "representation": "file-bytes", + "sha256": "afdf2e53648b417fcc49cd05e9a18ee9fff9ae41e791a6ffa333130e30f35feb" + }, + "research/e8-bit-r420/code/xcheck.py": { + "representation": "file-bytes", + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + }, + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "representation": "gzip-payload", + "sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2" + }, + "research/e8-bit-r420/data/complex-b.json": { + "representation": "file-bytes", + "sha256": "ec81d67d8a82d41859ee33a4e387679b71e5ced15de074a71195d08969dd308a" + }, + "research/e8-bit-r420/data/complex/pr535/EXACT-ASSEMBLY-PR493.json": { + "representation": "file-bytes", + "sha256": "3f4be566309841e00e842d5686f7937a355ae1a6a2eaa3ccb07bdf8a9ca604fb" + }, + "research/e8-bit-r420/data/complex/pr535/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "cb734055c36681d38cf431a6926b7713351a94073cfba37d70a5384a9ef0d178" + }, + "research/e8-bit-r420/data/hosting11-r420.json": { + "representation": "file-bytes", + "sha256": "d7964e04604f804b2b334a989087a5e855243160f4d40cf9336d9b25995ac5d8" + }, + "research/e8-bit-r420/data/plan-l3.json": { + "representation": "file-bytes", + "sha256": "d5c2494b4baae801143049e172db303b3c8e25a002e9d9715a1d79dcb2d74c58" + }, + "research/e8-bit-r420/data/selection9-r420.json": { + "representation": "file-bytes", + "sha256": "9737b5f39367ee5a8affa52e5fbb92d1408f0f9e9f14ed64d6f00ea9428b291c" + }, + "research/e8-bit-r420/discovery/README.md": { + "representation": "file-bytes", + "sha256": "9970e45fd1d5b34a2a384dee0e2768b6f17f85d26751860cd649d12144604e3c" + }, + "research/e8-bit-r420/discovery/planL3.py": { + "representation": "file-bytes", + "sha256": "dd65e617aa786754520ca839988a6f0a87af53ca108e2bd722bfd69ee2c71508" + }, + "research/e8-bit-r420/discovery/planL3b.py": { + "representation": "file-bytes", + "sha256": "7179039fddf3ea12c9cb1d61fad6668f3282b50afdc43c7948d0bfc3a2b35c77" + }, + "research/e8-bit-r420/requirements.txt": { + "representation": "file-bytes", + "sha256": "e11a6f5c2a40b77fbf54a31a4c45bac575e9d2f765d35b657406d5f088fd0664" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-dead-totals/data/bitE8mut-r480.json.gz": { + "representation": "gzip-payload", + "sha256": "8639e22008c24a5690dd250eba702fe5fca85ddd036dcbec20baba77b7e213ba" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "883f7a1a84f31d9e4430e348bc8d9c1ec10210b206ff602dbe126349056af13d" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/code/adapt.py": { + "representation": "file-bytes", + "sha256": "27b6b77cc4ebf439f9019e63a22dedc1ef72ee65fe120aad3d17316b1df06d7b" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/code/assemble9.py": { + "representation": "file-bytes", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/data/selection9-r480.json": { + "representation": "file-bytes", + "sha256": "8176db518bed23ea8121543bfb18085ec6633064142ba40ac5db00f63b06553d" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py": { + "representation": "file-bytes", + "sha256": "57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_parent_k.py": { + "representation": "file-bytes", + "sha256": "374e1d983589463bbfa06b6e9f2ffafb9d2c14acf97b1f858593a3cef90e93d2" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/bank_routes_k.py": { + "representation": "file-bytes", + "sha256": "ea678a7befda10c6f1b9dd38a36fe1437c6468472bd649f60b9f01522047e0bf" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py": { + "representation": "file-bytes", + "sha256": "298b16c3d4f58a468ad1a64564c8500cb281414a3f3c0428fd467908eeb4a4b4" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": { + "representation": "file-bytes", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/hosting_k.py": { + "representation": "file-bytes", + "sha256": "081c3b95b18d900d97ce82af64fb428f085b6adc6d8ca93ea920797dad7eb81e" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/bank_routes.py": { + "representation": "file-bytes", + "sha256": "7c6997c455bd55acca3a1603797c34e7733d557c27a7694a1429ff15773a505d" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/config.py": { + "representation": "file-bytes", + "sha256": "283d7fad45155ee91e704d63ec947cf4a60aeff5cc43510bc0e835f7da7d8767" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/e8core.py": { + "representation": "file-bytes", + "sha256": "1cb286196c1530d06f50f0997febc5993b388f33464e295611b920ba30a24eeb" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/base_two_moment.py": { + "representation": "file-bytes", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/moment.py": { + "representation": "file-bytes", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/outer.py": { + "representation": "file-bytes", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/tile_m.py": { + "representation": "file-bytes", + "sha256": "d6ae4a556472d403773cd2117c992bfc10e1187112da1b3893f3fae628a131dd" + }, + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py": { + "representation": "file-bytes", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + "research/e8-bit-r420/verify.sh": { + "representation": "file-bytes", + "sha256": "3192dea51acd17addb2750834a9dc3fb5b991e8dc5970ba9d2ac54608d79cafa" + }, + "research/e8-bit-carrier-skeleton/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "3494ba83280cc86548fe0cc6695c50d23e6b6ffca85aeb1a33337c1196e280cb" + }, + "research/e8-bit-carrier-skeleton/LICENSE": { + "representation": "file-bytes", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + "research/e8-bit-carrier-skeleton/MANIFEST.sha256": { + "representation": "file-bytes", + "sha256": "7f25c41d0400ef5adf763eae6e166003a9b59e5a655b860c04b052f6731c7297" + }, + "research/e8-bit-carrier-skeleton/NOTICE.md": { + "representation": "file-bytes", + "sha256": "5f4b7fcbf99f572be28b6da612ce775363908cdfc7810f7aca167be01c86e49a" + }, + "research/e8-bit-carrier-skeleton/README.md": { + "representation": "file-bytes", + "sha256": "e5212e8058c92a2b02cc12b4e174a65ce1cef7b4d7977ae770e64f5ff91b7204" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr370.json": { + "representation": "file-bytes", + "sha256": "03de1d341196cfa8cf1d39f3cc8648b25bb5f39c3c602a728cfbd089e8253ac0" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr381.json": { + "representation": "file-bytes", + "sha256": "16b1977240ca9acb58fa64572fb4231a423bc10bbf3e7bb30f1c8201fe369ba5" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr386.json": { + "representation": "file-bytes", + "sha256": "87c659ba932525631a40be14dca28a6a2efade8641f23bb08d6e1567fc991131" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr436.json": { + "representation": "file-bytes", + "sha256": "4a4f99f5bdb7530a0dcf9433f7f02afbf2abf908e718f7c63ffa5503d4f49693" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr445.json": { + "representation": "file-bytes", + "sha256": "e6f4a272442bb71ef68aaa3545b271236f9c99297e444fa01c62b0b5fb6a170f" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr448.json": { + "representation": "file-bytes", + "sha256": "c771fa9be492408a78d6d970c839e68c4dfd1b66f4f4a4748e3d12726a43cf27" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr451.json": { + "representation": "file-bytes", + "sha256": "a639956eec858341987a815b7464ef472505300db754b5f9ac012dd01d18c8df" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr458.json": { + "representation": "file-bytes", + "sha256": "cbdea984a46ab5de354b95e73fd76c1918fdc6676c658398a552772c4dc3dcaf" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr471.json": { + "representation": "file-bytes", + "sha256": "499d861e090c9e646d978dd67890a8e58a9ff6bf08512684e66605179132076b" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr472.json": { + "representation": "file-bytes", + "sha256": "6753bcf50c91806b75dd4dbe3963a79699a614d0dab8ce32b261cc3e76b288b1" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr473.json": { + "representation": "file-bytes", + "sha256": "2515c4f23dfa22a21913d92597669770f7f44c2a5b3ef069ef68a0c89779a656" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr478.json": { + "representation": "file-bytes", + "sha256": "9c7c4ea678865a955b0c89f0952927159976fdf55cadc6a488dec5757f03fe7d" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr483.json": { + "representation": "file-bytes", + "sha256": "24e3eab4a985e115adb7f8665a401423e9636e9f16cc4373ec68cc86950445a8" + }, + "research/e8-bit-carrier-skeleton/SOURCE-pr484.json": { + "representation": "file-bytes", + "sha256": "b92f43fbcba3921a1aa37bcb9f05cf5fa612ff708785e05512438a6317bf0867" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": { + "representation": "file-bytes", + "sha256": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": { + "representation": "file-bytes", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/gram_frames.py": { + "representation": "file-bytes", + "sha256": "223a5a07731fc315a90a3e48177796babc155c1d9985c7ae5017eff6af2a0608" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": { + "representation": "file-bytes", + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": { + "representation": "file-bytes", + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3" + }, + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": { + "representation": "file-bytes", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + "research/e8-bit-carrier-skeleton/code/bit/independent/checkword.py": { + "representation": "file-bytes", + "sha256": "11bf9620ca9db16d52d9fe806b814fc9ec9a89c4d7645354d1861d96f6e805ad" + }, + "research/e8-bit-carrier-skeleton/code/bit/independent/interface.py": { + "representation": "file-bytes", + "sha256": "2c63a039f97e3a11ce5a6b83302d4f5beda160c1db14164a5a9b0855aeb19d3c" + }, + "research/e8-bit-carrier-skeleton/code/bit/independent/mutate.py": { + "representation": "file-bytes", + "sha256": "0ff65aace5da4b57d96235bf830f8f11969322e75134d498aeb70e9753ec6b0d" + }, + "research/e8-bit-carrier-skeleton/code/bit/independent/mutate_mut.py": { + "representation": "file-bytes", + "sha256": "3b002c19a5dcca76a5594f2a30fac7c01d2b45fc96b3e7cfbfd8b720f5ffb4e8" + }, + "research/e8-bit-carrier-skeleton/code/bit/independent/relax.py": { + "representation": "file-bytes", + "sha256": "d6e9f58de3fa41f538516b6227c249d61fb30f0f6843027cc8a07a1a372fa6b6" + }, + "research/e8-bit-carrier-skeleton/code/bit/mutate_records.py": { + "representation": "file-bytes", + "sha256": "b0e75d6550412a7be4017695e6b237392b611bb852ad8ff309d6682c9f166a4e" + }, + "research/e8-bit-carrier-skeleton/code/bit/mutate_records_mut.py": { + "representation": "file-bytes", + "sha256": "a9e085ec60d5657cd5d77832e3d95004e81b9f4f249d9e0fc95e345366cb2d2e" + }, + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": { + "representation": "file-bytes", + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + "research/e8-bit-carrier-skeleton/code/cited.py": { + "representation": "file-bytes", + "sha256": "a4c2dd4755f2a45ceda327b36d9ee400c2804893000626ca8ff3f6ee296fd842" + }, + "research/e8-bit-carrier-skeleton/code/eleven/adapt.py": { + "representation": "file-bytes", + "sha256": "d8a8c13b484d985f0133a5d06de4a78b8477314f922b9f693ba73640b7184d6b" + }, + "research/e8-bit-carrier-skeleton/code/eleven/assemble.py": { + "representation": "file-bytes", + "sha256": "c47889a606701ae592374dd82a13cee8c5a4e8449b7facfdad2d90563a30a18c" + }, + "research/e8-bit-carrier-skeleton/code/eleven/audit.py": { + "representation": "file-bytes", + "sha256": "5ad832830c19ec6c904d1b64480f6b1e71c5673fdd38d487d17e179b1d197c09" + }, + "research/e8-bit-carrier-skeleton/code/eleven/emit.py": { + "representation": "file-bytes", + "sha256": "b0b25955875625ed63f82690f83aef976e3e9a978ae6620b23a23fc1207acd46" + }, + "research/e8-bit-carrier-skeleton/code/eleven/local_audit.py": { + "representation": "file-bytes", + "sha256": "95275473d7f9811011bda760dd0f04de5169c2a6922456dc9a5725a5d671f941" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/code/assemble.py": { + "representation": "file-bytes", + "sha256": "abb60c35e448e0f94073f38a0352d11249aaf7bb8dbd7352414ae60a1d2b79c3" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/code/audit.py": { + "representation": "file-bytes", + "sha256": "d28062127a9b0d3866a3b79aad98a307233b20ebdb94cfb9f197d726b82ffea5" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/code/emit.py": { + "representation": "file-bytes", + "sha256": "98d77cefbc3a76f9f10bd7df3a2590ab88b411f6afe77b5f8d73f1602eb2bef3" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/code/local_audit.py": { + "representation": "file-bytes", + "sha256": "23eda3fe3d774e7f2dbf4dbdd4ff90d69ae7d1762ff95c8629cdc7667aa3fe71" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/data/hosting.json": { + "representation": "file-bytes", + "sha256": "765382d4fefd594e94c8c5826ec6300422ce9f79c816d7f7323ef85e99320f28" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/data/residual-isometries.json": { + "representation": "file-bytes", + "sha256": "750221cc66badd0ed0a74e7aad2d59f91f89c107370af21c6d929fbdd4a08a9f" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r715-whole-hosted/data/word.json.gz": { + "representation": "gzip-payload", + "sha256": "f3195c4c5cfe6faa44fbf885c20cfa310af544392c65ff13a4c6e12b8ff36dfc" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/bank_routes.py": { + "representation": "file-bytes", + "sha256": "7c6997c455bd55acca3a1603797c34e7733d557c27a7694a1429ff15773a505d" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/e8core.py": { + "representation": "file-bytes", + "sha256": "1cb286196c1530d06f50f0997febc5993b388f33464e295611b920ba30a24eeb" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/base_two_moment.py": { + "representation": "file-bytes", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py": { + "representation": "file-bytes", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/outer.py": { + "representation": "file-bytes", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/tile_m.py": { + "representation": "file-bytes", + "sha256": "d6ae4a556472d403773cd2117c992bfc10e1187112da1b3893f3fae628a131dd" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/data/residual-isometries.json": { + "representation": "file-bytes", + "sha256": "e12ed7ddd13cee101ba74a083b54665fd64d0b122b0bad5b83d817dcc8bae9d8" + }, + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/data/word.json.gz": { + "representation": "gzip-payload", + "sha256": "64d7d1e0c6ea7a3a8e91254c0dfd51b71637b49703ef4c1fce184fded5040bc9" + }, + "research/e8-bit-carrier-skeleton/code/hub/idle-axis-hosting/hosting_core.py": { + "representation": "file-bytes", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/emit.py": { + "representation": "file-bytes", + "sha256": "ac63ee481f3d75cb9f0658faaa2412db81d55bc44d9f1ff1c0329ce1e75aa0d4" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/geometry.py": { + "representation": "file-bytes", + "sha256": "9554182d67e434ea84b4430f909a2c400abc755d8487b51454a8e6968e62859d" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py": { + "representation": "file-bytes", + "sha256": "de4a9b9cd797e1a05da56f62cfe725c8728cea3a4aa031b7d1b0a68f869760d6" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/data/selection.json": { + "representation": "file-bytes", + "sha256": "52dbbb68e8c147690d15eaa1d952df05d074b0c121885a4159d9f6732f391872" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-rank149/code/emit.py": { + "representation": "file-bytes", + "sha256": "ac63ee481f3d75cb9f0658faaa2412db81d55bc44d9f1ff1c0329ce1e75aa0d4" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-rank149/data/residual-isometries.json": { + "representation": "file-bytes", + "sha256": "b23fda74a7979179e8fd83ee9870c1e232442cc90c05077adaabfe31d050d1e4" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-rank149/data/selection.json": { + "representation": "file-bytes", + "sha256": "4d9c2cf6a3d31a6faa287731e0721cb16601b0bc5c1a186b9645bfb5760ce8db" + }, + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-rank149/data/word.json.gz": { + "representation": "gzip-payload", + "sha256": "6b4f5e6affc3c0ec43218b3c11f6214e363bfe618fd1abbf897cbbbd3a78e2b3" + }, + "research/e8-bit-carrier-skeleton/code/nine/geometry.py": { + "representation": "file-bytes", + "sha256": "36eeda3184bd009e89462b65c8725d10860c444f8da8f1f87e5f6e50120011ca" + }, + "research/e8-bit-carrier-skeleton/code/pricing/base_two_moment.py": { + "representation": "file-bytes", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + "research/e8-bit-carrier-skeleton/code/pricing/moment.py": { + "representation": "file-bytes", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + "research/e8-bit-carrier-skeleton/code/pricing/outer.py": { + "representation": "file-bytes", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + "research/e8-bit-carrier-skeleton/code/pricing/prime_witnesses.py": { + "representation": "file-bytes", + "sha256": "98cd03bc9582e7bd0ab194c191ea8eea940539e510051443ab9fd3e572a364ab" + }, + "research/e8-bit-carrier-skeleton/code/provenance.py": { + "representation": "file-bytes", + "sha256": "e28fd87d0e34a6f6f6f1fddb6c4891deac220662c954de855d7aa5a7f9cceca4" + }, + "research/e8-bit-carrier-skeleton/code/skeleton/e8.py": { + "representation": "file-bytes", + "sha256": "721d859a6517d665ca84d03ef89668da3aae7433ffb0ee47faf37f2aeb85450e" + }, + "research/e8-bit-carrier-skeleton/code/skeleton/gen.py": { + "representation": "file-bytes", + "sha256": "7cdcf48078ed4beacd2e240aa8145e4aa6984558748d07659cb1b252786e073a" + }, + "research/e8-bit-carrier-skeleton/code/skeleton/geom.py": { + "representation": "file-bytes", + "sha256": "bb356568fa05e7bfd5fcd9012903611cf742729a99b4dc3a13685355b2678ae3" + }, + "research/e8-bit-carrier-skeleton/code/skeleton/wordkit.py": { + "representation": "file-bytes", + "sha256": "2b6c12d96f24a4e81f2c807827c2b74cf80037367fc8034e8c871dd5ce008351" + }, + "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz": { + "representation": "gzip-payload", + "sha256": "fbc56ed40d857b6ed74cbab1badd144fc276f08f76326dcb21a3ab2178a40c13" + }, + "research/e8-bit-carrier-skeleton/data/bit/bitE8mut-r489.json.gz": { + "representation": "gzip-payload", + "sha256": "88435b75b8d6e5c722eb2aa1449f3a5e8e9601a9ffe243839ce1ec932ab76547" + }, + "research/e8-bit-carrier-skeleton/data/complex-b.json": { + "representation": "file-bytes", + "sha256": "dce3f4b76aa3f6c3ba826ce556ffa61398b33e81e4d1a226dd2a36ce684fb02e" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr448/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "18b42250c3faf6f0df76fcab6c3a483582192ad7bb09cb1985f4b0bb91d67024" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr458/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "a4312cb0c53c2066a28b683a971a41e7d76c5f6d828a96481c3ae7b3c01bb2f3" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr471/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "188f9d1a7450496dbfd8d64381febd20b0597141537eb1a003435297df2d1720" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr473/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "70e515f0a5a2f9508cd030d35a99f90981a6eccc027c9ad5a3c77f5860310910" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr478/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "07bd05d14c71df8925b0b03510b2b337334b73ac425a94e03b2ec34ed2680164" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr483/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "799fa4ab2f785c478c3cdcb6c1c0428a5ce6e3ddbe4a4b2fd88630d811a593f6" + }, + "research/e8-bit-carrier-skeleton/data/complex/pr484/EXPECTED.json": { + "representation": "file-bytes", + "sha256": "0c93018a23bc573c7d155d4786e0c3978e95be0fda974076697939a1a1d8e5be" + }, + "research/e8-bit-carrier-skeleton/data/eleven/hosting.json": { + "representation": "file-bytes", + "sha256": "61f790657c465d16d3455f48f90f816797b9ea08bf02dbd0c90d2cf41836257e" + }, + "research/e8-bit-carrier-skeleton/data/eleven/residual-isometries.json": { + "representation": "file-bytes", + "sha256": "0fa5b353a0321af2ce4e2045db1d4c2d6418a11663894e2afcdb1eaa1984bddc" + }, + "research/e8-bit-carrier-skeleton/data/skeleton/d4part-pairs.json": { + "representation": "file-bytes", + "sha256": "d69ffe3326140bc541b8f1639e02db43a5835ab8ca02cc742b5bee2bf2ef1ba9" + }, + "research/e8-bit-carrier-skeleton/data/skeleton/plan-skB.json": { + "representation": "file-bytes", + "sha256": "f6162bb4d8092bc233700fa7ebc6a0d79f2893135aee18e998369044abb3f44b" + }, + "research/e8-bit-carrier-skeleton/discovery/README.md": { + "representation": "file-bytes", + "sha256": "b09aa45d5651720e10326cde559c863ba3ea45fe2fb6b4aaa3bfaa66a8fcf69f" + }, + "research/e8-bit-carrier-skeleton/discovery/d4part.py": { + "representation": "file-bytes", + "sha256": "a64927c340a4772ce0682b349e0c90c80d1a766000ccf397fb41b36a31929179" + }, + "research/e8-bit-carrier-skeleton/discovery/host_select.py": { + "representation": "file-bytes", + "sha256": "2aaaac18e083d289d4341e734c32571c89c51fefba04b388d407c7372b906dc7" + }, + "research/e8-bit-carrier-skeleton/discovery/plan.py": { + "representation": "file-bytes", + "sha256": "40e8dea1b4b71c5afd5993625f57bcac089dd2f72dfbc4dbc23ce917e5a61010" + }, + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": { + "representation": "file-bytes", + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + }, + "research/e8-bit-carrier-skeleton/requirements.txt": { + "representation": "file-bytes", + "sha256": "6023d480f929cdfa4e2f35e361eea003451cd6695af806935a32038b0115abb5" + }, + "research/e8-bit-carrier-skeleton/verify.sh": { + "representation": "file-bytes", + "sha256": "0f9248aa3611dfe2b5d59dbe992c6f7d21a0cc4f1de2b5ed05a6110191191224" + } + } +} diff --git a/research/r420-optimal-composed-pairs/VALIDATION.md b/research/r420-optimal-composed-pairs/VALIDATION.md new file mode 100644 index 0000000000..d4d68704c1 --- /dev/null +++ b/research/r420-optimal-composed-pairs/VALIDATION.md @@ -0,0 +1,117 @@ +# Validation record + +Run on 2026-10-13 from base +`66849e1475c930fd7732b1a0067ffee7e1e95f60`, on Linux x86-64 with CPython 3.12.14, +GCC 14.2.0 and Boost 1.85.0. Optional hosted dependencies were NumPy 2.3.5, +SciPy 1.17.0 and SymPy 1.14.0. No remote CI or independent human-review pass +is claimed. + +## Local and independent checks + +```sh +python3 -I -B research/r420-optimal-composed-pairs/verify.py +python3 -I -B research/r420-optimal-composed-pairs/independent_check.py +python3 -I -B -O research/r420-optimal-composed-pairs/verify.py +python3 -I -B -O research/r420-optimal-composed-pairs/independent_check.py +make selected-record-check +``` + +All passed. The primary checker verifies the 1,442 optimum using all 7,140 +unordered edges, validates all 660 inputs of both complete words in both +directions, checks every frame with the original E8 checker, and reproduces +the entire PR681 comparator receipt exactly. It rejects twelve mutations and +accepts one neutral endpoint only with its two ADDs charged. The separate +column-incidence checker covers all 50,400 matrix coefficients and 540 literal +Boolean D inputs, and rejects four certificate corruptions. Its implementation +imports neither the main checker nor a matching solver. + +The original H2 and direct K extractor remain false for the substituted D. +The canonical composed body with the original D passes H1-H5 and their +conclusions. Exact D-boundary equality justifies the substitution. The original +guards were not relaxed. + +## Fresh native and hosted replay + +```sh +BOOST_INCLUDE=/directory/containing/boost python3 -I -B research/r420-optimal-composed-pairs/verify.py --hosted --out /absolute/fresh/output +``` + +Passed for the actual reconstructed PR681 comparator and this replacement. +`NATIVE.json` and `HOSTED.json` retain all deterministic fields; only runtime +`seconds` fields are omitted. Full commands compare the generated receipts +with these files. + +- Fresh unchanged C++ legality checks accepted both physical words, including + all 660 register paths, nine COPY/ERASE lifecycles and rank mass 5,112 +- Five-, nine- and eleven-stage replays covered 900, 1,380 and 1,620 independent + formal columns per word, with all 96 bridge-omission controls rejected +- Removing one helper-return ADD is rejected by all three native checkers + with `local defining-decoder full formal column`, rather than by an unrelated + parser or precision failure +- Both parent auditors rejected all 17 controls; both hosted auditors rejected + all 16 controls +- All 120,960 helper invocations remain hosted whole with zero banks +- Emitted local-invocation events fall **6,144,768 -> 6,140,160**, exactly 288 + times the local saving of 16. This counts the expanded local streams only; + 69,120 bridge ADDs and schedule/hosting work are separately charged and + unchanged. It is not a complete-machine instruction counter +- Both fresh invoices retain **196 raw prefix bits charged at 256**, and + **432 two-level coefficient bits charged at 512** +- Both exact moment engines reproduce bit lower bound + `413456747036699736067/250000000000000000000000` + +The native body counts are 18,378 and 18,362. Their D costs are 11,562 and +11,546. Both positive prefix maxima are 253,149 and 4,334,338; the exact local +payload bound is 19505369118995241654063407203584, strictly below 2^104. +The selected baseline remains 26,916 ADDs. The cumulative 8,554 reduction from +that baseline includes predecessor work and is not attributed to this change. + +The primary checker additionally reconstructs PR733's exact pinned 57-pair +recipe on the **same PR681 body**. It gives 18,370 total ADDs and 11,554 D ADDs, +with the identical 253,149 / 4,334,338 prefix bounds and 104-bit local envelope. +Full scalar endpoints in both directions and frame paths pass. Thus **eight** +ADDs are new beyond the strongest prior matching on this body; **16** is the +reduction from PR681's published complete word. A separate third native/hosted +replay for the same-body comparator is not claimed. + +The PR484 calculation inside the inherited hosted driver is a historical +control. This run does not rebuild the selected complex supplier or assert +a new selected outer assembly. The selected record/source-inventory check +passes without modifying its source files. + +## Portability and rejection checks + +A minimal tree containing only this package and the 143 pinned inherited files +was copied to a path containing spaces. From an unrelated working directory, +normal/optimized primary checks and the independent checker passed. + +`PACKAGE-TESTS.json` records these nine process-level checks: + +1. Relocated normal primary replay passes +2. Relocated optimized primary replay passes +3. Relocated independent replay passes +4. Recompressing the original word with a different gzip level/header passes +5. Altering its decompressed payload fails the source binding +6. Altering the claimed saved-ADD count fails exact receipt comparison +7. Altering a matching score fails its recomputed oriented price +8. An existing output directory is refused and its sentinel is preserved +9. Removing the pinned input fails instead of reporting success + +Python compilation and staged whitespace checks pass. Generated bytecode is +excluded from the patch. Only the new research package is changed; selected +artifacts and `upstream/` are untouched. + +## Live comparison and scope + +The initial scan inspected 598 open PRs through #779. A refresh through #799 +confirmed that PR681 and PR733 still have the pinned heads; `main` remains at +the exact base. PR794's 19,037-ADD target-basis word retains a smaller 192-bit +hosted charge and is explicitly compared in the README. PR789/790 alter +different B blocks; PR799 uses different suppliers. No duplicate certificate +for this fixed PR694-basis disjoint target-pair optimum was found. + +The independent review before publication is separate from the author's +checks above. Finite certificate success is not a formal multiplication +theorem. Repository-wide `make verify`, selected-frontier cold replay, Lean, +remote CI and all inherited uniform/compiler/physical/tape/analytic obligations +are outside the claimed validation. diff --git a/research/r420-optimal-composed-pairs/hosted.py b/research/r420-optimal-composed-pairs/hosted.py new file mode 100644 index 0000000000..79982c7bbe --- /dev/null +++ b/research/r420-optimal-composed-pairs/hosted.py @@ -0,0 +1,90 @@ +"""Replay the frozen nine-stage owner plan for both words, then compare invoices. + +Adapted from Ali Romman / PR688 by Alluri with substantial OpenAI Codex assistance. +Apache-2.0. All inherited emitters, owner auditors and invoice engines are unchanged. +Uses the unchanged PR543 / PR510 / PR463 / PR442 verification chain. +""" +import json +import shutil +import subprocess +import sys + + +def run(root, out): + package = root / "research/e8-bit-r420" + predecessor = root / "research/e8-bit-carrier-skeleton" + price = package / "vendor/pr510/e8-r480-nine-stage" + code = price / "vendor/e8-r715-eleven-stage-whole/code" + python = [sys.executable, "-B"] + results = {} + saving = json.loads((out / "LOCAL.json").read_text())["saved_additions"] + + def call(name, command): + print("RUN", name, flush=True) + with (out / (name + ".log")).open("w") as log: + subprocess.run(list(map(str, command)), check=True, stdout=log, stderr=subprocess.STDOUT) + + geometry = out / "geometry" + call("geometry", python + [predecessor / "code/nine/geometry.py", "--source", predecessor, "--out", geometry]) + # Geometry's only runtime field is excluded before it is hashed into the + # generated template. Preserve every proof-relevant field and rebind hashes. + gp = geometry / "GEOMETRY.json" + geometry_data = json.loads(gp.read_text()) + geometry_data.pop("seconds") + gp.write_text(json.dumps(geometry_data, sort_keys=True, indent=2) + "\n") + call("parent-audit-adapter", python + [price / "code/adapt.py", code, out / "adapted"]) + for name in ("baseline", "replacement"): + base = out / name + parent = base / "nine" + parent.mkdir() + shutil.copy2(geometry / "GEOMETRY.json", parent / "GEOMETRY.json") + word = out / (name + ".json.gz") + call(name + "-parent", python + [code / "global_k.py", "--word", word, + "--local-check", base, "--out", parent, "--isometries", predecessor / "data/eleven/residual-isometries.json"]) + call(name + "-parent-audit", python + [out / "adapted/audit_parent_k.py", + "--word", word, "--local-check", base, "--out", parent]) + hosted = base / "hosted" + call(name + "-hosted", python + [code / "emit_k.py", parent, base, hosted, + "--selection", package / "data/selection9-r420.json", "--key", "bit"]) + call(name + "-hosted-audit", python + [code / "audit_hosted_k.py", base, hosted, hosted / "AUDIT.json"]) + + # The unchanged pr484 price is a historical arithmetic control only. + # No complex construction is replayed or selected by this command. + call(name + "-invoice", python + [price / "code/assemble9.py", base, hosted, + hosted / "AUDIT.json", predecessor, base / "PRICE.json", "pr484"]) + pg = json.loads((parent / "GLOBAL.json").read_text()) + parent_audit = json.loads((parent / "AUDIT.json").read_text()) + audit = json.loads((hosted / "AUDIT.json").read_text()) + invoice = json.loads((base / "PRICE.json").read_text()) + if (parent_audit["status"] != "PASS_INDEPENDENT_COMPRESSED_BIT_TEMPLATE_AUDIT" + or audit["status"] != "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT" + or invoice["status"] != "PASS_NINE_STAGE_WHOLE_HOSTED_BIT_PRICE_AND_CITED_ASSEMBLY"): + raise ValueError("Hosted verification did not pass") + if audit["hosted_residuals"] != 120960 or audit["bank_assignments"] != 0: + raise ValueError("Whole-owner inventory changed") + if len(parent_audit["mutations_rejected"]) != 17 or len(audit["mutations_rejected"]) != 16: + raise ValueError("Incomplete inherited mutation coverage") + results[name] = {"parent_mutations": parent_audit["mutations_rejected"], "hosted_audit": audit, + "bit_lower": invoice["bit_lower"], "bit_lower_decimal": invoice["bit_lower_decimal"], + "invoice": invoice["bit"], "global_prefix_bound": pg["global_prefix_bound"], + "bit_profile": invoice["bit_profile"], "local_additions": pg["local_additions"]} + old, new = results["baseline"], results["replacement"] + if old["bit_profile"] != new["bit_profile"] or old["bit_lower"] != new["bit_lower"]: + raise ValueError("The recursive profile or bit exponent changed") + if new["bit_lower_decimal"] != "0.001653826988146798944268": + raise ValueError("The original R420 bit price was not reproduced") + if old["hosted_audit"]["emitted_events"] - new["hosted_audit"]["emitted_events"] != 288 * saving: + raise ValueError("Wrong physical instruction saving") + # Reprice the changed positive envelope. A larger raw prefix is not inherited + # for free: assemble9 recomputes both rounded charges from the actual word. + changing = {"prefix_bits", "charged_prefix_bits", "coefficient_bits", "two_level_coefficient_bits"} + if ({k: v for k, v in old["invoice"].items() if k not in changing} + != {k: v for k, v in new["invoice"].items() if k not in changing}): + raise ValueError("A non-prefix finite invoice field changed") + for result in results.values(): + invoice = result["invoice"] + if (invoice["prefix_bits"] != int(result["global_prefix_bound"]).bit_length() + or invoice["charged_prefix_bits"] < invoice["prefix_bits"] + or invoice["charged_two_level_coefficient_bits"] < invoice["two_level_coefficient_bits"]): + raise ValueError("Insufficient fresh precision invoice") + return results diff --git a/research/r420-optimal-composed-pairs/independent_check.py b/research/r420-optimal-composed-pairs/independent_check.py new file mode 100644 index 0000000000..0b0b4ce391 --- /dev/null +++ b/research/r420-optimal-composed-pairs/independent_check.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python3 +"""Column-incidence proof check, independent of verify.py and matching solvers. + +Sagar Thakrar, substantial OpenAI Codex assistance. Apache-2.0. +This checks the frozen matching class, not geometry or hosted execution. +""" +import copy +import gzip +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(value, message): + if not value: + raise ValueError(message) + + +def check(certificate, helper_recipe, word): + # Each integer holds a helper column's 120 target coefficients. + cols = [0]*420 + for frame, destination, sources in word['D']: + require(frame == 0 and 120 <= destination < 240, 'input D') + for source in sources: + cols[source-240] ^= 1 << (destination-120) + original = cols[:] + used = set() + for pair in helper_recipe['pairs']: + a, b = pair['dst']-240, pair['src']-240 + require(a != b and 0 <= a < 420 and 0 <= b < 420 and not ({a, b} & used), 'helper domain') + cols[b] ^= cols[a] + used.update((a, b)) + counts = [0]*120 + common = [[0]*120 for _ in range(120)] + for column in cols: + support = [t for t in range(120) if column & (1 << t)] + for a in support: + counts[a] += 1 + for b in support: + common[a][b] += 1 + q = certificate['doubled_vertex_prices'] + require(len(q) == 120 and all(type(x) is int and x >= 0 for x in q), 'dual domain') + for a, b in itertools.combinations(range(120), 2): + # This incidence formula avoids row-set symmetric differences. + weight = max(0, 2*common[a][b]-counts[a]-2, 2*common[a][b]-counts[b]-2) + require(q[a]+q[b] >= 2*weight, 'edge inequality') + used, saving = set(), 0 + transformed = cols[:] + pairs = certificate['pairs'] + for source, destination, claimed in pairs: + a, b = source-120, destination-120 + require(0 <= a < 120 and 0 <= b < 120 and a != b and not ({a, b} & used), 'target domain') + actual = 2*common[a][b]-counts[a]-2 + require(actual == claimed and actual > 0, 'oriented saving') + used.update((a, b)); saving += actual + for i, column in enumerate(transformed): + if column & (1 << a): + transformed[i] ^= 1 << b + require(sum(q) == 2*saving == 2884 and certificate['gain'] == saving, 'tight objective') + # Direct literal Boolean inputs cover all 120 dirty targets and 420 helpers. + for input_column in range(540): + targets = [int(input_column == t) for t in range(120)] + helpers = [int(input_column == 120+h) for h in range(420)] + for pair in helper_recipe['pairs']: + helpers[pair['dst']-240] ^= helpers[pair['src']-240] + for a, b, _ in pairs: + targets[b-120] ^= targets[a-120] + for h, column in enumerate(transformed): + if helpers[h]: + for t in range(120): + targets[t] ^= (column >> t) & 1 + for a, b, _ in reversed(pairs): + targets[b-120] ^= targets[a-120] + for pair in reversed(helper_recipe['pairs']): + helpers[pair['dst']-240] ^= helpers[pair['src']-240] + for t in range(120): + expected = int(input_column == t) + if input_column >= 120: + expected ^= (original[input_column-120] >> t) & 1 + require(targets[t] == expected, 'target column') + require(helpers == [int(input_column == 120+h) for h in range(420)], 'helper return') + reads = sum(column.bit_count() for column in transformed) + require(2*201 + 2*len(pairs) + reads == 11546, 'complete D cost') + return saving + + +def main(): + manifest = json.loads((HERE/'SOURCES.json').read_text()) + raw = (ROOT/'research/e8-bit-r420/data/bitE8mut-r420.json.gz').read_bytes() + payload = gzip.decompress(raw) + pin = manifest['base_files']['research/e8-bit-r420/data/bitE8mut-r420.json.gz'] + require(hashlib.sha256(payload).hexdigest() == pin['sha256'], 'original word pin') + helper_bytes = (HERE/'vendor/pr694-recipe.json').read_bytes() + require(hashlib.sha256(helper_bytes).hexdigest() == + manifest['imported']['vendor/pr694-recipe.json']['sha256'], 'helper recipe pin') + word, helpers = json.loads(payload), json.loads(helper_bytes) + cert = json.loads((HERE/'OPTIMUM.json').read_text()) + check(cert, helpers, word) + controls = [] + mutants = [copy.deepcopy(cert) for _ in range(4)] + mutants[0]['doubled_vertex_prices'] = [0]*120 + mutants[1]['doubled_vertex_prices'][11] += 1 + mutants[2]['pairs'].append(mutants[2]['pairs'][0]) + mutants[3]['pairs'][0][2] += 1 + for i, mutant in enumerate(mutants): + try: + check(mutant, helpers, word) + except ValueError: + controls.append(i) + else: + raise ValueError('certificate mutation accepted') + print('PASS_R420_COLUMN_MATCHING optimum=1442 coefficients=50400 edges=7140 ' + 'boolean_columns=540 D_ADDs=11546 controls=4') + + +if __name__ == '__main__': + main() diff --git a/research/r420-optimal-composed-pairs/native.py b/research/r420-optimal-composed-pairs/native.py new file mode 100644 index 0000000000..e529444ac7 --- /dev/null +++ b/research/r420-optimal-composed-pairs/native.py @@ -0,0 +1,79 @@ +"""Compare the original and replacement words with the pinned cohort checkers. + +Adapted from Ali Romman / PR688 by Alluri with substantial OpenAI Codex assistance. +Apache-2.0. The underlying C++ checkers are unchanged. +""" +import json +import os +import shlex +import subprocess +import sys + + +def run(root, out): + package = root / "research/e8-bit-carrier-skeleton" + bit = package / "code/bit" + checkers = bit / "checkers" + python = [sys.executable, "-B"] + compiler = shlex.split(os.environ.get("CXX", "c++")) + include = os.environ.get("BOOST_INCLUDE", "/usr/include") + flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=120", "-DRHELP=420", + "-I" + str(package / "portable-include"), "-I" + str(checkers), "-I" + include] + bindir = out / "bin" + bindir.mkdir() + + def call(name, command): + with (out / (name + ".log")).open("w") as log: + subprocess.run(list(map(str, command)), check=True, stdout=log, stderr=subprocess.STDOUT) + + call("compile-legality", compiler + flags + ["-o", bindir / "legality", checkers / "legality_h.cpp"]) + for pairs in (2, 4, 5): + call("compile-columns" + str(pairs), compiler + flags + ["-DKPAIRS=" + str(pairs), "-o", + bindir / ("columns" + str(pairs)), checkers / "columns_k.cpp"]) + results = {} + local = json.loads((out / "LOCAL.json").read_text()) + saving = local["saved_additions"] + for name in ("baseline", "replacement"): + base = out / name + records, cin, cout = (base / item for item in ("records", "cin", "cout")) + call(name + "-export", python + [bit / "export_records.py", out / (name + ".json.gz"), records]) + call(name + "-cohort", python + [bit / "regression/stage_cohort.py", records, records, cin, cout]) + call(name + "-legality", [bindir / "legality", cin, cout, cout / "legality.json"]) + legality = json.loads((cout / "legality.json").read_text()) + if legality["status"] != "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE": + raise ValueError("Legality did not pass") + results[name] = {"legality": legality, "stages": {}} + for pairs in (2, 4, 5): + receipt = cout / ("columns.json" if pairs == 2 else "columns" + str(pairs) + ".json") + call(name + "-columns" + str(pairs), [bindir / ("columns" + str(pairs)), + cout / "COHORT249-RECORDS.bin", receipt]) + data = json.loads(receipt.read_text()) + expected_status = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if pairs == 2 + else "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + if data["status"] != expected_status: + raise ValueError("Formal columns did not pass") + expected = 6 * (pairs - 1) + if (len(data["negative_controls"]) != expected + or not all(c["rejected"] for c in data["negative_controls"])): + raise ValueError("A bridge control failed") + if data["formal_columns_checked"] != 240 * pairs + 420: + raise ValueError("Wrong formal column count") + results[name]["stages"][str(2 * pairs + 1)] = { + "bridge_controls_rejected": expected, + "receipt": { + key: data[key] for key in ("formal_columns_checked", "local_scalar_additions", "local_raw_H", + "payload_prefix_bits", "payload_prefix_upper", "signed_lift_prefix")}} + for stages in ("5", "9", "11"): + old, new = (results[name]["stages"][stages]["receipt"] for name in ("baseline", "replacement")) + if old["local_raw_H"] != new["local_raw_H"] or old["local_scalar_additions"] - new["local_scalar_additions"] != saving: + raise ValueError("Paid profile or XOR saving differs") + for name, receipt in (("baseline", old), ("replacement", new)): + expected = local[name] + if (int(receipt["payload_prefix_upper"]) != int(expected["payload_prefix_upper"]) + or receipt["payload_prefix_bits"] != expected["payload_prefix_bits"] + or int(receipt["payload_prefix_upper"]) >= 2**104): + raise ValueError("Independent native precision bill differs or exceeds the retained cap") + actual = [int(x["cancellation_free_signed_row_l1_upper"]) for x in receipt["signed_lift_prefix"]] + if actual != [expected["forward_prefix"], expected["reverse_prefix"]]: + raise ValueError("Independent signed prefix bounds differ") + return results diff --git a/research/r420-optimal-composed-pairs/vendor/pr670-block.json b/research/r420-optimal-composed-pairs/vendor/pr670-block.json new file mode 100644 index 0000000000..325c18cd44 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr670-block.json @@ -0,0 +1,199 @@ +{ + "schema": "r420-block3-xor-candidate/1", + "source_path": "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "source_sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "block_index": 3, + "b_start": 263, + "b_stop": 313, + "frame": 545, + "registers": [21, 29, 37, 45, 53, 62, 71, 73, 81, 89, 97, 105], + "seed": 13, + "method": "commuting transvections plus exact 3-to-at-most-2 lookup", + "domain": "12 original registers; same ordered 12x12 F2 endpoint; no helpers or relabelling", + "coverage": { + "trials": 50, + "shuffle_steps_per_trial": 400, + "attempted_shuffle_steps": 20000, + "accepted_reductions": 170, + "stopping_rule": "fixed trials times steps; no claim of exhaustive optimality" + }, + "original_gate_count": 50, + "replacement_gate_count": 33, + "original_local_ops": [ + [3, 1], + [3, 11], + [3, 2], + [3, 9], + [3, 8], + [3, 10], + [7, 6], + [7, 0], + [7, 4], + [7, 2], + [7, 9], + [7, 5], + [6, 0], + [6, 4], + [6, 5], + [1, 2], + [1, 9], + [1, 10], + [11, 0], + [11, 9], + [0, 4], + [0, 9], + [0, 5], + [2, 8], + [2, 5], + [9, 8], + [8, 10], + [10, 3], + [10, 7], + [10, 1], + [5, 3], + [5, 6], + [8, 3], + [8, 7], + [8, 0], + [8, 4], + [8, 2], + [9, 3], + [9, 7], + [2, 3], + [2, 7], + [4, 3], + [4, 6], + [0, 3], + [11, 3], + [11, 7], + [1, 3], + [1, 7], + [6, 3], + [7, 3] + ], + "replacement_local_ops": [ + [3, 11], + [1, 2], + [11, 0], + [0, 5], + [0, 4], + [6, 0], + [7, 2], + [2, 5], + [2, 8], + [0, 9], + [7, 6], + [11, 7], + [1, 10], + [1, 9], + [3, 1], + [7, 9], + [9, 3], + [2, 7], + [3, 8], + [11, 3], + [8, 2], + [8, 4], + [8, 10], + [6, 3], + [4, 6], + [5, 6], + [9, 7], + [7, 3], + [1, 7], + [10, 1], + [0, 3], + [2, 3], + [8, 0] + ], + "endpoint_rows": [3391, 3069, 3295, 3854, 3951, 3935, 3967, 3579, 3070, 3835, 4093, 2042], + "nonnegative_forward_componentwise_no_worse": true, + "nonnegative_reverse_componentwise_no_worse": true, + "improvements": [ + { + "trial": 0, + "step": 26, + "gates": 49 + }, + { + "trial": 0, + "step": 40, + "gates": 48 + }, + { + "trial": 0, + "step": 50, + "gates": 47 + }, + { + "trial": 0, + "step": 85, + "gates": 46 + }, + { + "trial": 0, + "step": 89, + "gates": 45 + }, + { + "trial": 0, + "step": 159, + "gates": 44 + }, + { + "trial": 0, + "step": 174, + "gates": 43 + }, + { + "trial": 0, + "step": 212, + "gates": 42 + }, + { + "trial": 0, + "step": 218, + "gates": 41 + }, + { + "trial": 0, + "step": 227, + "gates": 40 + }, + { + "trial": 0, + "step": 237, + "gates": 39 + }, + { + "trial": 1, + "step": 62, + "gates": 38 + }, + { + "trial": 1, + "step": 68, + "gates": 37 + }, + { + "trial": 1, + "step": 121, + "gates": 36 + }, + { + "trial": 1, + "step": 220, + "gates": 35 + }, + { + "trial": 1, + "step": 256, + "gates": 34 + }, + { + "trial": 2, + "step": 364, + "gates": 33 + } + ] +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr674-block.json b/research/r420-optimal-composed-pairs/vendor/pr674-block.json new file mode 100644 index 0000000000..cc16574133 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr674-block.json @@ -0,0 +1,865 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "baseline_local_roundtrip_peak": 1075, + "baseline_reverse_majorant": [ + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 7, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 1, + 3, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3, + 1, + 1, + 5, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 5, + 2, + 1, + 9, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 3, + 0, + 0, + 7, + 2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 4, + 1, + 9, + 0, + 0, + 23, + 7 + ], + [ + 0, + 0, + 0, + 0, + 1, + 2, + 1, + 5, + 0, + 0, + 13, + 4 + ], + [ + 0, + 0, + 0, + 0, + 4, + 7, + 2, + 18, + 0, + 0, + 44, + 13 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 5, + 2, + 1, + 9, + 1 + ], + [ + 0, + 0, + 2, + 1, + 0, + 0, + 0, + 10, + 3, + 3, + 18, + 1 + ], + [ + 1, + 2, + 5, + 2, + 0, + 0, + 0, + 29, + 8, + 8, + 52, + 3 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 2, + 1 + ] + ], + "candidate_canonical_sha256": "aef2fc8c510b87b4da62d5756c2be3d16da1c2557bfd8358e01ee25d02ffbc99", + "candidate_local_roundtrip_peak": 485, + "candidate_reverse_majorant": [ + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 3, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 1, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3, + 1, + 1, + 1, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 5, + 2, + 1, + 1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 3, + 0, + 0, + 3, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 1, + 3, + 0, + 0, + 3, + 3 + ], + [ + 0, + 0, + 0, + 0, + 1, + 2, + 1, + 5, + 0, + 0, + 5, + 4 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 2, + 0, + 0, + 2, + 1 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 5, + 2, + 1, + 3, + 1 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 4, + 1, + 1, + 2, + 1 + ], + [ + 1, + 2, + 1, + 2, + 0, + 0, + 0, + 17, + 4, + 4, + 10, + 3 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 2, + 1 + ] + ], + "cost": { + "baseline": { + "adds_by_phase": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1077, + "5": 2973 + }, + "five_stage_payload_bits": 100, + "five_stage_payload_bound": "998206739997057013039187410944", + "forward": { + "all_columns": 660, + "bits": 18, + "cancellation_free_row_l1": 144651, + "maximum_at": { + "destination": 528, + "phase": 5, + "record_in_direction": 29536 + } + }, + "negative_controls": { + "broken_COPY_source": "ERASE source frame or workspace mismatch", + "missing_ERASE": "copy workspace already open", + "modified_MOVE_rank": "MOVE rank mismatch", + "omitted_B_source_ADD": "scalar endpoint mismatch" + }, + "nine_stage_charged_prefix_bits": 192, + "nine_stage_prefix_bits": 189, + "nine_stage_prefix_bound": "440858815560454746902811617646181283465263876766227759104", + "operations": { + "0": 2940, + "1": 26916, + "2": 9, + "3": 9 + }, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "paid_rank_mass": 5112, + "records": 29874, + "reverse": { + "all_columns": 660, + "bits": 22, + "cancellation_free_row_l1": 2270064, + "maximum_at": { + "destination": 141, + "phase": 1, + "record_in_direction": 26356 + } + } + }, + "candidate": { + "adds_by_phase": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1065, + "5": 2961 + }, + "five_stage_payload_bits": 100, + "five_stage_payload_bound": "962930826045767086638403792896", + "forward": { + "all_columns": 660, + "bits": 18, + "cancellation_free_row_l1": 144651, + "maximum_at": { + "destination": 528, + "phase": 5, + "record_in_direction": 29512 + } + }, + "negative_controls": { + "broken_COPY_source": "ERASE source frame or workspace mismatch", + "missing_ERASE": "copy workspace already open", + "modified_MOVE_rank": "MOVE rank mismatch", + "omitted_B_source_ADD": "scalar endpoint mismatch" + }, + "nine_stage_charged_prefix_bits": 192, + "nine_stage_prefix_bits": 189, + "nine_stage_prefix_bound": "410250116818741208821899034315310017378193525612293914624", + "operations": { + "0": 2940, + "1": 26892, + "2": 9, + "3": 9 + }, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "paid_rank_mass": 5112, + "records": 29850, + "reverse": { + "all_columns": 660, + "bits": 22, + "cancellation_free_row_l1": 2229592, + "maximum_at": { + "destination": 141, + "phase": 1, + "record_in_direction": 26332 + } + } + }, + "formula_and_exporter_sources": { + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + "same_frame_paths": true, + "status": "PASS_LOCAL_SCALAR_PROFILE_AND_PREFIX_AUDIT" + }, + "full_word_checks": { + "H1_H5_and_conclusion": true, + "closed_frames": 672, + "columns": 660 + }, + "integer_forward_matrix": [ + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 0, + 0, + 3, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 2 + ], + [ + 1, + 1, + 3, + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 3, + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 2, + 1, + 2, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "negative_controls": [ + "omit block gate", + "change block source", + "parity-preserving duplicated pair", + "omit cleanup gate", + "block gate at zero frame", + "stale cleanup violates literal-reverse interface" + ], + "registers": [ + 19, + 24, + 35, + 40, + 54, + 56, + 65, + 74, + 84, + 95, + 100, + 111 + ], + "replacement_ops": [ + [ + 40, + 35 + ], + [ + 100, + 95 + ], + [ + 100, + 19 + ], + [ + 100, + 84 + ], + [ + 100, + 40 + ], + [ + 100, + 24 + ], + [ + 65, + 54 + ], + [ + 56, + 65 + ], + [ + 74, + 56 + ], + [ + 95, + 40 + ], + [ + 95, + 111 + ], + [ + 19, + 111 + ], + [ + 19, + 24 + ], + [ + 84, + 111 + ], + [ + 84, + 35 + ], + [ + 35, + 74 + ], + [ + 35, + 95 + ], + [ + 35, + 84 + ], + [ + 111, + 100 + ], + [ + 54, + 74 + ], + [ + 54, + 111 + ], + [ + 54, + 56 + ], + [ + 65, + 111 + ], + [ + 65, + 56 + ], + [ + 24, + 74 + ], + [ + 24, + 95 + ], + [ + 56, + 111 + ], + [ + 111, + 74 + ], + [ + 74, + 100 + ], + [ + 40, + 74 + ], + [ + 40, + 84 + ], + [ + 84, + 74 + ], + [ + 19, + 74 + ], + [ + 95, + 74 + ] + ], + "scope": "Finite block and native-word improvement; no new kappa, full hosting replay or full theorem proof", + "source_B_slice": [ + 371, + 417 + ], + "source_offsets": [ + 16, + 0, + 1, + 2, + 3, + 4, + 19, + 17, + 6, + 9, + 10, + 12, + 13, + 14, + 15, + 20, + 21, + 22, + 34, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 33, + 35, + 45, + 37, + 38, + 40, + 42, + 44 + ], + "status": "PASS_R420_BLOCK5_RESYNTHESIS", + "steps": [ + { + "gates": 43, + "roundtrip_unit_peak": 1075 + }, + { + "gates": 39, + "roundtrip_unit_peak": 809 + }, + { + "gates": 37, + "roundtrip_unit_peak": 809 + }, + { + "gates": 36, + "roundtrip_unit_peak": 809 + }, + { + "gates": 34, + "roundtrip_unit_peak": 485 + } + ], + "strict_reverse_entries": 28 +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr681-decoders.json b/research/r420-optimal-composed-pairs/vendor/pr681-decoders.json new file mode 100644 index 0000000000..ad6bfff6c5 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr681-decoders.json @@ -0,0 +1,354 @@ +{ + "source_pairs": [ + [ + 377, + 366 + ], + [ + 356, + 339 + ], + [ + 415, + 506 + ], + [ + 511, + 532 + ], + [ + 497, + 326 + ], + [ + 540, + 534 + ], + [ + 531, + 530 + ], + [ + 434, + 514 + ], + [ + 559, + 438 + ], + [ + 529, + 431 + ], + [ + 498, + 547 + ], + [ + 402, + 551 + ], + [ + 502, + 398 + ], + [ + 575, + 488 + ], + [ + 309, + 347 + ], + [ + 516, + 507 + ], + [ + 515, + 489 + ], + [ + 382, + 343 + ], + [ + 327, + 395 + ], + [ + 283, + 373 + ], + [ + 439, + 404 + ], + [ + 473, + 260 + ], + [ + 374, + 492 + ], + [ + 328, + 505 + ], + [ + 435, + 379 + ], + [ + 297, + 444 + ], + [ + 482, + 305 + ] + ], + "selected_indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 21, + 22, + 23, + 26 + ], + "pairs": [ + [ + 377, + 366 + ], + [ + 356, + 339 + ], + [ + 415, + 506 + ], + [ + 511, + 532 + ], + [ + 497, + 326 + ], + [ + 540, + 534 + ], + [ + 531, + 530 + ], + [ + 434, + 514 + ], + [ + 559, + 438 + ], + [ + 529, + 431 + ], + [ + 498, + 547 + ], + [ + 402, + 551 + ], + [ + 502, + 398 + ], + [ + 575, + 488 + ], + [ + 309, + 347 + ], + [ + 516, + 507 + ], + [ + 515, + 489 + ], + [ + 382, + 343 + ], + [ + 327, + 395 + ], + [ + 473, + 260 + ], + [ + 374, + 492 + ], + [ + 328, + 505 + ], + [ + 482, + 305 + ] + ], + "selection": "greedy add one remaining source pair minimizing total additions then payload, subject to strict payload < 2^104; stop when none fits", + "variants_tested": 372, + "history": [ + { + "accepted_index": 1, + "additions": 18476, + "payload_bits": 103 + }, + { + "accepted_index": 3, + "additions": 18468, + "payload_bits": 103 + }, + { + "accepted_index": 0, + "additions": 18460, + "payload_bits": 103 + }, + { + "accepted_index": 2, + "additions": 18452, + "payload_bits": 103 + }, + { + "accepted_index": 5, + "additions": 18446, + "payload_bits": 103 + }, + { + "accepted_index": 4, + "additions": 18440, + "payload_bits": 103 + }, + { + "accepted_index": 7, + "additions": 18434, + "payload_bits": 103 + }, + { + "accepted_index": 6, + "additions": 18428, + "payload_bits": 104 + }, + { + "accepted_index": 17, + "additions": 18424, + "payload_bits": 104 + }, + { + "accepted_index": 14, + "additions": 18420, + "payload_bits": 104 + }, + { + "accepted_index": 16, + "additions": 18416, + "payload_bits": 104 + }, + { + "accepted_index": 12, + "additions": 18412, + "payload_bits": 104 + }, + { + "accepted_index": 10, + "additions": 18408, + "payload_bits": 104 + }, + { + "accepted_index": 15, + "additions": 18404, + "payload_bits": 104 + }, + { + "accepted_index": 13, + "additions": 18400, + "payload_bits": 104 + }, + { + "accepted_index": 11, + "additions": 18396, + "payload_bits": 104 + }, + { + "accepted_index": 9, + "additions": 18392, + "payload_bits": 104 + }, + { + "accepted_index": 8, + "additions": 18388, + "payload_bits": 104 + }, + { + "accepted_index": 26, + "additions": 18386, + "payload_bits": 104 + }, + { + "accepted_index": 21, + "additions": 18384, + "payload_bits": 104 + }, + { + "accepted_index": 18, + "additions": 18382, + "payload_bits": 104 + }, + { + "accepted_index": 22, + "additions": 18380, + "payload_bits": 104 + }, + { + "accepted_index": 23, + "additions": 18378, + "payload_bits": 104 + } + ], + "initial_all_pairs_bits": 105, + "initial_all_pairs_additions": 18370, + "leave_one_out_variants": 27, + "leave_one_out_valid": 0 +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr681-expected.json b/research/r420-optimal-composed-pairs/vendor/pr681-expected.json new file mode 100644 index 0000000000..f2b4e8bd55 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr681-expected.json @@ -0,0 +1,438 @@ +{ + "status": "PASS_SUPPLIER_CIRCUIT_CONSOLIDATION", + "bit": { + "status": "PASS_CONSOLIDATED_BIT_CIRCUIT", + "baseline": { + "semantic_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "scalar_stream_sha256": "95be862aadd3cd5dc9a8ba76e1ede1cc367d51f26fc24af3f56795b4807ba6f0", + "binary_additions": 26916, + "D_binary_additions": 19922, + "D_grouped_gates": 120, + "forward_and_reverse": [ + { + "copies": 9, + "columns": 660 + }, + { + "copies": 9, + "columns": 660 + } + ], + "forward_prefix": 144651, + "reverse_prefix": 2270064, + "payload_prefix_upper": "998206739997057013039187410944", + "payload_prefix_bits": 100, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "exported_records": 29874, + "record_sha256": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f" + }, + "replacement": { + "semantic_word_sha256": "983aec23d244575ae6205c53ed8ccae2f4a2aa8171463eef71d64c6bfceafe40", + "scalar_stream_sha256": "6494f36ba4ce06ae142ab0f81c2178d91c6a1c0c812a57f40958e48635b1853c", + "binary_additions": 18378, + "D_binary_additions": 11562, + "D_grouped_gates": 634, + "forward_and_reverse": [ + { + "copies": 9, + "columns": 660 + }, + { + "copies": 9, + "columns": 660 + } + ], + "forward_prefix": 253149, + "reverse_prefix": 4334338, + "payload_prefix_upper": "19505369118995241654063407203584", + "payload_prefix_bits": 104, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "exported_records": 21336, + "record_sha256": "df920f588352d4d1d165d034655480c55f2182ae7fe4cee620d1a2c395c05b6b" + }, + "stages": [ + { + "stage": "selected R420", + "additions": 26916 + }, + { + "stage": "PR694 helper basis", + "additions": 19982 + }, + { + "stage": "PR713 target method on transformed rows", + "additions": 18556 + }, + { + "stage": "PR691 quad", + "additions": 18542 + }, + { + "stage": "PR670/674 via PR688 blocks", + "additions": 18484 + }, + { + "stage": "PR708 compatible 23/27 pairs", + "additions": 18378 + } + ], + "saved_additions": 8538, + "D_columns": 660, + "canonical_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 + }, + "canonical_conclusions": { + "U_block_form": true, + "J_identity": true, + "K_equals_D": true, + "C_is_U_inverse": true + }, + "actual_full_word": { + "columns": 660, + "gates": { + "D": 634, + "A": 2103, + "B": 808, + "C": 2671 + }, + "scatter_terms": 568 + }, + "labels": { + "labels": 120, + "lattice_rank": 8, + "gram_det": 1, + "frames": 672 + }, + "controls": [ + "missing_helper_preparation", + "missing_helper_restoration", + "missing_target_preparation", + "wrong_middle_read", + "nonzero_D_frame", + "stale_cleanup", + "wrong_A_with_rebuilt_cleanup", + "wrong_B_with_rebuilt_cleanup", + "all_27_decoder_pairs_exceed_precision" + ], + "semantic_D_contract": true, + "literal_H2_claimed": false, + "compatibility_candidates": 400, + "retained_decoder_pairs": 23 + }, + "complex": { + "selected_programs": { + "status": "PASS_COMPLEX_DYADIC_LOWERING", + "programs": { + "ck/forward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 21936, + "additions": 21443, + "unit_additions": 6217, + "baseline_real_primitives": 224938, + "new_real_primitives": 169618, + "saved_real_primitives": 55320, + "primitive_tags": { + "add": 23838, + "clear": 42918, + "copy": 30468, + "double": 11170, + "halve": 38998, + "negate": 696, + "subtract": 21530 + }, + "primitive_word_sha256": "16ae874e3352c4df265026f62db95359a30399f1edc4c1b151d564d71902380c", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "retained_prefix_l1_upper": "920709848294", + "charged_payload_bits": 192 + }, + "ck/backward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 21936, + "additions": 21451, + "unit_additions": 6225, + "baseline_real_primitives": 224986, + "new_real_primitives": 169634, + "saved_real_primitives": 55352, + "primitive_tags": { + "add": 24236, + "clear": 42934, + "copy": 30452, + "double": 11170, + "halve": 38998, + "negate": 696, + "subtract": 21148 + }, + "primitive_word_sha256": "e342c630489789aa7e2aa938d8740ffc63d267d2420994be902893e7d9b50bf4", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "retained_prefix_l1_upper": "146068000389976309073/32", + "charged_payload_bits": 192 + }, + "jp8/forward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 22693, + "additions": 22211, + "unit_additions": 6215, + "baseline_real_primitives": 257232, + "new_real_primitives": 200380, + "saved_real_primitives": 56852, + "primitive_tags": { + "add": 29050, + "clear": 44454, + "copy": 32008, + "double": 32576, + "halve": 39438, + "negate": 692, + "subtract": 22162 + }, + "primitive_word_sha256": "21bdebedaf5ef43d0a9149e56d15e6287c87d5031bcfaad13973fb5c24a662fe", + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "retained_prefix_l1_upper": "4536094588619580433782972610869617/281474976710656", + "charged_payload_bits": 192 + }, + "jp8/backward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 22693, + "additions": 22219, + "unit_additions": 6223, + "baseline_real_primitives": 257280, + "new_real_primitives": 200396, + "saved_real_primitives": 56884, + "primitive_tags": { + "add": 29176, + "clear": 44470, + "copy": 31992, + "double": 32576, + "halve": 39438, + "negate": 692, + "subtract": 22052 + }, + "primitive_word_sha256": "c71f7fd2d52031e730f3ed42e56e38878e5746c053d990aad9d6e5c0d55d2bbd", + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "retained_prefix_l1_upper": "16753412757380464429924108070201913461/8388608", + "charged_payload_bits": 192 + } + }, + "distinct_coefficients": 686, + "controls": { + "coefficient": "-8403008", + "rejected": [ + "missing_cleanup", + "missing_source_copy", + "wrong_sign", + "redundant_work", + "endpoint_neutral_prefix_growth", + "unit_dirty_work_not_cleared", + "nondyadic", + "zero_coefficient", + "source_alias", + "work_alias" + ] + } + }, + "raw_factory_with_lowering": { + "before/forward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 16996, + "additions": 16440, + "unit_additions": 4456, + "baseline_real_primitives": 170488, + "new_real_primitives": 128696, + "saved_real_primitives": 41792, + "primitive_tags": { + "add": 16400, + "clear": 32912, + "copy": 23984, + "double": 556, + "halve": 37356, + "negate": 1008, + "subtract": 16480 + }, + "primitive_word_sha256": "863eebd9f07d48fce5432fe9827deeb17da68b05209463c4b0472b75586ff4c4", + "paid_profile": { + "1": 2024, + "2": 760, + "3": 300, + "4": 168, + "5": 168, + "6": 44, + "8": 8 + }, + "retained_prefix_l1_upper": "86491024246", + "charged_payload_bits": 192 + }, + "before/backward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 16996, + "additions": 16448, + "unit_additions": 4464, + "baseline_real_primitives": 170536, + "new_real_primitives": 128712, + "saved_real_primitives": 41824, + "primitive_tags": { + "add": 16704, + "clear": 32928, + "copy": 23968, + "double": 556, + "halve": 37356, + "negate": 1008, + "subtract": 16192 + }, + "primitive_word_sha256": "3ed14017939cb681e51232e4708c5819644a2b8a4b61124b4c870f03b727455c", + "paid_profile": { + "1": 2024, + "2": 760, + "3": 300, + "4": 168, + "5": 168, + "6": 44, + "8": 8 + }, + "retained_prefix_l1_upper": "2028759644357/2", + "charged_payload_bits": 192 + }, + "after/forward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 15512, + "additions": 15208, + "unit_additions": 3056, + "baseline_real_primitives": 160296, + "new_real_primitives": 123768, + "saved_real_primitives": 36528, + "primitive_tags": { + "add": 15168, + "clear": 30448, + "copy": 24320, + "double": 836, + "halve": 37412, + "negate": 336, + "subtract": 15248 + }, + "primitive_word_sha256": "6c4740a1e300f5ed503316fdae374de43f726c3a1c84486b80c6bde37103445b", + "paid_profile": { + "1": 2024, + "2": 760, + "3": 300, + "4": 168, + "5": 168, + "6": 44, + "8": 8 + }, + "retained_prefix_l1_upper": "68417", + "charged_payload_bits": 192 + }, + "after/backward": { + "all_input_columns": 716, + "dirty_helper_columns_restored": 492, + "scalar_macros": 15512, + "additions": 15216, + "unit_additions": 3064, + "baseline_real_primitives": 160344, + "new_real_primitives": 123784, + "saved_real_primitives": 36560, + "primitive_tags": { + "add": 15472, + "clear": 30464, + "copy": 24304, + "double": 836, + "halve": 37412, + "negate": 336, + "subtract": 14960 + }, + "primitive_word_sha256": "85afe26224475798889b89b238acbd66fa50045f646e6390d043218330326675", + "paid_profile": { + "1": 2024, + "2": 760, + "3": 300, + "4": 168, + "5": 168, + "6": 44, + "8": 8 + }, + "retained_prefix_l1_upper": "1649462", + "charged_payload_bits": 192 + } + }, + "emitted": { + "ck": { + "canonical_sha256": "9593109ef3f8cdfe56504023dd83d130a1ea111d3b3b0ad89719c3925bae6e67", + "one_real_component": true, + "artifact_name": "ck-PRIMITIVES.json.gz" + }, + "jp8": { + "canonical_sha256": "2e644979c36d23014d148c7fb00932e77abaf41122eea14d6f9db0aa7270a429", + "one_real_component": true, + "artifact_name": "jp8-PRIMITIVES.json.gz" + }, + "raw-before": { + "canonical_sha256": "9206932f985d8713122479b5df4030c56c695bbd42f4dddaf25ab2d188ba1503", + "one_real_component": true, + "artifact_name": "raw-before-PRIMITIVES.json.gz" + }, + "raw-after": { + "canonical_sha256": "a83b6a9f57e4cd944249421ebb3bc25236f1c6a1fe98aa36ac58a3342396cbe5", + "one_real_component": true, + "artifact_name": "raw-after-PRIMITIVES.json.gz" + } + } + }, + "new_kappa_claim": false +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr681-notice.md b/research/r420-optimal-composed-pairs/vendor/pr681-notice.md new file mode 100644 index 0000000000..638ce1b8d8 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr681-notice.md @@ -0,0 +1,156 @@ +# Consolidated supplier circuits: checked composition and integration batch + +**Finite circuit integration; no new κ.** This batch brings six pending research +packages into one tested integration, incorporates two earlier bit circuits +through their retained PR688 certificates, and composes PR681 with PR696. It +adds an opt-in executable path, exact receipts, a sufficient semantic D-boundary +proof, and a disposition table. It does not merely collect independent savings. + +| Measured operation bill | Before | Consolidated | Reduction | +|---|---:|---:|---:| +| Bit ADDs per local invocation | 26,916 | **18,378** | **31.72%** | +| Complete hosted bit instructions, 288 invocations | 8,603,712 | **6,144,768** | **28.58%** | +| Selected CK forward real-component primitives | 224,938 | **169,618** | **24.59%** | +| Selected CK inverse-transpose primitives | 224,986 | **169,634** | **24.60%** | +| Selected JP8 forward real-component primitives | 257,232 | **200,380** | **22.10%** | +| Selected JP8 inverse-transpose primitives | 257,280 | **200,396** | **22.11%** | +| Raw complex factory forward primitives, PR681 + PR696 | 170,488 | **123,768** | **27.40%** | +| Raw factory inverse-transpose primitives | 170,536 | **123,784** | **27.41%** | + +These rows are distinct bills and must not be summed into a runtime claim. +The selected conditional κ stays **0.001635527380375392**, exactly +`51110230636731/31250000000000000`. Scalar work decreases; recursive child +profiles remain unchanged. Raw factory improvements are not transported through +selected optimized provider recipes. Only PR696's lowering is used for the +selected CK/JP8 primitive rows. + +## Reproduce and use + +From the repository root, Python 3.11+: + +```sh +python3 -B research/supplier-circuit-consolidation/verify.py +``` + +The local command uses the standard library. It rebuilds and checks the combined +bit word, every scalar column and precision bound, both raw complex words, the +four selected complex programs, and the complete frozen receipt. It refuses +optimized Python because inherited auditors require assertions. + +For the complete native, whole-owner and invoice check, install NumPy, SciPy, +SymPy and a C++17 compiler with Boost headers, then run: + +```sh +python3 -B research/supplier-circuit-consolidation/verify.py --hosted --out /path/to/new-directory +``` + +Set `CXX` and `BOOST_INCLUDE` if needed. Expected final marker: + +```text +PASS_SUPPLIER_CIRCUIT_CONSOLIDATION bit_ADDs=26916->18378 saved=8538 hosted=True kappa=unchanged +``` + +Omitting `--out` uses a temporary directory. A named output directory must be +new; it retains baseline/replacement bit words, compiled-checker receipts, +whole-owner templates and invoices, and four `*-PRIMITIVES.json.gz` artifacts. +Those artifacts preserve all non-scalar events and replace scalar macros with +explicit real-component primitive instructions, carrying the macro's frame. +The complex bill charges two components. Primitive counts and sequence digests +are bound to the streams independently replayed by PR696's verifier. + +Normal commands compare `EXPECTED.json` or `HOSTED.json` exactly; `--write PATH` +is a development-only receipt regeneration mode. Package integrity checks: + +```sh +python3 -B research/supplier-circuit-consolidation/test_package.py +``` + +This tests a minimal source closure in a path with spaces, no Git metadata or +cached outputs, and five meaningful rejection/output-preservation controls. +The template `ci/supplier-circuit-consolidation.yml` defines Python 3.11/3.14 +local checks and a full Linux hosted replay. To activate it, copy it to +`.github/workflows/` using workflow-authorized access. GitHub rejected the +connected OAuth token's attempt to publish an active workflow because it lacks +`workflow` scope. No remote CI pass is claimed. + +## What actually composes + +- **PR694, Greer Guthrie:** all 201 helper-basis pairs are retained. +- **PR713, Scott Woolsey Biggart:** the target-row method is rerun on the new + helper-transformed matrix, yielding 56 pairs. The old 57-pair recipe and its + 3,150-ADD headline are not reused or added to PR694's saving. +- **PR691, mtpsl:** the complete 19-to-12-operation phase-A quad is retained. +- **PR670, yongjae321, and PR674, x0hu, via PR688, Ali Romman:** both smaller + phase-B circuits and their exact original certificates are retained. +- **PR708, Sagar Thakrar:** 23 of 27 decoder-sharing pairs fit the combined + precision budget. All 27 would save eight further ADDs but require 105 bits; + that version is an explicit rejection control. All leave-one-out variants + also fail. The finite compatibility pass is reproducible (372 extensions). +- **PR696, Sagar Thakrar:** the full selected complex lowering is retained and + additionally checked on the freshly rebuilt PR681 raw factory words. +- **PR681, Alluri:** all fourteen exact factory replacements are retained. + +PR686 is credited for the earlier one-pair compensation idea and semantic +D-prefix contract; its code is not imported. See `PROOF.md` for complete-map, +frame, restoration, composition and precision arguments. The bit substitutions +use the original geometry, helper inventory, nine COPYs and 5,112 rank mass. + +## Precision is repriced, not hidden + +| Precision quantity | Before | Consolidated | +|---|---:|---:| +| Local bit payload bound, bits | 100 | 104 (within strict `< 2^104`) | +| Raw hosted positive-prefix bound, bits | 189 | 196 | +| Charged hosted prefix allocation, bits | 192 | 256 | +| Two-level coefficient bound, bits | 416 | 432 | +| Charged two-level allocation, bits | 512 | 512 | + +The actual changed stream passes unchanged C++ 5/9/11-stage formal-column +checks and both inherited parent/whole-owner auditors. All 120,960 helper +invocations remain hosted without zero-bank allocation. The unchanged exact +moment engines reproduce bit saving `0.001653826988146798944268`. The hosted +invoice's cited PR484 outer calculation is a historical arithmetic control, +not a new selected assembly. + +The original literal H2 and K extractor cannot admit a temporary helper/target +basis. They are not patched or relabelled. The integration proves the exact +frame-zero D boundary and checks original H1-H5 on the canonical D with the +changed A/B/C. Native geometry and complete actual-word replay check the new +syntax separately. This semantic extension is explicit and independently +reviewable, not an ignored checker failure. + +## Maintainer handoff and attribution + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. `SOURCES.json` pins 235 consumed +source files and the exact imported heads. The six packages remain byte for +byte under their original research paths; their two standalone workflows are +represented by the broader activation-ready consolidation template. Their original validation +claims remain historical; `VALIDATION.md` records this integration's own runs. + +`DISPOSITIONS.json` separates retained source, composed scope and proposed +post-merge action. The linked central review-ledger supplement does not mark +these proposals published or change historical dispositions. After merge and +a fresh head check, a maintainer can resolve the six imported research PRs +with their preserved credit and remaining scope linked. PR670/674 have only +the cited circuit subset imported through PR688; full-PR closure is not claimed. +No other PR is merged, closed or modified by this batch. + +Prepared for **Alluri (@alluri-ritual)** with substantial **OpenAI Codex** +assistance in integration, code, proof analysis, verification and writing. +No independent human or delegated-agent review is claimed. Apache-2.0. +Credit remains with all component authors listed above and with eumemic, +Dylan Crow / DreamingOfClouds, Jeremy Kothe, icekylinx, Chafik Boukhalfa, +Dugongue, Zhihao Chen, DaysSky and the complete supplier/compiler/hosting +lineage in the original notices. Imported packages preserve their AI disclosures. + +Inherited all-size compiler, common-label/mutable-basis realization, physical +hosting, uniform precision/tape and analytic assumptions remain. This is a +finite integration candidate, not a formal multiplication theorem, optimal +circuit claim, new κ or measured practical runtime speedup. `upstream/` and +the selected certificate remain unchanged. + +Later arrivals #716 (optimal target pairs on the original matrix), #722 +(shared JP8 coefficient work) and #723 (signed-digit lowering) are credited +as related work outside this frozen batch. Their different matrix or work/prefix +boundaries require another composed recount. `OVERLAP.json` records the refreshed +549-PR queue through #730 and confirms unchanged imported heads. diff --git a/research/r420-optimal-composed-pairs/vendor/pr681-targets.json b/research/r420-optimal-composed-pairs/vendor/pr681-targets.json new file mode 100644 index 0000000000..f102e89b04 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr681-targets.json @@ -0,0 +1,286 @@ +{ + "seed": 5, + "oriented_pairs_scored": 14280, + "pairs": [ + [ + 222, + 219, + 46 + ], + [ + 145, + 148, + 44 + ], + [ + 233, + 239, + 42 + ], + [ + 236, + 234, + 42 + ], + [ + 143, + 137, + 41 + ], + [ + 230, + 224, + 40 + ], + [ + 139, + 141, + 39 + ], + [ + 225, + 231, + 36 + ], + [ + 144, + 149, + 35 + ], + [ + 120, + 125, + 35 + ], + [ + 133, + 131, + 35 + ], + [ + 174, + 173, + 35 + ], + [ + 193, + 194, + 34 + ], + [ + 156, + 200, + 34 + ], + [ + 182, + 176, + 33 + ], + [ + 185, + 191, + 32 + ], + [ + 181, + 196, + 32 + ], + [ + 170, + 189, + 31 + ], + [ + 134, + 128, + 31 + ], + [ + 217, + 220, + 28 + ], + [ + 138, + 140, + 28 + ], + [ + 229, + 227, + 27 + ], + [ + 208, + 214, + 27 + ], + [ + 198, + 178, + 26 + ], + [ + 199, + 179, + 26 + ], + [ + 154, + 205, + 25 + ], + [ + 136, + 142, + 25 + ], + [ + 235, + 237, + 25 + ], + [ + 152, + 158, + 24 + ], + [ + 207, + 202, + 24 + ], + [ + 124, + 122, + 24 + ], + [ + 151, + 146, + 24 + ], + [ + 162, + 135, + 24 + ], + [ + 238, + 232, + 24 + ], + [ + 211, + 167, + 23 + ], + [ + 212, + 210, + 23 + ], + [ + 216, + 221, + 22 + ], + [ + 171, + 186, + 22 + ], + [ + 183, + 195, + 20 + ], + [ + 163, + 166, + 20 + ], + [ + 215, + 209, + 20 + ], + [ + 169, + 187, + 19 + ], + [ + 123, + 126, + 19 + ], + [ + 218, + 223, + 18 + ], + [ + 197, + 180, + 17 + ], + [ + 157, + 155, + 16 + ], + [ + 165, + 160, + 16 + ], + [ + 184, + 175, + 15 + ], + [ + 168, + 177, + 14 + ], + [ + 127, + 121, + 11 + ], + [ + 172, + 190, + 11 + ], + [ + 188, + 150, + 11 + ], + [ + 203, + 206, + 11 + ], + [ + 228, + 226, + 10 + ], + [ + 132, + 129, + 7 + ], + [ + 161, + 164, + 3 + ] + ] +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr691-quad.json b/research/r420-optimal-composed-pairs/vendor/pr691-quad.json new file mode 100644 index 0000000000..6112423a46 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr691-quad.json @@ -0,0 +1,245 @@ +{ + "original": [ + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 5, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 4 + ], + [ + 1, + 0 + ], + [ + 2, + 4 + ], + [ + 2, + 0 + ], + [ + 0, + 5 + ], + [ + 0, + 2 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 2, + 5 + ], + [ + 2, + 1 + ] + ], + "replacement": [ + [ + 5, + 3 + ], + [ + 2, + 4 + ], + [ + 5, + 1 + ], + [ + 5, + 0 + ], + [ + 2, + 0 + ], + [ + 5, + 4 + ], + [ + 1, + 2 + ], + [ + 3, + 1 + ], + [ + 2, + 5 + ], + [ + 0, + 2 + ], + [ + 4, + 2 + ], + [ + 2, + 1 + ] + ], + "registers": [ + 267, + 347, + 349, + 376, + 467, + 491 + ], + "history": [ + 14, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12, + 12 + ], + "phase": "A", + "start": 873, + "stop": 892, + "frame": 315, + "quad": 13 +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr694-recipe.json b/research/r420-optimal-composed-pairs/vendor/pr694-recipe.json new file mode 100644 index 0000000000..d81608927f --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr694-recipe.json @@ -0,0 +1,1015 @@ +{ + "optimality_claim": false, + "orientations_per_pair": 2, + "pairs": [ + { + "dst": 552, + "net_saved_additions": 108, + "src": 521 + }, + { + "dst": 286, + "net_saved_additions": 97, + "src": 296 + }, + { + "dst": 275, + "net_saved_additions": 65, + "src": 448 + }, + { + "dst": 477, + "net_saved_additions": 65, + "src": 249 + }, + { + "dst": 425, + "net_saved_additions": 63, + "src": 415 + }, + { + "dst": 433, + "net_saved_additions": 63, + "src": 280 + }, + { + "dst": 360, + "net_saved_additions": 62, + "src": 350 + }, + { + "dst": 435, + "net_saved_additions": 62, + "src": 451 + }, + { + "dst": 395, + "net_saved_additions": 62, + "src": 369 + }, + { + "dst": 613, + "net_saved_additions": 62, + "src": 637 + }, + { + "dst": 549, + "net_saved_additions": 62, + "src": 584 + }, + { + "dst": 380, + "net_saved_additions": 62, + "src": 351 + }, + { + "dst": 404, + "net_saved_additions": 62, + "src": 304 + }, + { + "dst": 371, + "net_saved_additions": 62, + "src": 389 + }, + { + "dst": 386, + "net_saved_additions": 62, + "src": 365 + }, + { + "dst": 354, + "net_saved_additions": 62, + "src": 340 + }, + { + "dst": 370, + "net_saved_additions": 61, + "src": 348 + }, + { + "dst": 263, + "net_saved_additions": 61, + "src": 472 + }, + { + "dst": 463, + "net_saved_additions": 61, + "src": 289 + }, + { + "dst": 419, + "net_saved_additions": 61, + "src": 403 + }, + { + "dst": 313, + "net_saved_additions": 61, + "src": 422 + }, + { + "dst": 429, + "net_saved_additions": 61, + "src": 319 + }, + { + "dst": 550, + "net_saved_additions": 60, + "src": 650 + }, + { + "dst": 532, + "net_saved_additions": 60, + "src": 565 + }, + { + "dst": 639, + "net_saved_additions": 60, + "src": 597 + }, + { + "dst": 493, + "net_saved_additions": 60, + "src": 511 + }, + { + "dst": 531, + "net_saved_additions": 60, + "src": 566 + }, + { + "dst": 527, + "net_saved_additions": 60, + "src": 558 + }, + { + "dst": 547, + "net_saved_additions": 60, + "src": 586 + }, + { + "dst": 413, + "net_saved_additions": 60, + "src": 329 + }, + { + "dst": 551, + "net_saved_additions": 60, + "src": 582 + }, + { + "dst": 621, + "net_saved_additions": 60, + "src": 633 + }, + { + "dst": 376, + "net_saved_additions": 60, + "src": 372 + }, + { + "dst": 453, + "net_saved_additions": 60, + "src": 300 + }, + { + "dst": 442, + "net_saved_additions": 59, + "src": 277 + }, + { + "dst": 504, + "net_saved_additions": 58, + "src": 423 + }, + { + "dst": 602, + "net_saved_additions": 58, + "src": 583 + }, + { + "dst": 540, + "net_saved_additions": 58, + "src": 604 + }, + { + "dst": 400, + "net_saved_additions": 57, + "src": 324 + }, + { + "dst": 290, + "net_saved_additions": 56, + "src": 516 + }, + { + "dst": 467, + "net_saved_additions": 56, + "src": 268 + }, + { + "dst": 367, + "net_saved_additions": 55, + "src": 341 + }, + { + "dst": 303, + "net_saved_additions": 55, + "src": 454 + }, + { + "dst": 392, + "net_saved_additions": 54, + "src": 505 + }, + { + "dst": 627, + "net_saved_additions": 54, + "src": 248 + }, + { + "dst": 305, + "net_saved_additions": 54, + "src": 420 + }, + { + "dst": 595, + "net_saved_additions": 54, + "src": 655 + }, + { + "dst": 337, + "net_saved_additions": 54, + "src": 362 + }, + { + "dst": 272, + "net_saved_additions": 54, + "src": 436 + }, + { + "dst": 358, + "net_saved_additions": 54, + "src": 336 + }, + { + "dst": 622, + "net_saved_additions": 54, + "src": 634 + }, + { + "dst": 295, + "net_saved_additions": 54, + "src": 452 + }, + { + "dst": 414, + "net_saved_additions": 54, + "src": 317 + }, + { + "dst": 616, + "net_saved_additions": 54, + "src": 640 + }, + { + "dst": 375, + "net_saved_additions": 54, + "src": 390 + }, + { + "dst": 325, + "net_saved_additions": 54, + "src": 410 + }, + { + "dst": 449, + "net_saved_additions": 53, + "src": 291 + }, + { + "dst": 416, + "net_saved_additions": 53, + "src": 307 + }, + { + "dst": 345, + "net_saved_additions": 53, + "src": 394 + }, + { + "dst": 308, + "net_saved_additions": 53, + "src": 312 + }, + { + "dst": 461, + "net_saved_additions": 53, + "src": 445 + }, + { + "dst": 430, + "net_saved_additions": 53, + "src": 311 + }, + { + "dst": 409, + "net_saved_additions": 53, + "src": 431 + }, + { + "dst": 378, + "net_saved_additions": 53, + "src": 385 + }, + { + "dst": 399, + "net_saved_additions": 53, + "src": 393 + }, + { + "dst": 282, + "net_saved_additions": 53, + "src": 434 + }, + { + "dst": 383, + "net_saved_additions": 52, + "src": 387 + }, + { + "dst": 596, + "net_saved_additions": 52, + "src": 656 + }, + { + "dst": 614, + "net_saved_additions": 52, + "src": 638 + }, + { + "dst": 533, + "net_saved_additions": 52, + "src": 619 + }, + { + "dst": 601, + "net_saved_additions": 52, + "src": 649 + }, + { + "dst": 620, + "net_saved_additions": 52, + "src": 632 + }, + { + "dst": 580, + "net_saved_additions": 52, + "src": 544 + }, + { + "dst": 427, + "net_saved_additions": 52, + "src": 598 + }, + { + "dst": 278, + "net_saved_additions": 52, + "src": 570 + }, + { + "dst": 523, + "net_saved_additions": 52, + "src": 559 + }, + { + "dst": 469, + "net_saved_additions": 51, + "src": 479 + }, + { + "dst": 446, + "net_saved_additions": 51, + "src": 273 + }, + { + "dst": 548, + "net_saved_additions": 50, + "src": 585 + }, + { + "dst": 412, + "net_saved_additions": 50, + "src": 323 + }, + { + "dst": 529, + "net_saved_additions": 50, + "src": 539 + }, + { + "dst": 279, + "net_saved_additions": 49, + "src": 462 + }, + { + "dst": 608, + "net_saved_additions": 48, + "src": 659 + }, + { + "dst": 600, + "net_saved_additions": 48, + "src": 625 + }, + { + "dst": 610, + "net_saved_additions": 48, + "src": 528 + }, + { + "dst": 498, + "net_saved_additions": 48, + "src": 502 + }, + { + "dst": 603, + "net_saved_additions": 48, + "src": 346 + }, + { + "dst": 253, + "net_saved_additions": 46, + "src": 484 + }, + { + "dst": 355, + "net_saved_additions": 46, + "src": 497 + }, + { + "dst": 252, + "net_saved_additions": 45, + "src": 259 + }, + { + "dst": 492, + "net_saved_additions": 44, + "src": 338 + }, + { + "dst": 534, + "net_saved_additions": 44, + "src": 509 + }, + { + "dst": 495, + "net_saved_additions": 44, + "src": 568 + }, + { + "dst": 391, + "net_saved_additions": 44, + "src": 515 + }, + { + "dst": 246, + "net_saved_additions": 44, + "src": 240 + }, + { + "dst": 475, + "net_saved_additions": 44, + "src": 465 + }, + { + "dst": 243, + "net_saved_additions": 44, + "src": 456 + }, + { + "dst": 407, + "net_saved_additions": 44, + "src": 417 + }, + { + "dst": 255, + "net_saved_additions": 43, + "src": 474 + }, + { + "dst": 247, + "net_saved_additions": 43, + "src": 271 + }, + { + "dst": 251, + "net_saved_additions": 41, + "src": 260 + }, + { + "dst": 287, + "net_saved_additions": 40, + "src": 438 + }, + { + "dst": 569, + "net_saved_additions": 38, + "src": 575 + }, + { + "dst": 631, + "net_saved_additions": 38, + "src": 508 + }, + { + "dst": 457, + "net_saved_additions": 36, + "src": 437 + }, + { + "dst": 314, + "net_saved_additions": 34, + "src": 402 + }, + { + "dst": 443, + "net_saved_additions": 34, + "src": 455 + }, + { + "dst": 257, + "net_saved_additions": 32, + "src": 468 + }, + { + "dst": 283, + "net_saved_additions": 32, + "src": 288 + }, + { + "dst": 320, + "net_saved_additions": 30, + "src": 334 + }, + { + "dst": 306, + "net_saved_additions": 28, + "src": 326 + }, + { + "dst": 293, + "net_saved_additions": 28, + "src": 458 + }, + { + "dst": 459, + "net_saved_additions": 26, + "src": 364 + }, + { + "dst": 267, + "net_saved_additions": 26, + "src": 478 + }, + { + "dst": 285, + "net_saved_additions": 26, + "src": 447 + }, + { + "dst": 327, + "net_saved_additions": 24, + "src": 347 + }, + { + "dst": 342, + "net_saved_additions": 24, + "src": 359 + }, + { + "dst": 332, + "net_saved_additions": 22, + "src": 444 + }, + { + "dst": 441, + "net_saved_additions": 22, + "src": 269 + }, + { + "dst": 379, + "net_saved_additions": 22, + "src": 373 + }, + { + "dst": 330, + "net_saved_additions": 20, + "src": 440 + }, + { + "dst": 382, + "net_saved_additions": 20, + "src": 343 + }, + { + "dst": 242, + "net_saved_additions": 18, + "src": 470 + }, + { + "dst": 264, + "net_saved_additions": 18, + "src": 357 + }, + { + "dst": 381, + "net_saved_additions": 18, + "src": 615 + }, + { + "dst": 476, + "net_saved_additions": 18, + "src": 245 + }, + { + "dst": 418, + "net_saved_additions": 18, + "src": 315 + }, + { + "dst": 352, + "net_saved_additions": 18, + "src": 439 + }, + { + "dst": 261, + "net_saved_additions": 18, + "src": 483 + }, + { + "dst": 651, + "net_saved_additions": 18, + "src": 406 + }, + { + "dst": 401, + "net_saved_additions": 16, + "src": 361 + }, + { + "dst": 302, + "net_saved_additions": 16, + "src": 292 + }, + { + "dst": 310, + "net_saved_additions": 16, + "src": 363 + }, + { + "dst": 530, + "net_saved_additions": 16, + "src": 514 + }, + { + "dst": 256, + "net_saved_additions": 16, + "src": 266 + }, + { + "dst": 464, + "net_saved_additions": 14, + "src": 377 + }, + { + "dst": 328, + "net_saved_additions": 14, + "src": 421 + }, + { + "dst": 396, + "net_saved_additions": 14, + "src": 428 + }, + { + "dst": 368, + "net_saved_additions": 14, + "src": 384 + }, + { + "dst": 250, + "net_saved_additions": 14, + "src": 487 + }, + { + "dst": 318, + "net_saved_additions": 14, + "src": 450 + }, + { + "dst": 466, + "net_saved_additions": 12, + "src": 398 + }, + { + "dst": 557, + "net_saved_additions": 12, + "src": 658 + }, + { + "dst": 274, + "net_saved_additions": 12, + "src": 339 + }, + { + "dst": 374, + "net_saved_additions": 12, + "src": 460 + }, + { + "dst": 297, + "net_saved_additions": 12, + "src": 432 + }, + { + "dst": 471, + "net_saved_additions": 12, + "src": 301 + }, + { + "dst": 294, + "net_saved_additions": 10, + "src": 366 + }, + { + "dst": 349, + "net_saved_additions": 10, + "src": 581 + }, + { + "dst": 333, + "net_saved_additions": 10, + "src": 335 + }, + { + "dst": 344, + "net_saved_additions": 10, + "src": 331 + }, + { + "dst": 284, + "net_saved_additions": 10, + "src": 397 + }, + { + "dst": 244, + "net_saved_additions": 10, + "src": 411 + }, + { + "dst": 316, + "net_saved_additions": 10, + "src": 353 + }, + { + "dst": 496, + "net_saved_additions": 10, + "src": 567 + }, + { + "dst": 426, + "net_saved_additions": 10, + "src": 281 + }, + { + "dst": 322, + "net_saved_additions": 10, + "src": 507 + }, + { + "dst": 270, + "net_saved_additions": 8, + "src": 299 + }, + { + "dst": 405, + "net_saved_additions": 8, + "src": 298 + }, + { + "dst": 657, + "net_saved_additions": 8, + "src": 388 + }, + { + "dst": 574, + "net_saved_additions": 8, + "src": 545 + }, + { + "dst": 588, + "net_saved_additions": 8, + "src": 262 + }, + { + "dst": 606, + "net_saved_additions": 8, + "src": 254 + }, + { + "dst": 636, + "net_saved_additions": 8, + "src": 276 + }, + { + "dst": 624, + "net_saved_additions": 8, + "src": 473 + }, + { + "dst": 579, + "net_saved_additions": 8, + "src": 408 + }, + { + "dst": 503, + "net_saved_additions": 8, + "src": 265 + }, + { + "dst": 591, + "net_saved_additions": 6, + "src": 644 + }, + { + "dst": 642, + "net_saved_additions": 6, + "src": 593 + }, + { + "dst": 609, + "net_saved_additions": 6, + "src": 626 + }, + { + "dst": 499, + "net_saved_additions": 6, + "src": 241 + }, + { + "dst": 556, + "net_saved_additions": 6, + "src": 520 + }, + { + "dst": 618, + "net_saved_additions": 6, + "src": 635 + }, + { + "dst": 554, + "net_saved_additions": 6, + "src": 482 + }, + { + "dst": 589, + "net_saved_additions": 6, + "src": 646 + }, + { + "dst": 630, + "net_saved_additions": 6, + "src": 489 + }, + { + "dst": 560, + "net_saved_additions": 6, + "src": 424 + }, + { + "dst": 612, + "net_saved_additions": 6, + "src": 641 + }, + { + "dst": 525, + "net_saved_additions": 6, + "src": 561 + }, + { + "dst": 564, + "net_saved_additions": 6, + "src": 506 + }, + { + "dst": 645, + "net_saved_additions": 6, + "src": 590 + }, + { + "dst": 512, + "net_saved_additions": 6, + "src": 494 + }, + { + "dst": 587, + "net_saved_additions": 6, + "src": 546 + }, + { + "dst": 605, + "net_saved_additions": 6, + "src": 648 + }, + { + "dst": 643, + "net_saved_additions": 6, + "src": 592 + }, + { + "dst": 577, + "net_saved_additions": 6, + "src": 541 + }, + { + "dst": 538, + "net_saved_additions": 6, + "src": 309 + }, + { + "dst": 526, + "net_saved_additions": 6, + "src": 562 + }, + { + "dst": 563, + "net_saved_additions": 6, + "src": 522 + }, + { + "dst": 481, + "net_saved_additions": 6, + "src": 258 + }, + { + "dst": 491, + "net_saved_additions": 6, + "src": 321 + }, + { + "dst": 571, + "net_saved_additions": 6, + "src": 535 + }, + { + "dst": 517, + "net_saved_additions": 4, + "src": 553 + }, + { + "dst": 542, + "net_saved_additions": 4, + "src": 578 + }, + { + "dst": 607, + "net_saved_additions": 4, + "src": 628 + }, + { + "dst": 537, + "net_saved_additions": 4, + "src": 573 + }, + { + "dst": 519, + "net_saved_additions": 4, + "src": 555 + }, + { + "dst": 599, + "net_saved_additions": 4, + "src": 654 + }, + { + "dst": 524, + "net_saved_additions": 4, + "src": 543 + }, + { + "dst": 536, + "net_saved_additions": 4, + "src": 572 + }, + { + "dst": 576, + "net_saved_additions": 2, + "src": 652 + } + ], + "positive_pair_candidates": 27653, + "seed": 12, + "stopping_rule": "one score enumeration and one greedy matching", + "unordered_pairs_scored": 87990 +} diff --git a/research/r420-optimal-composed-pairs/vendor/pr733-targets.json b/research/r420-optimal-composed-pairs/vendor/pr733-targets.json new file mode 100644 index 0000000000..7c6acd2a10 --- /dev/null +++ b/research/r420-optimal-composed-pairs/vendor/pr733-targets.json @@ -0,0 +1,293 @@ +{ + "assignment_seed": 2, + "fixed_helper_recipe_sha256": "df48dd3b1c8d1d0f8894bb901043a9a8ba21777ecdacb21800c22fd71290d01e", + "matrix_scored": "KQ", + "ordered_target_pairs_scored": 14280, + "target_pairs": [ + [ + 222, + 219, + 46 + ], + [ + 145, + 148, + 44 + ], + [ + 239, + 233, + 42 + ], + [ + 236, + 234, + 42 + ], + [ + 143, + 137, + 41 + ], + [ + 230, + 224, + 40 + ], + [ + 139, + 141, + 39 + ], + [ + 225, + 231, + 36 + ], + [ + 174, + 173, + 35 + ], + [ + 120, + 125, + 35 + ], + [ + 133, + 131, + 35 + ], + [ + 144, + 149, + 35 + ], + [ + 193, + 194, + 34 + ], + [ + 156, + 200, + 34 + ], + [ + 182, + 176, + 33 + ], + [ + 181, + 196, + 32 + ], + [ + 185, + 191, + 32 + ], + [ + 134, + 128, + 31 + ], + [ + 170, + 189, + 31 + ], + [ + 138, + 140, + 28 + ], + [ + 217, + 220, + 28 + ], + [ + 229, + 227, + 27 + ], + [ + 208, + 214, + 27 + ], + [ + 198, + 178, + 26 + ], + [ + 199, + 179, + 26 + ], + [ + 136, + 142, + 25 + ], + [ + 154, + 205, + 25 + ], + [ + 235, + 237, + 25 + ], + [ + 238, + 232, + 24 + ], + [ + 151, + 146, + 24 + ], + [ + 207, + 202, + 24 + ], + [ + 162, + 135, + 24 + ], + [ + 124, + 122, + 24 + ], + [ + 152, + 158, + 24 + ], + [ + 212, + 210, + 23 + ], + [ + 211, + 209, + 23 + ], + [ + 216, + 221, + 22 + ], + [ + 171, + 186, + 22 + ], + [ + 183, + 195, + 20 + ], + [ + 213, + 215, + 20 + ], + [ + 163, + 166, + 20 + ], + [ + 123, + 126, + 19 + ], + [ + 169, + 187, + 19 + ], + [ + 218, + 223, + 18 + ], + [ + 197, + 180, + 17 + ], + [ + 157, + 155, + 16 + ], + [ + 165, + 160, + 16 + ], + [ + 184, + 175, + 15 + ], + [ + 168, + 177, + 14 + ], + [ + 172, + 190, + 11 + ], + [ + 203, + 206, + 11 + ], + [ + 127, + 121, + 11 + ], + [ + 188, + 150, + 11 + ], + [ + 228, + 226, + 10 + ], + [ + 159, + 167, + 8 + ], + [ + 132, + 129, + 7 + ], + [ + 161, + 164, + 3 + ] + ] +} diff --git a/research/r420-optimal-composed-pairs/verify.py b/research/r420-optimal-composed-pairs/verify.py new file mode 100644 index 0000000000..0ccab0820c --- /dev/null +++ b/research/r420-optimal-composed-pairs/verify.py @@ -0,0 +1,434 @@ +#!/usr/bin/env python3 +"""Exact target-matching certificate on the fixed PR694 basis, composed with PR681. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance, Apache-2.0. +Circuit mechanisms and the native/hosted drivers retain their predecessor credit. +""" +import argparse +from collections import Counter +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import struct +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BIT = ROOT / 'research/e8-bit-r420/data/bitE8mut-r420.json.gz' +CHECK = ROOT / 'research/e8-bit-r420/code/xcheck.py' +EXPORT = ROOT / 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + data = Path(path).read_bytes() + return json.loads(gzip.decompress(data) if str(path).endswith('.gz') else data) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def module(path): + spec = importlib.util.spec_from_file_location('paired_' + path.stem, path) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result + + +def source_check(): + pins = read(HERE / 'SOURCES.json') + for name, pin in pins['imported'].items(): + data = (HERE / name).read_bytes() + need(hashlib.sha256(data).hexdigest() == pin['sha256'], 'import changed: ' + name) + blob = b'blob ' + str(len(data)).encode() + b'\0' + data + need(hashlib.sha1(blob).hexdigest() == pin['git_blob'], 'import Git blob: ' + name) + for name, pin in pins['base_files'].items(): + data = (ROOT / name).read_bytes() + if pin['representation'] == 'gzip-payload': + data = gzip.decompress(data) + else: + need(pin['representation'] == 'file-bytes', 'unknown source representation') + need(hashlib.sha256(data).hexdigest() == pin['sha256'], 'base source changed: ' + name) + return pins + + +def cleanup(word): + return [[1, d, list(ss)] for _, d, ss in reversed(word['A'] + word['B']) + if not 120 <= d < 240] + + +def body(original): + """Reconstruct PR681's A/B/C from its immutable, attributed recipes.""" + word = copy.deepcopy(original) + q = read(HERE / 'vendor/pr691-quad.json') + regs = q['registers'] + need(word['A'][q['start']:q['stop']] == + [[q['frame'], regs[d], [regs[s]]] for d, s in q['original']], 'quad input slice') + word['A'][q['start']:q['stop']] = [[q['frame'], regs[d], [regs[s]]] + for d, s in q['replacement']] + b = read(HERE / 'vendor/pr674-block.json') + word['B'][371:417] = [[547, d, [s]] for d, s in b['replacement_ops']] + b = read(HERE / 'vendor/pr670-block.json') + regs = b['registers'] + word['B'][263:313] = [[545, regs[d], [regs[s]]] for d, s in b['replacement_local_ops']] + r = read(HERE / 'vendor/pr681-decoders.json') + need(r['pairs'] == [r['source_pairs'][i] for i in r['selected_indices']], 'decoder recipe subset') + tail = word['A'][-9:] + need([g[1] for g in tail] == word['ret'] and all(g[0] == 1 for g in tail), 'decoder location') + pre = [[1, a, [b]] for a, b in r['pairs']] + transformed = [] + for frame, dst, sources in tail: + row = set(sources) + for a, b in r['pairs']: + if a in row: + row.symmetric_difference_update({b}) + transformed.append([frame, dst, sorted(row)]) + word['A'] = word['A'][:-9] + pre + transformed + copy.deepcopy(pre[::-1]) + word['C'] = cleanup(word) + return word + + +def helper_matrix(original): + rows = {d: set(sources) for frame, d, sources in original['D']} + need(len(rows) == 120 and set(rows) == set(range(120, 240)), 'canonical D targets') + prefix, used = [], set() + for pair in read(HERE / 'vendor/pr694-recipe.json')['pairs']: + a, b = pair['dst'], pair['src'] + need(type(a) is int and type(b) is int and 240 <= a < 660 and 240 <= b < 660 + and a != b and not ({a, b} & used), 'helper pair domain') + used.update((a, b)) + before = sum(map(len, rows.values())) + for row in rows.values(): + if a in row: + row.symmetric_difference_update({b}) + need(before - sum(map(len, rows.values())) - 2 == pair['net_saved_additions'], 'helper price') + prefix.append([0, a, [b]]) + need(len(prefix) == 201 and sum(map(len, rows.values())) == 12586, 'fixed helper matrix') + return rows, prefix + + +def gain(rows, a, b): + return len(rows[b]) - len(rows[a] ^ rows[b]) - 2 + + +def matching_check(rows, pairs, prices): + need(len(prices) == 120 and all(type(q) is int and q >= 0 for q in prices), 'dual domain') + for a, b in itertools.combinations(range(120, 240), 2): + weight = max(0, gain(rows, a, b), gain(rows, b, a)) + need(prices[a-120] + prices[b-120] >= 2*weight, 'dual edge inequality') + used, saving = set(), 0 + for pair in pairs: + need(len(pair) == 3 and all(type(x) is int for x in pair), 'matching integer triple') + a, b, score = pair + need(120 <= a < 240 and 120 <= b < 240 and a != b and not ({a, b} & used), 'matching overlap/domain') + need(score == gain(rows, a, b) and score > 0, 'oriented matching price') + used.update((a, b)) + saving += score + need(2*saving == sum(prices), 'dual/primal objective gap') + return {'unordered_edges': 7140, 'oriented_edges': 14280, 'pairs': len(pairs), + 'saving': saving, 'twice_dual_objective': sum(prices)} + + +def substitute(word, original, pairs): + rows, helpers = helper_matrix(original) + targets, used = [], set() + for a, b, score in pairs: + need(a in rows and b in rows and a != b and not ({a, b} & used), 'target matching domain') + need(gain(rows, a, b) == score and score > 0, 'target gain') + used.update((a, b)) + rows[b] ^= rows[a] + targets.append([0, b, [a]]) + result = copy.deepcopy(word) + result['D'] = helpers + targets + [[0, t, sorted(row)] for t, row in sorted(rows.items())] + result['D'] += copy.deepcopy(targets[::-1] + helpers[::-1]) + return result + + +def d_operator(word): + rows = [{i} for i in range(660)] + for frame, dst, sources in word['D']: + need(frame == 0 and word['frames'][frame] == [] and 120 <= dst < 660 and sources, + 'D frame/destination') + need(len(set([dst] + sources)) == len(sources)+1 and all(120 <= s < 660 for s in sources), 'D operands') + need(dst < 240 or all(s >= 240 for s in sources), 'target feeds helper') + for source in sources: + rows[dst].symmetric_difference_update(rows[source]) + return rows + + +def scalar_events(word): + for phase in ('D', 'A', 'scatter', 'B', 'C'): + if phase == 'scatter': + for k, source in enumerate(word['ret']): + yield ('copy', 660, source) + for t, row in enumerate(word['scatter']): + if k in row: + yield ('add', 120+t, 660) + yield ('erase', 660, source) + else: + for _, dst, sources in word[phase]: + for source in sources: + yield ('add', dst, source) + + +def replay(events, reverse=False): + """Separate set-valued 660-input replay plus integer positive row bounds.""" + rows = [{i} for i in range(660)] + [set()] + bound = [1]*660 + [0] + peak, opened, copies = 1, None, 0 + for kind, dst, src in reversed(events) if reverse else events: + if reverse and kind != 'add': + kind = 'copy' if kind == 'erase' else 'erase' + if kind == 'add': + need(0 <= dst < 660 and 0 <= src <= 660 and dst != src + and (src != 660 or opened is not None) and dst != opened, 'scalar ADD/lifecycle') + rows[dst].symmetric_difference_update(rows[src]) + bound[dst] += bound[src] + peak = max(peak, bound[dst]) + elif kind == 'copy': + need(opened is None and dst == 660 and not rows[660], 'COPY lifecycle') + rows[660] = set(rows[src]); bound[660] = bound[src] + opened = src; copies += 1 + elif kind == 'erase': + need(opened == src and dst == 660 and rows[660] == rows[src], 'ERASE lifecycle') + rows[660] = set(); bound[660] = 0; opened = None + else: + raise ValueError('unknown event') + expected = [{i} for i in range(660)] + [set()] + for t in range(120): + expected[120+t].add(t) + need(rows == expected and opened is None and copies == 9, 'full arbitrary-input endpoint') + return peak + + +def frame_paths(word, dimensions): + paths = [[f] for f in word['start']] + paid = Counter() + for phase in ('D', 'A', 'scatter', 'B', 'C', 'final'): + if phase == 'scatter': + for r in word['ret']: + paid[dimensions[paths[r][-1]]] += 1 + continue + gates = [[f, r, []] for r, f in enumerate(word['final'])] if phase == 'final' else word[phase] + for frame, dst, sources in gates: + for r in [dst] + sources: + old = paths[r][-1] + if frame != old: + rank = dimensions[frame]-dimensions[old] + need(rank > 0 and set(word['frames'][old]) <= set(word['frames'][frame]), 'frame ascent') + paid[rank] += 1; paths[r].append(frame) + return paths, {str(r): n for r, n in sorted(paid.items())} + + +def receipt(word, dimensions): + events = list(scalar_events(word)) + f, b = replay(events), replay(events, True) + payload = 64*f**3*b**2 + need(payload < 2**104, '104-bit payload cap') + paths, paid = frame_paths(word, dimensions) + return {'semantic_word_sha256': digest(word), 'scalar_stream_sha256': digest(events), + 'binary_additions': sum(e[0] == 'add' for e in events), + 'D_binary_additions': sum(len(g[2]) for g in word['D']), 'D_grouped_gates': len(word['D']), + 'forward_and_reverse': [{'copies': 9, 'columns': 660} for _ in range(2)], + 'forward_prefix': f, 'reverse_prefix': b, 'payload_prefix_upper': str(payload), + 'payload_prefix_bits': payload.bit_length(), 'paid_histogram': paid, + 'rank_mass': sum(int(r)*n for r, n in paid.items()), 'frame_paths_sha256': digest(paths)} + + +def export_check(word, result, out): + word_path = out / 'word.json.gz' + word_path.write_bytes(gzip.compress(canonical(word)+b'\n', mtime=0)) + subprocess.run([sys.executable, '-I', '-B', str(EXPORT), str(word_path), str(out/'records')], + check=True, stdout=subprocess.DEVNULL) + data = (out/'records/249-records.bin').read_bytes() + need(len(data) % 24 == 0, 'record alignment') + events, paid = [], Counter() + for op, a, b, c, d, e in struct.iter_unpack('<6i', data): + if op == 0: + paid[d] += 1 + elif op == 1: + need(c == 1, 'ADD coefficient'); events.append(('add', a, b)) + elif op == 2: + paid[e] += 1; events.append(('copy', b, a)) + elif op == 3: + events.append(('erase', b, a)) + else: + raise ValueError('unknown record') + need(events == list(scalar_events(word)), 'exported scalar events differ') + need({str(k): v for k, v in sorted(paid.items())} == result['paid_histogram'], 'exported paid profile') + result.update(exported_records=len(data)//24, record_sha256=hashlib.sha256(data).hexdigest()) + + +def controls(original, before, after, cert): + names = [] + def reject(name, action): + try: + action() + except ValueError: + names.append(name) + else: + raise ValueError('control accepted: ' + name) + expected = d_operator(original) + for name, index in [('helper preparation', 0), ('target preparation', 201), + ('target restoration', -202), ('helper restoration', -1), ('middle read', 259)]: + wrong = copy.deepcopy(after); del wrong['D'][index] + reject('omit '+name, lambda w=wrong: need(d_operator(w) == expected, 'D endpoint')) + wrong = copy.deepcopy(after); wrong['D'][0][0] = 1 + reject('D leaves frame zero', lambda: d_operator(wrong)) + rows, _ = helper_matrix(original) + reject('zero vertex prices', lambda: matching_check(rows, cert['pairs'], [0]*120)) + wrong_pairs = copy.deepcopy(cert['pairs']); wrong_pairs.append(wrong_pairs[0]) + reject('overlapping target pairs', lambda: matching_check(rows, wrong_pairs, cert['doubled_vertex_prices'])) + wrong_prices = list(cert['doubled_vertex_prices']) + wrong_prices[11] += 1 + reject('feasible but nontight dual', lambda: matching_check(rows, cert['pairs'], wrong_prices)) + wrong_pairs = copy.deepcopy(cert['pairs']); wrong_pairs[0][2] += 1 + reject('inflated pair saving', lambda: matching_check(rows, wrong_pairs, cert['doubled_vertex_prices'])) + # A pairing certificate for K cannot be substituted for the transformed KQ. + stale = {d: set(ss) for _, d, ss in original['D']} + reject('certificate on original K', lambda: matching_check(stale, cert['pairs'], cert['doubled_vertex_prices'])) + wrong = copy.deepcopy(after); wrong['C'].pop() + reject('missing cleanup', lambda: replay(list(scalar_events(wrong)))) + neutral = copy.deepcopy(after) + neutral['D'].extend([[0, 240, [241]], [0, 240, [241]]]) + need(d_operator(neutral) == expected, 'neutral pair endpoint') + need(sum(e[0] == 'add' for e in scalar_events(neutral)) == + sum(e[0] == 'add' for e in scalar_events(after))+2, 'neutral operations uncharged') + return names + ['neutral endpoint accepted and two ADDs charged'] + + +def run(out): + pins = source_check() + original = read(BIT) + cert = read(HERE / 'OPTIMUM.json') + need(cert['assignment_seed'] == 11, 'assignment seed') + rows, _ = helper_matrix(original) + optimum = matching_check(rows, cert['pairs'], cert['doubled_vertex_prices']) + need(optimum['saving'] == cert['gain'] == 1442, 'optimum value') + integrated = body(original) + old_pairs = read(HERE / 'vendor/pr681-targets.json')['pairs'] + before = substitute(integrated, original, old_pairs) + after = substitute(integrated, original, cert['pairs']) + pr733 = read(HERE/'vendor/pr733-targets.json') + need(pr733['fixed_helper_recipe_sha256'] == hashlib.sha256( + (HERE/'vendor/pr694-recipe.json').read_bytes()).hexdigest(), 'PR733 fixed helper recipe differs') + same_body = substitute(integrated, original, pr733['target_pairs']) + need(d_operator(before) == d_operator(after) == d_operator(original), 'semantic D substitution') + checker = module(CHECK) + checked, _, _, h, c, _ = checker.check(original) + need(all(h.values()) and all(c.values()), 'original H1-H5') + canonical_word = copy.copy(checked); canonical_word.w = integrated + canonical_word.full() + h, c, _ = canonical_word.interface() + need(all(h.values()) and all(c.values()), 'canonical integrated H1-H5') + for word in (before, after, same_body): + obj = copy.copy(checked); obj.w = word; obj.full() + h, c, _ = obj.interface() + need(not h['H2_D_frame0_targets_from_helpers'] and not c['K_equals_D'], 'literal guard unexpectedly accepts') + need(all(v for k, v in h.items() if k != 'H2_D_frame0_targets_from_helpers'), 'other H hypothesis') + results = {} + for name, word in [('baseline', before), ('replacement', after)]: + folder = out/(name+'-export'); folder.mkdir() + results[name] = receipt(word, checked.fdim) + export_check(word, results[name], folder) + (out/(name+'.json.gz')).write_bytes(gzip.compress(canonical(word)+b'\n', mtime=0)) + expected = read(HERE / 'vendor/pr681-expected.json')['bit']['replacement'] + need(results['baseline'] == expected, 'PR681 exact bit receipt differs') + old, new = results['baseline'], results['replacement'] + need(old['binary_additions'] == 18378 and new['binary_additions'] == 18362, 'composed cost') + for key in ('forward_prefix', 'reverse_prefix', 'paid_histogram', 'rank_mass', 'frame_paths_sha256'): + need(old[key] == new[key], 'composed envelope/profile differs: ' + key) + prior = receipt(same_body, checked.fdim) + need(prior['binary_additions'] == 18370 and prior['D_binary_additions'] == 11554, + 'PR733 matching on the same PR681 body') + for key in ('forward_prefix', 'reverse_prefix', 'paid_histogram', 'rank_mass', 'frame_paths_sha256'): + need(prior[key] == new[key], 'same-body comparator differs: ' + key) + result = {'status': 'PASS_R420_OPTIMAL_COMPOSED_PAIRS', 'base_commit': pins['base_commit'], + **results, 'saved_additions': 16, 'selected_ADDs': 26916, 'saved_from_selected': 8554, + 'matching_optimum': optimum, 'controls': controls(original, before, after, cert), + 'PR733_matching_on_PR681_body': prior, 'saved_beyond_prior_matching_on_same_body': 8, + 'inherited_PR733_ADDs': 18548, 'same_optimum_on_PR733_body_ADDs': 18540, + 'literal_H2_claimed': False, 'semantic_D_columns': 660, 'no_new_kappa': True} + (out/'LOCAL.json').write_text(json.dumps(result, indent=2)+'\n') + return result + + +def deterministic(value): + if isinstance(value, dict): + return {k: deterministic(v) for k, v in value.items() if k != 'seconds'} + if isinstance(value, list): + return [deterministic(v) for v in value] + return value + + +def native_controls(out, local, native): + for name in ('baseline', 'replacement'): + need(native[name]['legality']['common_frame_ADDs'] == local[name]['binary_additions'], 'native absolute cost') + for stage in native[name]['stages'].values(): + need(stage['receipt']['local_scalar_additions'] == local[name]['binary_additions'], 'native stage cost') + raw = (out/'replacement/cout/COHORT249-RECORDS.bin').read_bytes() + rows = list(struct.iter_unpack('<6i', raw)) + index = max(i for i, e in enumerate(rows) if e[0] == 1 and e[5] == 1 and e[1] >= 240) + mutant = out/'missing-helper-return.bin' + mutant.write_bytes(b''.join(struct.pack('<6i', *e) for i, e in enumerate(rows) if i != index)) + for pairs in (2, 4, 5): + rejected = subprocess.run([str(out/('bin/columns'+str(pairs))), str(mutant), + str(out/('invalid'+str(pairs)+'.json'))], capture_output=True, text=True) + need(rejected.returncode != 0 and 'local defining-decoder full formal column' in rejected.stderr, + 'native missing restoration was not rejected by the endpoint check') + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--out', type=Path, help='fresh output directory') + p.add_argument('--native', action='store_true') + p.add_argument('--hosted', action='store_true', help='includes native replay') + p.add_argument('--record', type=Path, help='write a candidate receipt for review; not a certificate PASS') + args = p.parse_args() + if args.out: + need(not args.out.exists(), 'output already exists') + args.out.mkdir(parents=True) + out = args.out + temporary = None + else: + temporary = tempfile.TemporaryDirectory(prefix='r420-optimal-pairs-') + out = Path(temporary.name) + result = run(out) + if args.record: + need(not args.record.exists(), 'record destination already exists') + args.record.write_text(json.dumps(result, indent=2)+'\n') + print('RECORDED_CANDIDATE_RECEIPT', args.record) + else: + need(result == read(HERE/'CERTIFICATE.json'), 'committed certificate differs') + if args.native or args.hosted: + native = module(HERE/'native.py').run(ROOT, out) + native_controls(out, result, native) + need(deterministic(native) == read(HERE/'NATIVE.json'), 'native certificate differs') + (out/'NATIVE.json').write_text(json.dumps(native, indent=2)+'\n') + if args.hosted: + hosted = module(HERE/'hosted.py').run(ROOT, out) + need(deterministic(hosted) == read(HERE/'HOSTED.json'), 'hosted certificate differs') + (out/'HOSTED.json').write_text(json.dumps(hosted, indent=2)+'\n') + print('PASS_R420_OPTIMAL_COMPOSED_PAIRS optimum=1442 pairs=58 edges=7140 ' + 'ADDs=18378->18362 payload_bits=104 columns=660 controls=13 no_new_kappa') + if temporary: + temporary.cleanup() + + +if __name__ == '__main__': + main()