From 3147cac35c659152d36db1e0e60b9ce4b152c008 Mon Sep 17 00:00:00 2001 From: thakrarsagar Date: Tue, 13 Oct 2026 11:31:12 +0530 Subject: [PATCH] Certify fixed-basis R420 target matching and the eight-ADD gap Attain the exact 1442 matching saving on fixed KQ, with full native and hosted replay. Save eight ADDs beyond PR733 on the same PR681 body, or sixteen versus published PR681. No new kappa. Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. --- .../CERTIFICATE.json | 129 +++ .../r420-optimal-composed-pairs/CLAIM.json | 71 ++ .../r420-optimal-composed-pairs/HOSTED.json | 184 +++ .../r420-optimal-composed-pairs/NATIVE.json | 352 ++++++ .../r420-optimal-composed-pairs/OPTIMUM.json | 420 +++++++ .../PACKAGE-TESTS.json | 47 + .../r420-optimal-composed-pairs/README.md | 226 ++++ .../r420-optimal-composed-pairs/SOURCES.json | 649 +++++++++++ .../r420-optimal-composed-pairs/VALIDATION.md | 117 ++ .../r420-optimal-composed-pairs/hosted.py | 90 ++ .../independent_check.py | 121 ++ .../r420-optimal-composed-pairs/native.py | 79 ++ .../vendor/pr670-block.json | 199 ++++ .../vendor/pr674-block.json | 865 ++++++++++++++ .../vendor/pr681-decoders.json | 354 ++++++ .../vendor/pr681-expected.json | 438 +++++++ .../vendor/pr681-notice.md | 156 +++ .../vendor/pr681-targets.json | 286 +++++ .../vendor/pr691-quad.json | 245 ++++ .../vendor/pr694-recipe.json | 1015 +++++++++++++++++ .../vendor/pr733-targets.json | 293 +++++ .../r420-optimal-composed-pairs/verify.py | 434 +++++++ 22 files changed, 6770 insertions(+) create mode 100644 research/r420-optimal-composed-pairs/CERTIFICATE.json create mode 100644 research/r420-optimal-composed-pairs/CLAIM.json create mode 100644 research/r420-optimal-composed-pairs/HOSTED.json create mode 100644 research/r420-optimal-composed-pairs/NATIVE.json create mode 100644 research/r420-optimal-composed-pairs/OPTIMUM.json create mode 100644 research/r420-optimal-composed-pairs/PACKAGE-TESTS.json create mode 100644 research/r420-optimal-composed-pairs/README.md create mode 100644 research/r420-optimal-composed-pairs/SOURCES.json create mode 100644 research/r420-optimal-composed-pairs/VALIDATION.md create mode 100644 research/r420-optimal-composed-pairs/hosted.py create mode 100644 research/r420-optimal-composed-pairs/independent_check.py create mode 100644 research/r420-optimal-composed-pairs/native.py create mode 100644 research/r420-optimal-composed-pairs/vendor/pr670-block.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr674-block.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr681-decoders.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr681-expected.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr681-notice.md create mode 100644 research/r420-optimal-composed-pairs/vendor/pr681-targets.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr691-quad.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr694-recipe.json create mode 100644 research/r420-optimal-composed-pairs/vendor/pr733-targets.json create mode 100644 research/r420-optimal-composed-pairs/verify.py 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()