diff --git a/.github/workflows/r439-deferred-native.yml b/.github/workflows/r439-deferred-native.yml new file mode 100644 index 0000000000..f10ec7d0a1 --- /dev/null +++ b/.github/workflows/r439-deferred-native.yml @@ -0,0 +1,70 @@ +name: R439 deferred target native replay +on: + pull_request: + paths: + - "research/r439-deferred-native/**" + - ".github/workflows/r439-deferred-native.yml" + - "research/e8-bit-carrier-skeleton/LICENSE" + - "research/e8-bit-carrier-skeleton/NOTICE.md" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp" + - "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + - "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py" + - "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h" + - "research/e8-bit-p111-tuned/code/xcheck_p.py" + - "research/r439-gl5-shortest/NOTICE.md" + - "research/r439-gl5-shortest/candidate.json.gz" + - "research/r439-gl5-shortest/native.py" + - "research/r439-gl5-shortest/literal.py" + push: + branches: [main] + paths: + - "research/r439-deferred-native/**" + - ".github/workflows/r439-deferred-native.yml" + - "research/e8-bit-carrier-skeleton/LICENSE" + - "research/e8-bit-carrier-skeleton/NOTICE.md" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp" + - "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp" + - "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + - "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py" + - "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h" + - "research/e8-bit-p111-tuned/code/xcheck_p.py" + - "research/r439-gl5-shortest/NOTICE.md" + - "research/r439-gl5-shortest/candidate.json.gz" + - "research/r439-gl5-shortest/native.py" + - "research/r439-gl5-shortest/literal.py" + workflow_dispatch: +permissions: + contents: read +jobs: + native: + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + fetch-depth: 0 + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.12' + - name: Native dependencies + run: sudo apt-get update && sudo apt-get install -y g++ libboost-dev + - name: Finite replay and package controls + run: python -B scripts/research_package.py --package research/r439-deferred-native + - name: Fresh native 5/9/11-stage replay + env: + PYTHONOPTIMIZE: '2' + REPLAY_DIR: ${{ runner.temp }}/r439-deferred-native + run: python -I -O -B research/r439-deferred-native/verify.py --native --output "$REPLAY_DIR" + - name: Source tree unchanged + run: git diff --exit-code + - name: Upload native records, logs and receipt + if: always() + uses: actions/upload-artifact@v4 + with: + name: r439-deferred-native + path: ${{ runner.temp }}/r439-deferred-native + if-no-files-found: warn diff --git a/research/r439-deferred-native/FINITE.json b/research/r439-deferred-native/FINITE.json new file mode 100644 index 0000000000..8ac3506623 --- /dev/null +++ b/research/r439-deferred-native/FINITE.json @@ -0,0 +1,85 @@ +{ + "all_dirty_columns": 661, + "controls": [ + "missing undo gate", + "old scatter", + "wrong undo order", + "undo after first target climb" + ], + "directions": 2, + "new_kappa_claim": false, + "owner_false": { + "0": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "1": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ] + }, + "payloads": { + "0": "b381d9bc18820b89f92485826ff9f8449d0f72f7599772d52c14e07d6b89b7f2", + "1": "e7dd976535977adb327cfe03847324eef05f0d76b38bf120a17a79facac495bf" + }, + "phase_ADDs": { + "0": { + "1": 5548, + "2": 1626, + "3": 527, + "4": 800, + "5": 1991 + }, + "1": { + "1": 5242, + "2": 1626, + "3": 97, + "4": 1106, + "5": 1991 + } + }, + "prices": { + "0": { + "ADDs": 10492, + "B": 3758418, + "F": 13667, + "admitted": true, + "local_bits": 91, + "local_upper": "2307861360443122886999501568", + "nine_bits": 175, + "nine_upper": "24941709210337926871896158204497246778939630375927808" + }, + "1": { + "ADDs": 10062, + "B": 2825146, + "F": 13667, + "admitted": true, + "local_bits": 91, + "local_upper": "1304011286425361906630611712", + "nine_bits": 173, + "nine_upper": "7962867333575952586253133241476806906784083238453248" + } + }, + "sources": { + "research/e8-bit-carrier-skeleton/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "research/e8-bit-carrier-skeleton/NOTICE.md": "5f4b7fcbf99f572be28b6da612ce775363908cdfc7810f7aca167be01c86e49a", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/r439-gl5-shortest/NOTICE.md": "c37d4ba8f547fe492ea1834f985c86778d9b57460e16d27682fd338279d5db0f", + "research/r439-gl5-shortest/candidate.json.gz": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359", + "research/r439-gl5-shortest/literal.py": "619f9df6db6f9ef004aaeeb6aa04239850ebf5dde313936bd64e0f4e4e15fbd9", + "research/r439-gl5-shortest/native.py": "1766e96047132d97b6c9cb77c7d692b66df9311511c870e6b79156c14706007e", + "vendor/pr2115/EXPECTED.json": "8412f4025843af6400745faeb192ba976fd293702ee7322af1b7992fd0a05841", + "vendor/pr2115/PROOF.md": "3a921c0e7cb8670dc28980e08635e0c1361f88f5391b14254438b56a699e488b", + "vendor/pr2115/README.md": "69269d301d23a37242953449ef7d231fc820311f7c59ffb86625ac401a9560de", + "vendor/pr2115/candidate-1188.json.gz": "b0d74149ddb9333338ccee9fda6e84ea9aaa60b63000dcf783c4208f3fe3c8fb" + }, + "status": "PASS_R439_DEFERRED_FINITE", + "undo_gates": 306 +} diff --git a/research/r439-deferred-native/NATIVE.json b/research/r439-deferred-native/NATIVE.json new file mode 100644 index 0000000000..c25a328796 --- /dev/null +++ b/research/r439-deferred-native/NATIVE.json @@ -0,0 +1,767 @@ +{ + "exported_phase_ADDs": { + "0": { + "1": 5548, + "2": 1626, + "3": 527, + "4": 800, + "5": 1991 + }, + "1": { + "1": 5242, + "2": 1626, + "3": 97, + "4": 1106, + "5": 1991 + } + }, + "finite_payloads": { + "0": "b381d9bc18820b89f92485826ff9f8449d0f72f7599772d52c14e07d6b89b7f2", + "1": "e7dd976535977adb327cfe03847324eef05f0d76b38bf120a17a79facac495bf" + }, + "finite_result_sha256": "c0df006fe93529accc73a939fdc2042f79bc2c50e8a6593be5067ef7bb434794", + "native": { + "0": { + "common_frame_ADDs": 10492, + "copies": 9, + "erasures": 9, + "nine_stage_admitted": true, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 13421, + "staged": { + "11": { + "bridge_additions": 2664, + "controls_rejected": 24, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "2307861360443122886999501568", + "reverse_fresh_center_copies": 45, + "scalar_ADDs": 115412, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3758418", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 10 + } + ] + }, + "5": { + "bridge_additions": 666, + "controls_rejected": 6, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "2307861360443122886999501568", + "reverse_fresh_center_copies": 18, + "scalar_ADDs": 52460, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3758418", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 4 + } + ] + }, + "9": { + "bridge_additions": 1998, + "controls_rejected": 18, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "2307861360443122886999501568", + "reverse_fresh_center_copies": 36, + "scalar_ADDs": 94428, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3758418", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 10492, + "signed_inverse": false, + "stage": 8 + } + ] + } + } + }, + "1": { + "common_frame_ADDs": 10062, + "copies": 9, + "erasures": 9, + "nine_stage_admitted": true, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 12991, + "staged": { + "11": { + "bridge_additions": 2664, + "controls_rejected": 24, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "1304011286425361906630611712", + "reverse_fresh_center_copies": 45, + "scalar_ADDs": 110682, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2825146", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 10 + } + ] + }, + "5": { + "bridge_additions": 666, + "controls_rejected": 6, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "1304011286425361906630611712", + "reverse_fresh_center_copies": 18, + "scalar_ADDs": 50310, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2825146", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 4 + } + ] + }, + "9": { + "bridge_additions": 1998, + "controls_rejected": 18, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "payload_prefix_bits": 91, + "payload_prefix_upper": "1304011286425361906630611712", + "reverse_fresh_center_copies": 36, + "scalar_ADDs": 90558, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "13667", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2825146", + "reverse": true + } + ], + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 10062, + "signed_inverse": false, + "stage": 8 + } + ] + } + } + } + }, + "native_controls": [ + { + "control": "missing-undo", + "reason": "local defining-decoder full formal column", + "rejected": true, + "returncode": 2 + }, + { + "control": "old-scatter", + "reason": "local defining-decoder full formal column", + "rejected": true, + "returncode": 2 + }, + { + "control": "late-undo", + "reason": "illegal or mispriced MOVE", + "rejected": true, + "returncode": -6 + }, + { + "control": "phase-label-only", + "labels_changed": 306, + "native_engines_accept": true, + "phase_binding_rejects": true + }, + { + "control": "count-preserving-phase-exchange", + "phase_counts_accept": true, + "record_binding_rejects": true + } + ], + "native_omitted_bridge_controls": 96, + "new_kappa_claim": false, + "record_sha256": { + "0": "2df55087c71725651b7fc531323a371810f6c8c6d49d84d2c397bdc2d1862133", + "1": "9732a8373b845d090615a39a693dc3c1fdb165777aa9b136f4f86aaac8f90e0c" + }, + "status": "PASS_R439_DEFERRED_NATIVE" +} diff --git a/research/r439-deferred-native/NOTICE.md b/research/r439-deferred-native/NOTICE.md new file mode 100644 index 0000000000..e07e3db1b0 --- /dev/null +++ b/research/r439-deferred-native/NOTICE.md @@ -0,0 +1,12 @@ +New integration package by Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance. Apache-2.0. + +PR2115 candidate, proof and README: Sagar Thakrar, with substantial Anthropic Claude assistance; copied unchanged from b56dceffad83c88e8ad39ffd82a1bdd55c4130da. All predecessor credits and disclosures in vendor/pr2115/README.md remain in force. + +literal.py and native.py are adaptations of Gareth Davidson's PR1188 code, retaining the PR1122/980/926, PR837 and PR967 lineage named in their headers. Exact original source hashes are recorded in SOURCES.json. This package does not claim the reused mathematical engines as independently written. + +Unchanged consumed native/checker/exporter notices: +- ../e8-bit-carrier-skeleton/NOTICE.md and LICENSE +- ../r439-gl5-shortest/NOTICE.md +- ../e8-bit-p111-tuned/code/xcheck_p.py (source attribution) + +The repository root LICENSE applies to new work. No source-specific notices are removed or superseded. diff --git a/research/r439-deferred-native/PREDECESSOR.json b/research/r439-deferred-native/PREDECESSOR.json new file mode 100644 index 0000000000..bd550b164a --- /dev/null +++ b/research/r439-deferred-native/PREDECESSOR.json @@ -0,0 +1,30 @@ +{ + "pr": 2115, + "head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "files": { + "vendor/pr2115/candidate-1188.json.gz": { + "commit": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "source_path": "research/r439-deferred-target-basis-seed06/candidate-1188.json.gz", + "git_blob": "e72404c4578a3fe19ea12321ddc28dfa0196961b", + "sha256": "b0d74149ddb9333338ccee9fda6e84ea9aaa60b63000dcf783c4208f3fe3c8fb" + }, + "vendor/pr2115/README.md": { + "commit": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "source_path": "research/r439-deferred-target-basis-seed06/README.md", + "git_blob": "65f1c7c1ba199153dd511d0aedf0d850a918b2df", + "sha256": "69269d301d23a37242953449ef7d231fc820311f7c59ffb86625ac401a9560de" + }, + "vendor/pr2115/PROOF.md": { + "commit": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "source_path": "research/r439-deferred-target-basis-seed06/PROOF.md", + "git_blob": "a4e52fd2bab145a31a01d6c99bf61b43fb81affb", + "sha256": "3a921c0e7cb8670dc28980e08635e0c1361f88f5391b14254438b56a699e488b" + }, + "vendor/pr2115/EXPECTED.json": { + "commit": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", + "source_path": "research/r439-deferred-target-basis-seed06/EXPECTED.json", + "git_blob": "074ede527a574d597392db0ca3df567ffbfc8a99", + "sha256": "8412f4025843af6400745faeb192ba976fd293702ee7322af1b7992fd0a05841" + } + } +} diff --git a/research/r439-deferred-native/README.md b/research/r439-deferred-native/README.md new file mode 100644 index 0000000000..fb525e39f1 --- /dev/null +++ b/research/r439-deferred-native/README.md @@ -0,0 +1,76 @@ +# Native replay of the deferred R439 target basis + +The exact deferred PR1188 candidate in Sagar Thakrar's [PR2115](https://github.com/CrocSwap/integer-mult-bounds/pull/2115), head `b56dceffad83c88e8ad39ffd82a1bdd55c4130da`, passes the unchanged native legality and 5/9/11-stage formal-column engines. This completes its README **Open next questions, item 4**, for one committed candidate. It verifies an implementation boundary; the circuit, replacement H5 lemma and 430-ADD saving belong to PR2115. + +The selected supplier and exponent are unchanged. This is a finite native integration check, not hosted admission or a proof of the full multiplication theorem. + +## Exact object and boundary + +The baseline is Gareth Davidson's retained PR1188 word, `research/r439-gl5-shortest/candidate.json.gz`. The candidate is PR2115's unchanged `candidate-1188.json.gz`, canonical payload SHA256 `e7dd976535977adb327cfe03847324eef05f0d76b38bf120a17a79facac495bf`. Its 306 target-basis undo gates move from zero-frame D (exporter phase 1) to the beginning of B (phase 4), before any target climbs. The scatter is expressed in the prepared target basis. + +A new reconstruction reads the baseline's two inverse 306-gate blocks, moves the literal undo, applies the preparation to all nine scatter columns, and compares the **entire** resulting JSON payload with the pinned candidate. It imports no PR2115 generator. The full dirty COPY/ADD/ERASE interpreter and native harness are adapted from PR1188 and credited, not offered as newly independent algorithms. The original exporter, stage wrapper, owner checker and C++ engines execute from pinned, unchanged source bytes. + +For both words, exact symbolic execution checks all 661 source, target and arbitrary dirty-helper columns in both directions. It requires the boundary `(x,y,h) -> (x,y+x,h)`, clean copied storage at every reuse and equality with its original source at ERASE. The inherited owner checker still reports H2/K false on the baseline, and H2/K/**H5** false on the deferred word. Those flags are retained. PR2115's argued `VR=I` bridge is the proposed replacement; native success does not turn the old H5 flag true. + +## Complete local and staged bills + +| Quantity | PR1188 baseline | Exact deferred candidate | +|---|---:|---:| +| D / A / scatter / B / C ADDs | 5548 / 1626 / 527 / 800 / 1991 | 5242 / 1626 / 97 / 1106 / 1991 | +| Total ADDs | 10,492 | 10,062 | +| Native records | 13,421 | 12,991 | +| Native MOVEs | 2,911 | 2,911 | +| COPY / ERASE | 9 / 9 | 9 / 9 | +| Rank mass | 5,129 | 5,129 | +| Positive forward bound F | 13,667 | 13,667 | +| Positive reverse bound B | 3,758,418 | 2,825,146 | +| Local / nine-stage guard bits | 91 / 175 | 91 / 173 | + +All 306 undo gates remain charged. The native and literal bounds agree exactly; `64 F^3 B^2 < 2^104` and `2^18 F^5 B^4 < 2^192` hold. The paid profile remains `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`. Per-register ordered MOVE paths and COPY/ERASE records are compared across the words. + +The freshly compiled engines check 883, 1327 and 1549 independent global formal columns at 5, 9 and 11 stages. Candidate scalar ADD totals are 50,310, 90,558 and 110,682, plus respectively 666, 1998 and 2664 bridge ADDs. There are 45, 81 and 99 fresh COPYs; each corresponding reverse stage also executes its recorded lifecycle. All 96 inherited omitted-bridge controls across the two words reject. Eleven-stage column success is not an assertion of a separate eleven-stage precision cap. + +Even granting scalar work for free leaves the recursive profile unchanged. No improved moment or kappa follows from this result. + +## What the failure controls establish + +Four finite controls reject a missing undo gate, the old scatter, reversed undo order, and undo after a target's first climb. Three of these are also executed through the actual native tools: the first two fail the local full formal-column boundary; late undo fails MOVE legality. + +A fourth native probe changes only the 306 undo ADD phase labels from 4 to 1. **Both unchanged native engines accept it.** Inspection confirms they use the literal records' order, geometry and coefficients, not ADD phase labels. This is a scope limit of those engines, not an alleged failure of their stated mathematical checks. The new replay separately checks the exported phase counts and the complete raw-record SHA256 against PR2115's pinned exporter receipts. It rejects the relabeling. A fifth probe swaps two phase labels while preserving every phase count; only the complete record binding rejects it. + +The correct record hashes are `2df55087c71725651b7fc531323a371810f6c8c6d49d84d2c397bdc2d1862133` (baseline) and `9732a8373b845d090615a39a693dc3c1fdb165777aa9b136f4f86aaac8f90e0c` (candidate). They bind exact deterministic binary instruction traces, not regenerated gzip containers. Source gzip files stay byte-pinned; newly emitted gzip words are compared through complete decoded payloads. + +## Reproduce + +Python 3.12, C++17 and Boost headers are sufficient. From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/r439-deferred-native +BOOST_INCLUDE=/path/to/boost/include python3.12 -I -B research/r439-deferred-native/verify.py --native --output /absolute/new/output +``` + +Omit `BOOST_INCLUDE` for system headers; `CXX` selects the compiler. `--native` recompiles all four binaries and compares the complete deterministic result with `NATIVE.json`. Output must be a new directory, and all generated data stay outside the source package. Omitting `--output` uses temporary storage. Explicit `--write` regenerates receipts during development. Child exporter assertions stay enabled even when the wrapper runs with `-O` and inherited `PYTHONOPTIMIZE=2`. + +The generic registered replay checks the finite contract and the real entry point in a Git-free read-only export, including source and typed-receipt corruption. **It does not run C++.** The separate `r439-deferred-native.yml` workflow runs the native command with Boost and uploads its output. A metadata or generic-replay pass must not be reported as a native run. Expected native marker: + +```text +PASS_R439_DEFERRED_NATIVE words=2 stages=5,9,11 controls=96+5 no_new_kappa +``` + +`VALIDATION.json` records the actual local environment and executed commands. Source bytes, historical assignment, predecessor provenance and mathematical receipts are in SOURCES, SELECTION, TASK, PREDECESSOR, FINITE and NATIVE. No hosted CI success is inferred from local execution. + +## Scope and overlap + +The fresh random draw `f0fe3489369e5f7a530effe408323d98` chose `bit-helper-contract`, priority revision 4, on canonical main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Its prescribed PR1062 baseline passed. The scope is **changed**: PR1194/PR1311/PR1806 already cover the original H2/K route; this takes the explicit native handoff for PR2115's target-basis/H5 extension. PR2279 proves the best undo-ideal scatter count, and PR2356 concerns interleaved taps in two undo orders. Neither covers this native two-word replay. The claim and final overlap checkpoint are linked in TASK.json. + +Only the exact full-deferral PR1188 candidate is checked. The 94-scatter-ADD order-ideal refinement and PR1868 twisted-helper variants are not inferred from it. Full hosted emission/invoice, physical projector routing, recursive scratch allocation, all-size compilation, common-label realization, precision/tape and outer analytic assembly remain outside this replay. No Lean kernel proof is claimed. Supplier adoption is separate maintainer work. + +## Open next questions + +Can this exact word pass a complete changed-word hosted emission and invoice? Start from the PR1806 route, bind its actual owner/routing and phase records to this exact deferred payload, and charge recursive child output plus scratch. This matters because local formal columns and native MOVE legality do not establish the physical hosting/allocator contract. Changed-word hosted emission and inherited compiler/common-label/precision/tape obligations remain blockers. TASK.json gives the structured handoff. + +## Credit + +Sagar Thakrar / PR2115 supplies the target-basis deferral, replacement H5 proof and all circuit savings. Gareth Davidson / PR1188 supplies the baseline, literal interpreter and native harness, following his PR1122/980/926 and Sagar Thakrar's PR837 and Sricharan Vagvala's PR967 harnesses. The retained lineage includes PR915/PR794 target compensation, Sagar Thakrar PR1062, Aaron Wang PR1015, Ross Richardson PR923/936, Sricharan Vagvala PR967, DreamingOfClouds PR589 and eumemic PR555/543; Dylan Crow supplies the exporter. Credit the scalar-interface and checker authors retained in their notices. PR1194 (woklerx), PR1311 (Arham Tahir), PR1806 (mtpsl) and Hanson Sun's PR1902 establish the semantic and replay context. + +PR2115's README and proof are preserved verbatim under vendor/pr2115. The upstream native, owner and lineage notices remain unchanged; NOTICE.md links them. Prepared by **Gareth Davidson (@bitplane)** with substantial **OpenAI Codex assistance** in research, implementation, validation and writing. No subagents or independent human review. Apache-2.0. diff --git a/research/r439-deferred-native/SELECTION.json b/research/r439-deferred-native/SELECTION.json new file mode 100644 index 0000000000..5aa697197c --- /dev/null +++ b/research/r439-deferred-native/SELECTION.json @@ -0,0 +1,93 @@ +{ + "seed": "f0fe3489369e5f7a530effe408323d98", + "track": "bit-mechanisms", + "suggestions": [ + { + "task_id": "bit-helper-contract", + "scope_key": "3475f46c8358c6a9211b", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "method": "Derive a replacement interface lemma and price its implementation.", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/r439-deferred-native/SOURCES.json b/research/r439-deferred-native/SOURCES.json new file mode 100644 index 0000000000..a9bbe9108c --- /dev/null +++ b/research/r439-deferred-native/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/e8-bit-carrier-skeleton/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/e8-bit-carrier-skeleton/NOTICE.md", + "usage": "input", + "git_blob": "5a0ecdcd2c7fad0488740a1da0f633b73b56a809", + "sha256": "5f4b7fcbf99f572be28b6da612ce775363908cdfc7810f7aca167be01c86e49a" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "usage": "input", + "git_blob": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "usage": "input", + "git_blob": "82d69f7c5d044c9887c96b90c97f5639083ecd14", + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "usage": "input", + "git_blob": "cb1233c7e96b1aa8bbf4d2e4165d75ab0dca64b9", + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "usage": "input", + "git_blob": "f6d7afe3e623208c4207b6a683a1e3e49249e31c", + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + { + "path": "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h", + "usage": "input", + "git_blob": "fc5664e929d9a81d9b4926bee049a93330be86ec", + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/r439-gl5-shortest/NOTICE.md", + "usage": "input", + "git_blob": "726353d12642af44fccc90401ea9a53d6e5e4bca", + "sha256": "c37d4ba8f547fe492ea1834f985c86778d9b57460e16d27682fd338279d5db0f" + }, + { + "path": "research/r439-gl5-shortest/candidate.json.gz", + "usage": "input", + "git_blob": "0d4dd2fb241a00cab1b57b17991db82bc06edd91", + "sha256": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359" + }, + { + "path": "research/r439-gl5-shortest/native.py", + "usage": "input", + "git_blob": "13355f66eb7344a5e9d3d0b5044ab2ac6dc425e3", + "sha256": "1766e96047132d97b6c9cb77c7d692b66df9311511c870e6b79156c14706007e" + }, + { + "path": "research/r439-gl5-shortest/literal.py", + "usage": "input", + "git_blob": "196ee6fdc81bddec7aafeb51a71f9f31755d5480", + "sha256": "619f9df6db6f9ef004aaeeb6aa04239850ebf5dde313936bd64e0f4e4e15fbd9" + } + ] +} diff --git a/research/r439-deferred-native/TASK.json b/research/r439-deferred-native/TASK.json new file mode 100644 index 0000000000..e1d56eb954 --- /dev/null +++ b/research/r439-deferred-native/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact PR2115 committed candidate-1188 through unchanged native legality and 5/9/11-stage engines, with explicit phase/source binding and complete local bills.", + "scope_change_reason": "The drawn H2/K lemma is already covered by PR1194/PR1311/PR1806. Take PR2115 README Open next questions item 4: relocation of 306 target undo gates from D to B under its H5 replacement has not been replayed natively. This is an integration audit of a target-basis contract, not a new helper-star lemma.", + "bottleneck_link": "Discharges the explicit finite native implementation handoff for the replacement target-basis boundary. Scalar savings and unchanged recursive profile belong to PR2115; this does not improve the binding complex budget.", + "budget_minutes": 60, + "stop_rule": "Complete the exact two-word 5/9/11-stage replay and controls, or report a concrete native failure. No candidate search or source checker edits.", + "outcome": "completed", + "evidence": "FINITE.json and NATIVE.json; exact predecessor bytes and root source pins; verify.py --native; test_package.py.", + "author": "Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in scoping, implementation, execution and writing; no subagents or independent human review.", + "open_questions": [ + { + "question": "Does the exact deferred PR1188 word pass full hosted emission and its complete supplier invoice?", + "why_it_matters": "Native local geometry and staged formal columns do not bind physical owner routing or recursive scratch allocation.", + "first_step": "Adapt the PR1806 hosted-invoice route to the source-bound deferred payload, preserving all actual MOVE/COPY and phase records.", + "blocked_by": "Changed-word hosted emission and physical/compiler, common-label, precision/tape and all-size obligations remain; this contribution does not select the supplier." + } + ], + "selection": { + "seed": "f0fe3489369e5f7a530effe408323d98", + "scope_key": "3475f46c8358c6a9211b", + "method": "Derive a replacement interface lemma and price its implementation." + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2362", + "predecessor": { + "pr": 2115, + "head": "b56dceffad83c88e8ad39ffd82a1bdd55c4130da" + }, + "submission_checkpoint": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_changed": false, + "selected_record_changed": false, + "predecessor_head_unchanged": true, + "overlap_at_utc": "2026-10-15T06:48:57.525544+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T06:47:19.758487+00:00", + "complete_pagination": true, + "records": 578 + }, + "discussions": { + "fetched_at": "2026-10-15T06:48:57.472922+00:00", + "complete_pagination": true, + "records": 1104 + } + }, + "warnings": [], + "matches_reviewed": 15, + "decision": "Proceed: PR2279/PR2356 concern distinct scatter costs and interleavings; no overlapping exact native replay found. Searches omit arbitrary diffs and are not a novelty certificate." + } +} diff --git a/research/r439-deferred-native/VALIDATION.json b/research/r439-deferred-native/VALIDATION.json new file mode 100644 index 0000000000..fe65cc16e4 --- /dev/null +++ b/research/r439-deferred-native/VALIDATION.json @@ -0,0 +1,36 @@ +{ + "status": "LOCAL_EXECUTED_NOT_HOSTED_CI", + "native_result_sha256": "81a58df4e5dd52985051951afae5b63d46a39c619c1f119d0b3917a5f077405f", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.43", + "python312": "Python 3.12.3", + "python314": "Python 3.14.4", + "compiler": "c++ (Ubuntu 15.2.0-16ubuntu1) 15.2.0", + "boost": "Ubuntu libboost1.90-dev 1.90.0-6ubuntu1; extracted only in scratch", + "boost_deb_sha256": "7b89698c907fd5d33ccd439674fa53803139923822181c87b910579827aca379", + "runs": { + "REGISTERED.log": { + "sha256": "bb7c002f80a2096099b7fe613442e7dac44c6cf54ffe4b81ed7017a2592eb4ce", + "log": "CHECK Two exact payloads, independent deferral reconstruction, reused full dirty forward/reverse interpretation, phase invoice, inherited owner flags and four mathematical controls; source/receipt binding.\nPASS_R439_DEFERRED_FINITE columns=661 directions=2 phase_transfer=306 saving=430 no_new_kappa\nCHECK Git-free read-only relocation and three actual-entry-point source/typed-receipt corruption controls under optimization.\nPASS_DEFERRED_PACKAGE readonly_git_free_files=31 corruption_controls=3\nPASS_REGISTERED_RESEARCH_PACKAGE research/r439-deferred-native outcome=completed\n" + }, + "NATIVE-FINAL.log": { + "sha256": "c3b0838d85ca9b4f44223000cf3b323f077d51920b3c005640da791327e57ed9", + "log": "native deferred word 0\nnative deferred word 1\nPASS_R439_DEFERRED_NATIVE words=2 stages=5,9,11 controls=96+5 no_new_kappa\n" + }, + "EXPORT314.log": { + "sha256": "c3b0838d85ca9b4f44223000cf3b323f077d51920b3c005640da791327e57ed9", + "log": "native deferred word 0\nnative deferred word 1\nPASS_R439_DEFERRED_NATIVE words=2 stages=5,9,11 controls=96+5 no_new_kappa\n" + } + }, + "readonly_export": { + "files": 31, + "git": false, + "native_replayed": true, + "contents_unchanged": true + }, + "commands": [ + "python3.12 -I -B scripts/research_package.py --package research/r439-deferred-native", + "BOOST_INCLUDE= PYTHONOPTIMIZE=2 python3.12 -I -O -B research/r439-deferred-native/verify.py --native --write --output ", + "BOOST_INCLUDE= PYTHONOPTIMIZE=2 python3.14 -I -O -B /research/r439-deferred-native/verify.py --native --output " + ], + "limits": "Finite Python controls and full native C++ executed locally. Hosted CI not claimed; no hosted supplier emission/all-size proof." +} diff --git a/research/r439-deferred-native/VERIFY.json b/research/r439-deferred-native/VERIFY.json new file mode 100644 index 0000000000..1934cf60bc --- /dev/null +++ b/research/r439-deferred-native/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-carrier-skeleton/LICENSE", + "research/e8-bit-carrier-skeleton/NOTICE.md", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/r439-gl5-shortest/NOTICE.md", + "research/r439-gl5-shortest/candidate.json.gz", + "research/r439-gl5-shortest/native.py", + "research/r439-gl5-shortest/literal.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two exact payloads, independent deferral reconstruction, reused full dirty forward/reverse interpretation, phase invoice, inherited owner flags and four mathematical controls; source/receipt binding." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only relocation and three actual-entry-point source/typed-receipt corruption controls under optimization." + } + ] +} diff --git a/research/r439-deferred-native/common.py b/research/r439-deferred-native/common.py new file mode 100644 index 0000000000..0c02a7d9dc --- /dev/null +++ b/research/r439-deferred-native/common.py @@ -0,0 +1,73 @@ +"""Strict source binding and JSON I/O. Gareth Davidson / OpenAI Codex; Apache-2.0.""" +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +HUB = "research/e8-bit-carrier-skeleton" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def same(left, right, message): + need(canonical(left) == canonical(right), message) + + +def pairs(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key: " + key) + result[key] = value + return result + + +def invalid(value): + raise ValueError("nonfinite JSON: " + value) + + +def load(path): + path = Path(path) + raw = path.read_bytes() + if path.suffix == ".gz": + raw = gzip.decompress(raw) + return json.loads(raw, object_pairs_hook=pairs, parse_constant=invalid) + + +def write(path, value): + path = Path(path) + raw = canonical(value) + if path.suffix == ".gz": + raw = gzip.compress(raw, mtime=0) + else: + raw = (json.dumps(value, indent=2, sort_keys=True, allow_nan=False) + "\n").encode() + with path.open("xb") as stream: + stream.write(raw) + + +def pins(root=ROOT): + checked = {} + for row in load(HERE / "SOURCES.json")["files"]: + if row["usage"] == "input": + raw = (Path(root) / row["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "source hash: " + row["path"]) + checked[row["path"]] = row["sha256"] + predecessor = load(HERE / "PREDECESSOR.json") + need(predecessor["head"] == "b56dceffad83c88e8ad39ffd82a1bdd55c4130da", "predecessor head") + for path, row in predecessor["files"].items(): + raw = (HERE / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "vendor source hash: " + path) + checked[path] = row["sha256"] + return checked diff --git a/research/r439-deferred-native/literal.py b/research/r439-deferred-native/literal.py new file mode 100644 index 0000000000..40c0edda20 --- /dev/null +++ b/research/r439-deferred-native/literal.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Literal COPY/ADD/ERASE interpreter, adapted unchanged in its execution and pricing from PR1188/1122. + +Set-valued streams and source-binding patterns follow PR926/967/980. +Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance. +Apache-2.0. No assertion is needed for rejection in this verifier. +""" +import argparse +import ast +import copy +from pathlib import Path +import runpy +import tempfile + +C = runpy.run_path(str(Path(__file__).with_name("common.py"))) +need, same, load = C["need"], C["same"], C["load"] + + +def instructions(word): + n = 2 * word["v"] + word["R"] + out = [] + for phase in ("D", "A", "scatter", "B", "C"): + if phase == "scatter": + for j, center in enumerate(word["ret"]): + out.append(("copy", n, center)) + for i, uses in enumerate(word["scatter"]): + if j in uses: + out.append(("add", word["v"] + i, n)) + out.append(("erase", n, center)) + else: + for frame, d, donors in word[phase]: + need(type(frame) is int and 0 <= frame < len(word["frames"]), "frame domain") + need(type(d) is int and 0 <= d < n, "destination domain") + need(type(donors) is list and len(set(donors)) == len(donors), "distinct donors") + need(all(type(s) is int and 0 <= s < n and s != d for s in donors), "donor domain") + out.extend(("add", d, s) for s in donors) + return out + + +def execute(word, reverse=False, stream=None): + """Sets of formal columns plus integer positive bounds; COPY work starts empty.""" + n = 2 * word["v"] + word["R"] + symbolic = [{i} for i in range(n)] + [set()] + positive = [1] * n + [0] + stream = instructions(word) if stream is None else stream + opened, peak, adds, copies, erasures = False, 1, 0, 0, 0 + for kind, d, s in reversed(stream) if reverse else stream: + if reverse and kind != "add": + kind = "erase" if kind == "copy" else "copy" + if kind == "add": + need(d < n, "private COPY target cannot be ADD destination") + need(s != n or opened, "private COPY read outside lifetime") + symbolic[d].symmetric_difference_update(symbolic[s]) + positive[d] += positive[s] + adds += 1 + elif kind == "copy": + need(d == n and not opened and not symbolic[n] and positive[n] == 0, "COPY destination not empty") + symbolic[n] = set(symbolic[s]) + positive[n] = positive[s] + opened = True + copies += 1 + elif kind == "erase": + need(d == n and opened and symbolic[n] == symbolic[s], "ERASE original changed or missing COPY") + symbolic[n] = set() + positive[n] = 0 + opened = False + erasures += 1 + else: + raise ValueError("unknown instruction") + peak = max(peak, positive[d]) + need(not opened and not symbolic[n] and positive[n] == 0, "unclosed private COPY") + expected = [{i} for i in range(n)] + for i in range(word["v"]): + expected[word["v"] + i].add(i) + need(symbolic[:-1] == expected, "dirty full-word boundary") + need(copies == erasures == 9, "complete COPY bill") + return dict(ADDs=adds, bound=peak, copies=copies, erasures=erasures, + columns=n, instructions=len(stream)) + + +def phase_rows(word, phase, reverse=False): + n = 2 * word["v"] + word["R"] + rows = [{i} for i in range(n)] + for _, d, donors in reversed(word[phase]) if reverse else word[phase]: + for s in donors: + rows[d].symmetric_difference_update(rows[s]) + return rows + + +def literal_cleanup(word): + fulls = [i for i, f in enumerate(word["frames"]) if sorted(f) == list(range(word["v"]))] + need(len(fulls) == 1, "one full frame") + reverse = [] + for phase in ("B", "A"): + for gate in word[phase][::-1]: + if not word["v"] <= gate[1] < 2 * word["v"]: + reverse.append([fulls[0], gate[1], list(gate[2])]) + same(reverse, word["C"], "literal cleanup") + + +def literal_price(word): + forward, reverse = execute(word), execute(word, True) + same(forward["ADDs"], reverse["ADDs"], "reverse ADD bill") + f, b = forward["bound"], reverse["bound"] + local, nine = 2**6 * f * f * f * b * b, 2**18 * f**5 * b**4 + return dict(ADDs=forward["ADDs"], F=f, B=b, local_upper=str(local), nine_upper=str(nine), + local_bits=local.bit_length(), nine_bits=nine.bit_length(), + admitted=local < 2**104 and nine < 2**192) + + +def require_admission(price): + need(int(price["local_upper"]) < 2**104, "local precision cap") + need(int(price["nine_upper"]) < 2**192, "nine-stage precision cap") diff --git a/research/r439-deferred-native/native.py b/research/r439-deferred-native/native.py new file mode 100644 index 0000000000..fea13f81ef --- /dev/null +++ b/research/r439-deferred-native/native.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Deferred-target words through unchanged native legality and 5/9/11-stage checkers. + +Adapted from the PR980/926 harness by Gareth Davidson, following Sagar Thakrar's +PR837 harness, and from Sricharan Vagvala's PR967 harness. Apache-2.0. +Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance. +""" +import os +from pathlib import Path +import runpy +import shlex +import struct +import subprocess +import sys + +C = runpy.run_path(str(Path(__file__).with_name("common.py"))) +need, same = C["need"], C["same"] + + +def run(root, words_dir, prices, output): + C["pins"](root) + output = Path(output).resolve() + output.mkdir(parents=True, exist_ok=False) + hub = Path(root).resolve() / C["HUB"] + checker = hub / "code/bit/checkers" + compiler = shlex.split(os.environ.get("CXX", "c++")) + includes = ["-I" + str(hub / "portable-include"), "-I" + str(checker), + "-I" + os.environ.get("BOOST_INCLUDE", "/usr/include")] + commands = [] + + def execute(args, log): + args = [str(x) for x in args] + commands.append(args) + with log.open("x") as stream: + subprocess.run(args, stdout=stream, stderr=subprocess.STDOUT, check=True, + env={k: v for k, v in os.environ.items() if k != "PYTHONOPTIMIZE"}) + + flags = compiler + ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9"] + includes + execute(flags + ["-o", output / "legality", checker / "legality_h.cpp"], output / "compile-legality.log") + for k in (2, 4, 5): + execute(flags + ["-DVPORTS=111", "-DRHELP=439", "-DKPAIRS=" + str(k), + "-o", output / ("columns-" + str(k)), checker / "columns_k.cpp"], + output / ("compile-columns-" + str(k) + ".log")) + # Original exporters contain assertions: keep them enabled even under -O. + python = [sys.executable, "-I", "-B"] + results, nonadd = {}, {} + for label in ("0", "1"): + print("native deferred word", label, flush=True) + folder = output / label + folder.mkdir() + records, cin, cout = (folder / name for name in ("records", "cin", "cout")) + execute(python + [hub / "code/bit/export_records.py", Path(words_dir) / (label + ".json.gz"), records], + folder / "export.log") + execute(python + [hub / "code/bit/regression/stage_cohort.py", records, records, cin, cout], + folder / "stage.log") + execute([output / "legality", cin, cout, cout / "legality.json"], folder / "legality.log") + legality = C["load"](cout / "legality.json") + need(legality["status"] == "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "native legality") + need(legality["copies"] == legality["erasures"] == 9, "native COPY lifetime") + record_rows = list(struct.iter_unpack("<6i", (records / "249-records.bin").read_bytes())) + movements = {} + for row in record_rows: + if row[0] == 0: + movements.setdefault(str(row[1]), []).append(list(row)) + nonadd[label] = {"moves": movements, + "copy_erase": [list(x) for x in record_rows if x[0] in (2, 3)]} + stages = {} + for k in (2, 4, 5): + name = "columns-" + str(k) + execute([output / name, cout / "COHORT249-RECORDS.bin", cout / (name + ".json")], + folder / (name + ".log")) + col = C["load"](cout / (name + ".json")) + expected = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if k == 2 + else "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + need(col["status"] == expected, "native columns") + need(col["formal_columns_checked"] == 2 * k * 111 + 439, "native column coverage") + need(len(col["stages"]) == 2 * k + 1, "native stage coverage") + need(col["bridge_additions"] == 6 * (k - 1) * 111, "native bridge bill") + need(col["fresh_center_copies"] == 9 * (2 * k + 1) + and col["reverse_fresh_center_copies"] == 9 * k, + "native staged COPY bill") + addition_key = "five_stage_additions" if k == 2 else "stage_additions" + need(col[addition_key] == (2 * k + 1) * prices[label]["ADDs"], "all scalar stages billed") + need(col["local_scalar_additions"] == legality["common_frame_ADDs"] == prices[label]["ADDs"], + "native ADD agreement") + need(col["payload_prefix_bits"] == prices[label]["local_bits"] <= 104, "native local precision") + need(int(col["payload_prefix_upper"]) == int(prices[label]["local_upper"]), "native exact local bill") + same([int(x["cancellation_free_signed_row_l1_upper"]) for x in col["signed_lift_prefix"]], + [prices[label]["F"], prices[label]["B"]], "native literal prefix agreement") + controls = col["negative_controls"] + need(len(controls) == 6 * (k - 1) and all(x["rejected"] is True for x in controls), + "native omitted-bridge controls") + stages[str(2 * k + 1)] = {key: col[key] for key in ( + "formal_columns_checked", "bridge_additions", "fresh_center_copies", "reverse_fresh_center_copies", + "signed_lift_prefix", "payload_prefix_bits", "payload_prefix_upper", "local_raw_H", "stages")} + stages[str(2 * k + 1)].update(scalar_ADDs=col[addition_key], controls_rejected=len(controls)) + results[label] = {key: legality[key] for key in ( + "records", "common_frame_ADDs", "rank_mass", "paid_histogram", "copies", "erasures")} + results[label]["staged"] = stages + results[label]["nine_stage_admitted"] = prices[label]["admitted"] + baseline = results["0"] + for label, after in results.items(): + same(nonadd["0"], nonadd[label], "per-register frame path or copy lifetime changed") + need(baseline["records"] - after["records"] == prices["0"]["ADDs"] - prices[label]["ADDs"], "unexpected record delta") + for key in ("rank_mass", "paid_histogram", "copies", "erasures"): + same(baseline[key], after[key], "paid resource changed: " + key) + for stage in ("5", "9", "11"): + same(baseline["staged"][stage]["local_raw_H"], after["staged"][stage]["local_raw_H"], + "local raw ranks changed") + C["write"](output / "commands.json", commands) + C["write"](output / "native-report.json", results) + return results diff --git a/research/r439-deferred-native/test_package.py b/research/r439-deferred-native/test_package.py new file mode 100644 index 0000000000..0d9629c07d --- /dev/null +++ b/research/r439-deferred-native/test_package.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Read-only relocation and source/receipt controls; Apache-2.0, Davidson/Codex.""" +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def tree(root): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + +def main(): + with tempfile.TemporaryDirectory(prefix="deferred-package-") as tmp: + root = Path(tmp) / "export" + package = root / "research/r439-deferred-native" + shutil.copytree(HERE, package) + for row in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if row["usage"] == "input": + dst = root / row["path"] + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], dst) + before = tree(root) + env = dict(os.environ, PYTHONOPTIMIZE="2") + + def run(expected=None): + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=tmp, env=env, capture_output=True, text=True) + if expected: + need(result.returncode != 0 and expected in result.stderr, + "wrong rejection for " + expected + ": " + result.stderr) + else: + need(result.returncode == 0 and "PASS_R439_DEFERRED_FINITE" in result.stdout, + "relocation failed: " + result.stderr) + + files = [p for p in root.rglob("*") if p.is_file()] + dirs = sorted([p for p in root.rglob("*") if p.is_dir()], key=lambda p: len(p.parts), reverse=True) + try: + for p in files: + p.chmod(0o444) + for p in dirs + [root]: + p.chmod(0o555) + run() + need(tree(root) == before, "read-only export changed") + finally: + for p in [root] + list(reversed(dirs)): + p.chmod(0o755) + for p in files: + p.chmod(0o644) + controls = 0 + for path, reason in ((package / "vendor/pr2115/candidate-1188.json.gz", "vendor source hash"), + (root / "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", "source hash")): + raw = path.read_bytes() + try: + path.write_bytes(raw + b"\n") + run(reason) + controls += 1 + finally: + path.write_bytes(raw) + receipt = package / "FINITE.json" + raw = receipt.read_bytes() + try: + changed = json.loads(raw) + changed["directions"] = 2.0 + receipt.write_text(json.dumps(changed)) + run("finite receipt") + controls += 1 + finally: + receipt.write_bytes(raw) + need(tree(root) == before, "corruption control did not restore export") + print(f"PASS_DEFERRED_PACKAGE readonly_git_free_files={len(before)} corruption_controls={controls}") + + +if __name__ == "__main__": + main() diff --git a/research/r439-deferred-native/vendor/pr2115/EXPECTED.json b/research/r439-deferred-native/vendor/pr2115/EXPECTED.json new file mode 100644 index 0000000000..074ede527a --- /dev/null +++ b/research/r439-deferred-native/vendor/pr2115/EXPECTED.json @@ -0,0 +1,7029 @@ +{ + "census": { + "PR1040": { + "ADDs": [ + 11780, + 11348 + ], + "B": [ + 10394084, + 9602408 + ], + "D_runs": [ + [ + "hh", + 221 + ], + [ + "yy", + 307 + ], + [ + "yh", + 111 + ], + [ + "yy", + 307 + ], + [ + "hh", + 221 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 72847, + 72847 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3558, + "cuts_with_target_difference": 2918, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "616732de2383dc406632a1dfce5e7cc111607f88a24e829f8d9e904c0a69134c", + "exporter": { + "base": { + "ADD": 11780, + "B": 10394084, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "b98c9307fe8e2f395cdfa63678d71fc485a61e9e1d523a85fb98badd128a1f6d", + "records": 14709 + }, + "deferred": { + "ADD": 11348, + "B": 9602408, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "d30e9d0d79bcf1f9a256c259e6d6257a93e69cbca1f409c7b59868f8880d28bd", + "records": 14277 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 606, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1110, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 587, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 95, + "prefix_split_argmin": [ + 0 + ], + "prefix_split_cost_full_deferral": 95, + "prefix_split_cost_min": 95, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 0, + "prefix_split_listing_unchanged_for_first_gates": 0, + "prefix_split_points": 308, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 16, + 8, + 4, + 8, + 10, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 92, + [ + 32, + 52, + 53 + ] + ], + "best_by_size": [ + [ + 95, + [] + ], + [ + 94, + [ + 32 + ] + ], + [ + 93, + [ + 32, + 52 + ] + ], + [ + 92, + [ + 32, + 52, + 53 + ] + ], + [ + 92, + [ + 1, + 32, + 52, + 53 + ] + ] + ], + "full_deferral_cost": 95, + "greedy": [ + 92, + [ + 32, + 52, + 53 + ] + ], + "ideals_by_size": [ + 1, + 62, + 1915, + 39313, + 603838 + ], + "minimal_gates": 62, + "size_bound": 4, + "undo_gates": 307 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-target-retune-seed14/candidate.json.gz", + "payload_sha256": "06fab704664b836fb79cc512daf39d684375b4523a1b9b827e3e91a591385dcd", + "preparation_contiguous": true, + "preparation_gates": 307, + "rank_mass": 5129, + "saving": 432, + "scatter_ADDs": [ + 527, + 95 + ], + "selected_profile": true, + "undo_gates": 307 + }, + "PR1047": { + "ADDs": [ + 11769, + 11339 + ], + "B": [ + 10394084, + 9602408 + ], + "D_runs": [ + [ + "hh", + 221 + ], + [ + "yy", + 306 + ], + [ + "hh", + 1 + ], + [ + "yh", + 111 + ], + [ + "hh", + 1 + ], + [ + "yy", + 306 + ], + [ + "hh", + 221 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 72847, + 72847 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3557, + "cuts_with_target_difference": 2916, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "0dd36801391a49f603ac0f3fa3a48b86776d22cd70f70a653dd1af60c6425ba7", + "exporter": { + "base": { + "ADD": 11769, + "B": 10394084, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "da5e33a7bde82fff5c86a42ca633e6bab2218a73a394734a098181c60e67c713", + "records": 14698 + }, + "deferred": { + "ADD": 11339, + "B": 9602408, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "17de64210ef0401ca57ec9d4588f52d247b41a87c74e6bb9210dbab7d95990ed", + "records": 14268 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-post-helper-shear-seed03/candidate.json.gz", + "payload_sha256": "784caecb6e3b5e38efcb7f9bbd3e0973f97edc0889b7c28fad5662c48388eb29", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1062": { + "ADDs": [ + 11500, + 11070 + ], + "B": [ + 5911840, + 5024524 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 236 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 25717, + 25717 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3585, + "cuts_with_target_difference": 2931, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "3a9cba324837a3f486ced7dc2b4df38c0c59b884c1763057194eb13096e9b687", + "exporter": { + "base": { + "ADD": 11500, + "B": 5911840, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "80bb888427eb8bf158dd4279aa56340d20cf573c296f15632b22afabedf0967d", + "records": 14429 + }, + "deferred": { + "ADD": 11070, + "B": 5024524, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "e3ed2ba50aca53620b1dde2f8b9ee68518213639fc6a187084aa5e945f1f86db", + "records": 13999 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 95, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 182, + 181 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "payload_sha256": "62fc64481911bec4c18643c0c6ac7d31091f09c081a9223096839a7150185be8", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1062-composition": { + "ADDs": [ + 11515, + 11085 + ], + "B": [ + 5846566, + 4971904 + ], + "D_runs": [ + [ + "hh", + 221 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 221 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 24625, + 24625 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3555, + "cuts_with_target_difference": 2916, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "6d5ea18989d817fad5d7447c1e54694cef8486a1387dc4f46bd8cb3da9c8e1a4", + "exporter": { + "base": { + "ADD": 11515, + "B": 5846566, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 24625, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "3ef472637d6d99f03bb0b92a88bd5109632b9ddc621362ff1ed49a9b502c3335", + "records": 14444 + }, + "deferred": { + "ADD": 11085, + "B": 4971904, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 24625, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 180, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "e2aa83c7ff8ad6de1ed65c1c636099b33ccf37b52582f1c8875ee50105982200", + "records": 14014 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 95, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 181, + 180 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-bsection-stars-seed01/composition.json.gz", + "payload_sha256": "42ca09ed2996737f9280f27688176ab4401b22600586df0e29f7460528568b55", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1062-pair-control": { + "ADDs": [ + 11715, + 11285 + ], + "B": [ + 5892602, + 5005286 + ], + "D_runs": [ + [ + "hh", + 188 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 188 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 24563, + 24563 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3489, + "cuts_with_target_difference": 2883, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "ac7302160e164c89c5cb2404a111cc5a11dcefd466fda3eed5f451a6f39a7964", + "exporter": { + "base": { + "ADD": 11715, + "B": 5892602, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 24563, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "da348d2ac45dd28670464c7237a89125ae7480397857b16bc1c0303a2892e9b0", + "records": 14644 + }, + "deferred": { + "ADD": 11285, + "B": 5005286, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 24563, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 180, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "45016403d1cabcfd1bb035845dc3a38e3d1377e54dca42aef0ba5fd560873517", + "records": 14214 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 95, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 181, + 180 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-bsection-stars-seed01/pair_control.json.gz", + "payload_sha256": "0bdfccdfa63cdba6b24a52dd06021af7cbf7159bb74b85c020b4a94d18da2e62", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1122": { + "ADDs": [ + 10652, + 10222 + ], + "B": [ + 3910388, + 2996128 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 236 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 15223, + 15223 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3216, + "cuts_with_target_difference": 2562, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "2c4f214a660c03fd45ec133542d86daed50b08391870d33909fba1f72a3b6040", + "exporter": { + "base": { + "ADD": 10652, + "B": 3910388, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 15223, + "MOVE": 2911, + "local_bits": 92, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 176, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "c3b2efc2282db0f5593c35c46c44b70af79e724f77b322637b26dc54e8578d7c", + "records": 13581 + }, + "deferred": { + "ADD": 10222, + "B": 2996128, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 15223, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 174, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "4ad6c661a7677605320276ca6a42d93ee7fd11c9c0463e85607d32a80122fe6a", + "records": 13151 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 92, + 91 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 176, + 174 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-abc-star-composition/candidate.json.gz", + "payload_sha256": "7bbaed96041297cd38e89ff48eb055750cfab36609b9fdbeafcec1b2758c1254", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1188": { + "ADDs": [ + 10492, + 10062 + ], + "B": [ + 3758418, + 2825146 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 236 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 13667, + 13667 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3136, + "cuts_with_target_difference": 2482, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "e7dd976535977adb327cfe03847324eef05f0d76b38bf120a17a79facac495bf", + "exporter": { + "base": { + "ADD": 10492, + "B": 3758418, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 175, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "2df55087c71725651b7fc531323a371810f6c8c6d49d84d2c397bdc2d1862133", + "records": 13421 + }, + "deferred": { + "ADD": 10062, + "B": 2825146, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 173, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "9732a8373b845d090615a39a693dc3c1fdb165777aa9b136f4f86aaac8f90e0c", + "records": 12991 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 91, + 91 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 175, + 173 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-gl5-shortest/candidate.json.gz", + "payload_sha256": "b381d9bc18820b89f92485826ff9f8449d0f72f7599772d52c14e07d6b89b7f2", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1208": { + "ADDs": [ + 10542, + 10112 + ], + "B": [ + 3663878, + 2774762 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 236 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 13721, + 13721 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3162, + "cuts_with_target_difference": 2508, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "8c6117493886d31bb13d055a308b60a0be3d97dee349e8c7004d87fd65cbfe09", + "exporter": { + "base": { + "ADD": 10542, + "B": 3663878, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13721, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 174, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "aeb75254657bc6e326398abcb9696b6076755c7d975a51ed89019cb19605c895", + "records": 13471 + }, + "deferred": { + "ADD": 10112, + "B": 2774762, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13721, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 173, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "3184b0189befdb67ea67bb1ef64d6082aec89afcfcafcfbc559243b747868d8f", + "records": 13041 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 91, + 91 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 526, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 174, + 173 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json", + "payload_sha256": "85df062ca4cdffc17113fe12e32588db91dc950c1ec9a089b59920a3be17e353", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1449": { + "ADDs": [ + 11781, + 11351 + ], + "B": [ + 10394084, + 9602408 + ], + "D_runs": [ + [ + "hh", + 221 + ], + [ + "yy", + 306 + ], + [ + "hh", + 1 + ], + [ + "yy", + 1 + ], + [ + "yh", + 111 + ], + [ + "yy", + 1 + ], + [ + "hh", + 1 + ], + [ + "yy", + 306 + ], + [ + "hh", + 221 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 72847, + 72847 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3560, + "cuts_with_target_difference": 2919, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "a158e2a75389d7ee5647737396f06a8b46f0eb65cc0ba05f4f27ad9e02d356f3", + "exporter": { + "base": { + "ADD": 11781, + "B": 10394084, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "e94864b8dd71f32932a6940ecf232dcb40cc931c6b612cc5330a0424fadbf3bc", + "records": 14710 + }, + "deferred": { + "ADD": 11351, + "B": 9602408, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "77ae47597f80fa9acdc5e760098551fd9a0257cf46de0cfe6d02e1104fbe2dfe", + "records": 14280 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 604, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1083, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 586, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 7, + "prefix_split_listing_unchanged_for_first_gates": 6, + "prefix_split_points": 308, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 32, + 52, + 53 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 32 + ] + ], + [ + 95, + [ + 32, + 52 + ] + ], + [ + 94, + [ + 32, + 52, + 53 + ] + ], + [ + 94, + [ + 0, + 32, + 52, + 53 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 32, + 52, + 53 + ] + ], + "ideals_by_size": [ + 1, + 62, + 1915, + 39315, + 603961 + ], + "minimal_gates": 62, + "size_bound": 4, + "undo_gates": 307 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-neutral-mixed-shears-seed13/candidate.json.gz", + "payload_sha256": "6d58ca3b5cb9f5d77615766995972202cfa75df90d02c85749d202aae86195eb", + "preparation_contiguous": false, + "preparation_gates": 307, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 307 + }, + "PR1543": { + "ADDs": [ + 11489, + 11059 + ], + "B": [ + 5977064, + 5089748 + ], + "D_runs": [ + [ + "hh", + 238 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 238 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 25885, + 25885 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3589, + "cuts_with_target_difference": 2933, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "798b59e1a587f2c77a53cfc46da6a139d209d3e5fc871f297599f626d88318b8", + "exporter": { + "base": { + "ADD": 11489, + "B": 5977064, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25885, + "MOVE": 2911, + "local_bits": 96, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "9ea8c7068d40c57ba2fb54296bcd0ace2f12966f9f394edeaade334fb0910679", + "records": 14418 + }, + "deferred": { + "ADD": 11059, + "B": 5089748, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25885, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "6ebef769d76ee76ec96313413971d48f0b45f793d17715265bcd29f8fe8e9b77", + "records": 13988 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 96, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 182, + 181 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-neutral-helper-chain-seed17/CANDIDATE.json.gz", + "payload_sha256": "ae112d1ee2fc6ef9f077a107a0e8ddeec8aaeaec6d88eee28e7272a7562937b7", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1709": { + "ADDs": [ + 11488, + 11058 + ], + "B": [ + 5921344, + 5034028 + ], + "D_runs": [ + [ + "hh", + 241 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 241 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 27061, + 27061 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3595, + "cuts_with_target_difference": 2936, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "5d18a3bb696dbad029fd9eeaa7cbfdcc120ea6cfdd4aba2e8cc34aaee733a277", + "exporter": { + "base": { + "ADD": 11488, + "B": 5921344, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 27061, + "MOVE": 2911, + "local_bits": 96, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "10de6f93ba0dcf14aaeb0bfeaea0e35f65ad5ba22de6284fe2828a7ee0504930", + "records": 14417 + }, + "deferred": { + "ADD": 11058, + "B": 5034028, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 27061, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "20745d9535ffab56e1fc54ed3a5e6a732daa310f84fdd478ee082ea21fbc489b", + "records": 13987 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 96, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 182, + 181 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-five-cycle-seed9f01/CANDIDATE.json.gz", + "payload_sha256": "b19f7c71997e5d402003b62c7083fc115fec931344ead2667d4e736e0008be2b", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1868-1062": { + "ADDs": [ + 11497, + 11067 + ], + "B": [ + 5858638, + 4976508 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 233 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 25717, + 25717 + ], + "T_is_identity": false, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": null, + "base_D_operator_equals_PR589_D": false + }, + "bridge": { + "cuts": 3582, + "cuts_with_target_difference": 2928, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "73a3285e2691a0e985dc0096b158df67f4275ff01fe77feaab2019b41f580d22", + "exporter": { + "base": { + "ADD": 11497, + "B": 5858638, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 182, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "c44b7709940a9256293cbd21a29e819382426ea15c02b90b0d39ca096bc53620", + "records": 14426 + }, + "deferred": { + "ADD": 11067, + "B": 4976508, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 25717, + "MOVE": 2911, + "local_bits": 95, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 181, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "b1d5e7ae1f5c0bfc519950a32aee3ad740d6ca34e280e06100f0fef8fa75bc77", + "records": 13996 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 95, + 95 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 182, + 181 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "K_equals_D", + "C_is_U_inverse" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "H5_V_identity", + "K_equals_D", + "C_is_U_inverse" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-twisted-star-absorption-seed02/absorbed-pr1062.json.gz", + "payload_sha256": "b6b2acfc7293ac1910fdf8b087ab62f002809eaec7760b7dcaae9aa754738062", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR1868-1188": { + "ADDs": [ + 10489, + 10059 + ], + "B": [ + 3748680, + 2816834 + ], + "D_runs": [ + [ + "hh", + 236 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 233 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 13667, + 13667 + ], + "T_is_identity": false, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": null, + "base_D_operator_equals_PR589_D": false + }, + "bridge": { + "cuts": 3133, + "cuts_with_target_difference": 2479, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "73c0d1713d5ceec20e0cee68f20973801ba3a50481ab0965269c6d0d46f4d18b", + "exporter": { + "base": { + "ADD": 10489, + "B": 3748680, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 175, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "2b4da8c826c816b58ea05f1b2906df46379e20da8d1e2bbd7e84430d99f0973f", + "records": 13418 + }, + "deferred": { + "ADD": 10059, + "B": 2816834, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 13667, + "MOVE": 2911, + "local_bits": 91, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 173, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "1fad8a002101d6ec04adc8b08502973f229608733c69a13faba8cb7374672fb2", + "records": 12988 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": false, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 91, + 91 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 527, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 175, + 173 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "K_equals_D", + "C_is_U_inverse" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H4_C_literal_reverse_at_full", + "H5_V_identity", + "K_equals_D", + "C_is_U_inverse" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-twisted-star-absorption-seed02/absorbed-pr1188.json.gz", + "payload_sha256": "72a28b93811e7f175dd824079f776dfde41eda7482bb86db01e153d84cff3931", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR915": { + "ADDs": [ + 13208, + 12778 + ], + "B": [ + 9534616, + 8742940 + ], + "D_runs": [ + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 49347, + 49347 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3113, + "cuts_with_target_difference": 2695, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "562e69a98dfb9cea8abe3bcdf97ce7d4854ea09cf10b0b172416fd0966ed24b2", + "exporter": { + "base": { + "ADD": 13208, + "B": 9534616, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 49347, + "MOVE": 2911, + "local_bits": 100, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 189, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "c8f0b1a067b94fcf10096df2758c1e943dd4f30ace9d3629cf8e20d19bed05cf", + "records": 16137 + }, + "deferred": { + "ADD": 12778, + "B": 8742940, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 49347, + "MOVE": 2911, + "local_bits": 99, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 189, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "770185daf2047ecb40d0ef5bc1441c22acffd38a4e7ff19607b58498ca4471aa", + "records": 15707 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 100, + 99 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 189, + 189 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-target-compensation/candidate.json.gz", + "payload_sha256": "6aec2c6f91c87a7440af10cdeb90b8814501224a86de14d4033ae3ffa00899da", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR926": { + "ADDs": [ + 11980, + 11550 + ], + "B": [ + 10562318, + 9770642 + ], + "D_runs": [ + [ + "hh", + 192 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 192 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 71907, + 71907 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3497, + "cuts_with_target_difference": 2887, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "a1398b11bb59033df2c395a3dd815f6588d8e46a3bafe4b4f0c4214303c0f1c7", + "exporter": { + "base": { + "ADD": 11980, + "B": 10562318, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 71907, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "1c93cd7f1d3a0971e30289eef4a1334a059a867a4f469095952bfb9de3b9f411", + "records": 14909 + }, + "deferred": { + "ADD": 11550, + "B": 9770642, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 71907, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "3240b377ab4507a7ac9e51f6cedcf456d72d73890bf5f32759f11ebed662dcf5", + "records": 14479 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-two-sided-compensation/candidate.json.gz", + "payload_sha256": "fdb1a0dfafe5392e01fb87f5813737db0f15682c5cb98fc224d4d4cdbc806dd2", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR941": { + "ADDs": [ + 11949, + 11519 + ], + "B": [ + 10548832, + 9757156 + ], + "D_runs": [ + [ + "hh", + 199 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 199 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 70083, + 70083 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3511, + "cuts_with_target_difference": 2894, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "8d8e2dcfecfe189f7f69347adc549e7a3bf0b6bd610307911aadadb7f9277b36", + "exporter": { + "base": { + "ADD": 11949, + "B": 10548832, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 70083, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "a03df32b8d6eed87f5037c2b28f600125dd30206f57e5ba9ea8ff78d3a9a2c22", + "records": 14878 + }, + "deferred": { + "ADD": 11519, + "B": 9757156, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 70083, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "b2dddda5fcb13b8183582f4a2463c1152eb2fdc9c2653d20f31b030c88c987bc", + "records": 14448 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 101, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-helper-matching/candidate.json.gz", + "payload_sha256": "06808b6a98689bba6095fd96c0602fa585dc114bf33073f30acce34b1fdff18d", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR941-floor": { + "ADDs": [ + 11948, + 11518 + ], + "B": [ + 10518760, + 9727084 + ], + "D_runs": [ + [ + "hh", + 199 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 199 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 73603, + 73603 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3511, + "cuts_with_target_difference": 2894, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "d1753c7837e3e8e3021d363feefcea306dbe7233e78a5d2e8ad758f22f095832", + "exporter": { + "base": { + "ADD": 11948, + "B": 10518760, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 73603, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": false, + "nine_stage_bits": 193, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "c4be2f74266fdc752f87f2ca1e52b5764f6c487be486720a58c83ee3989ca82d", + "records": 14877 + }, + "deferred": { + "ADD": 11518, + "B": 9727084, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 73603, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "74be8438db4a4ff22a99f6670582c5ec03fad9cbcf52a558be76574ac97c811a", + "records": 14447 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 193, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-helper-matching/floor-word.json.gz", + "payload_sha256": "8948c509341735070c46de5ecb723f8e4294c22b14470ad7c3140875ab10971f", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR965": { + "ADDs": [ + 11840, + 11410 + ], + "B": [ + 10464656, + 9672980 + ], + "D_runs": [ + [ + "hh", + 234 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 234 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 72399, + 72399 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3581, + "cuts_with_target_difference": 2929, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "e81c9cbe701005a08a2249a08cdf417284bfa7239cc03cfdf18d1fda33c27a22", + "exporter": { + "base": { + "ADD": 11840, + "B": 10464656, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72399, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "4283f1d5d6157b5bcf23f58204e4c73488dfffe0954c7e41379f4df3c01a4386", + "records": 14769 + }, + "deferred": { + "ADD": 11410, + "B": 9672980, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72399, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "06b65800e5736adcc03874796b844857968ed1d4ab6ff2a23bee82097229364c", + "records": 14339 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-helper-triples/candidate.json.gz", + "payload_sha256": "03016658f28ad8d53eba99c6a6bf4db8f6812200e978b4dfa15e74577ef612ee", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + }, + "PR967": { + "ADDs": [ + 11783, + 11353 + ], + "B": [ + 10394084, + 9602408 + ], + "D_runs": [ + [ + "hh", + 221 + ], + [ + "yy", + 306 + ], + [ + "yh", + 111 + ], + [ + "yy", + 306 + ], + [ + "hh", + 221 + ] + ], + "ES_nonzero_rows": 55, + "F": [ + 72847, + 72847 + ], + "T_is_identity": true, + "anchor": { + "PR589_D_splice_passes_every_owner_flag": true, + "base_D_operator_equals_PR589_D": true + }, + "bridge": { + "cuts": 3555, + "cuts_with_target_difference": 2916, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_sha256": "7a1d1b93ffb24a85f1eb598e8b8ee2b84716d7840cfe3ea2b16d14052af627ef", + "exporter": { + "base": { + "ADD": 11783, + "B": 10394084, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 102, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "4970411c56f2c7f7463c70f28d17c4bc517175b12259e7b5c4063e37c2abd856", + "records": 14712 + }, + "deferred": { + "ADD": 11353, + "B": 9602408, + "COPY": 9, + "COPY_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "ERASE": 9, + "F": 72847, + "MOVE": 2911, + "local_bits": 101, + "local_ok": true, + "nine_ok": true, + "nine_stage_bits": 192, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "record_sha256": "5c2cfb93680db6a02a4a6822a8dc3e3c744d9bcc7ee1e54339c1620628220cbf", + "records": 14282 + } + }, + "h5tw": { + "base": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": true, + "R_offdiagonal_ones": 0, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": true, + "V_offdiagonal_ones": 0, + "final_targets_y_plus_x": true + }, + "deferred": { + "C_Uprime_T_identity": true, + "C_full_frame_z_only": true, + "D_frame_zero": true, + "D_source_free": true, + "D_sources_identity": true, + "D_targets_no_source_column": true, + "J_identity": true, + "R_invertible": true, + "R_is_identity": false, + "R_offdiagonal_ones": 608, + "T_helper_only": true, + "T_invertible": true, + "T_is_identity": true, + "U_block_form": true, + "VN_equals_KprimeT": true, + "VR_identity": true, + "V_is_identity": false, + "V_offdiagonal_ones": 1104, + "final_targets_y_plus_x": true + } + }, + "local_bits": [ + 102, + 101 + ], + "maximality": { + "B_target_block_identity": true, + "B_target_write_frames_shared_by_another_target_path": 0, + "B_target_writes": 213, + "B_target_writes_at_zero": 0, + "B_target_writes_reading_targets": 0, + "absorption_pairs": 585, + "absorption_pairs_frame_legal": 0, + "first_B_target_climb_index": 0, + "first_B_touch_of_every_target_climbs": true, + "per_column_choice_total": 97, + "prefix_split_argmin": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6 + ], + "prefix_split_cost_full_deferral": 97, + "prefix_split_cost_min": 97, + "prefix_split_cost_no_deferral": 527, + "prefix_split_cost_unchanged_for_first_gates": 6, + "prefix_split_listing_unchanged_for_first_gates": 5, + "prefix_split_points": 307, + "relaxed_paths": { + "current": { + "max_partners": 55, + "writes_with_a_partner": 102 + }, + "loose": { + "max_partners": 58, + "writes_with_a_partner": 102 + }, + "monotone": { + "max_partners": 7, + "writes_with_a_partner": 94 + } + }, + "scatter_column_ones_new": [ + 17, + 17, + 8, + 4, + 8, + 11, + 13, + 6, + 13 + ], + "scatter_column_ones_old": [ + 63, + 55, + 55, + 55, + 63, + 63, + 55, + 55, + 63 + ], + "target_nonzero_frame_sets_pairwise_disjoint": true, + "target_pairs_sharing_a_nonzero_frame": 0, + "undo_latest_B_index_max": 661, + "undo_latest_B_index_min": 0, + "undo_operands": 111 + }, + "nine_stage_bits": [ + 192, + 192 + ], + "order_ideals": { + "best": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "best_by_size": [ + [ + 97, + [] + ], + [ + 96, + [ + 31 + ] + ], + [ + 95, + [ + 31, + 51 + ] + ], + [ + 94, + [ + 31, + 51, + 52 + ] + ], + [ + 94, + [ + 0, + 31, + 51, + 52 + ] + ] + ], + "full_deferral_cost": 97, + "greedy": [ + 94, + [ + 31, + 51, + 52 + ] + ], + "ideals_by_size": [ + 1, + 61, + 1854, + 37461, + 566500 + ], + "minimal_gates": 61, + "size_bound": 4, + "undo_gates": 306 + }, + "owner_false_base": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D" + ], + "owner_false_deferred": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "path": "research/r439-helper-stars-seed19/candidate.json.gz", + "payload_sha256": "82521d616fb9cd3b57576678e1b9de67c8587c7d0b8ed8d87a1405c5a684c3ae", + "preparation_contiguous": true, + "preparation_gates": 306, + "rank_mass": 5129, + "saving": 430, + "scatter_ADDs": [ + 527, + 97 + ], + "selected_profile": true, + "undo_gates": 306 + } + }, + "check_controls": [ + [ + "precision guard on the PR941 floor-calibration base word (193 nine-stage bits)", + "PR941-floor base: precision guard (exporter F/B)" + ] + ], + "columns": 661, + "controls": { + "PR1062": [ + [ + "deferral with the old scatter listing S", + "dirty endpoint wrong on 111 registers {'target': 111}; failed equations ['J_identity', 'VN_equals_KprimeT']" + ], + [ + "undo moved after B[0], the first B climb of an undo operand (frames)", + "illegal frame move: register 111 frame 127 -> 0" + ], + [ + "undo moved after B[0] (values, frames ignored)", + "dirty endpoint wrong on 28 registers {'target': 28}" + ], + [ + "first undo gate dropped", + "dirty endpoint wrong on 6 registers {'target': 6}; failed equations ['VR_identity', 'VN_equals_KprimeT']" + ], + [ + "undo gates in preparation order", + "dirty endpoint wrong on 111 registers {'target': 111}; failed equations ['VR_identity', 'J_identity', 'VN_equals_KprimeT']" + ], + [ + "E S row 1 with bit 0 flipped", + "dirty endpoint wrong on 6 registers {'target': 6}; failed equations ['J_identity', 'VN_equals_KprimeT']" + ], + [ + "corrupted source pin", + "source pin mismatch (sha256): research/r439-bsection-stars-seed01/candidate.json.gz" + ], + [ + "adjacent non-commuting undo gates 7,8 swapped", + "dirty endpoint wrong on 24 registers {'target': 24}; failed equations ['VR_identity', 'VN_equals_KprimeT']" + ], + [ + "bridge on the deferred word with its last D gate dropped", + "bridge: the deferred word D/A differ from the replayed steps" + ], + [ + "bridge on the old-S word", + "bridge: target 1 is not the tracked twist of the original" + ], + [ + "bridge on the swapped-undo word", + "bridge: the twist is not undone" + ], + [ + "owner delta on (base, base)", + "PR1062: owner flags newly false [], newly true []" + ], + [ + "frame paths: legal frame raise of B[500] 508 -> 422", + "PR1062: ordered per-register frame paths changed" + ], + [ + "paid profile: legal frame raise of B[500] 508 -> 422", + "PR1062: paid profile changed" + ], + [ + "exporter profile against the frame-raised profile", + "PR1062: exporter profile differs from the frame-path profile" + ], + [ + "maximality census with the deferred word as its own base", + "PR1062: maximality census" + ] + ], + "PR1188": [ + [ + "deferral with the old scatter listing S", + "dirty endpoint wrong on 111 registers {'target': 111}; failed equations ['J_identity', 'VN_equals_KprimeT']" + ], + [ + "undo moved after B[0], the first B climb of an undo operand (frames)", + "illegal frame move: register 111 frame 127 -> 0" + ], + [ + "undo moved after B[0] (values, frames ignored)", + "dirty endpoint wrong on 28 registers {'target': 28}" + ], + [ + "first undo gate dropped", + "dirty endpoint wrong on 6 registers {'target': 6}; failed equations ['VR_identity', 'VN_equals_KprimeT']" + ], + [ + "undo gates in preparation order", + "dirty endpoint wrong on 111 registers {'target': 111}; failed equations ['VR_identity', 'J_identity', 'VN_equals_KprimeT']" + ], + [ + "E S row 1 with bit 0 flipped", + "dirty endpoint wrong on 6 registers {'target': 6}; failed equations ['J_identity', 'VN_equals_KprimeT']" + ], + [ + "corrupted source pin", + "source pin mismatch (sha256): research/r439-gl5-shortest/candidate.json.gz" + ], + [ + "adjacent non-commuting undo gates 7,8 swapped", + "dirty endpoint wrong on 24 registers {'target': 24}; failed equations ['VR_identity', 'VN_equals_KprimeT']" + ], + [ + "bridge on the deferred word with its last D gate dropped", + "bridge: the deferred word D/A differ from the replayed steps" + ], + [ + "bridge on the old-S word", + "bridge: target 1 is not the tracked twist of the original" + ], + [ + "bridge on the swapped-undo word", + "bridge: the twist is not undone" + ], + [ + "owner delta on (base, base)", + "PR1188: owner flags newly false [], newly true []" + ], + [ + "frame paths: legal frame raise of B[500] 508 -> 422", + "PR1188: ordered per-register frame paths changed" + ], + [ + "paid profile: legal frame raise of B[500] 508 -> 422", + "PR1188: paid profile changed" + ], + [ + "exporter profile against the frame-raised profile", + "PR1188: exporter profile differs from the frame-path profile" + ], + [ + "maximality census with the deferred word as its own base", + "PR1188: maximality census" + ] + ] + }, + "ideal_split": { + "PR1040": { + "ADDs": [ + 11780, + 11348, + 11345 + ], + "B": 9602408, + "F": 72847, + "bridge": { + "cuts": 3558, + "cuts_with_target_difference": 2918, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_to_B": 304, + "kept_before_scatter": 3, + "kept_undo_gates": [ + 32, + 52, + 53 + ], + "label": "found by search (exhaustive over ideals of size <= 4 plus greedy descent), not optimal", + "local_bits": 101, + "nine_stage_bits": 192, + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "scatter_ADDs": [ + 527, + 95, + 92 + ], + "word_sha256": "b95bec07e83a67a861b0e05c81aaf07e9dc56239db77983f484ce16866f8a48f" + }, + "PR1062": { + "ADDs": [ + 11500, + 11070, + 11067 + ], + "B": 5024524, + "F": 25717, + "bridge": { + "cuts": 3585, + "cuts_with_target_difference": 2931, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_to_B": 303, + "kept_before_scatter": 3, + "kept_undo_gates": [ + 31, + 51, + 52 + ], + "label": "found by search (exhaustive over ideals of size <= 4 plus greedy descent), not optimal", + "local_bits": 95, + "nine_stage_bits": 181, + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "scatter_ADDs": [ + 527, + 97, + 94 + ], + "word_sha256": "5b7ce519bb3a93987bdbfeddcc15699dae436652d9da837dadbbcec2d834df6f" + }, + "PR1188": { + "ADDs": [ + 10492, + 10062, + 10059 + ], + "B": 2825146, + "F": 13667, + "bridge": { + "cuts": 3136, + "cuts_with_target_difference": 2482, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_to_B": 303, + "kept_before_scatter": 3, + "kept_undo_gates": [ + 31, + 51, + 52 + ], + "label": "found by search (exhaustive over ideals of size <= 4 plus greedy descent), not optimal", + "local_bits": 91, + "nine_stage_bits": 173, + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "scatter_ADDs": [ + 527, + 97, + 94 + ], + "word_sha256": "3cadbce5c79d65f18183bb97f64d972099e73a1635f897215085f0a32e781187" + }, + "PR1868-1188": { + "ADDs": [ + 10489, + 10059, + 10056 + ], + "B": 2816834, + "F": 13667, + "bridge": { + "cuts": 3133, + "cuts_with_target_difference": 2479, + "max_targets_differing": 111, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "deferred_to_B": 303, + "kept_before_scatter": 3, + "kept_undo_gates": [ + 31, + 51, + 52 + ], + "label": "found by search (exhaustive over ideals of size <= 4 plus greedy descent), not optimal", + "local_bits": 91, + "nine_stage_bits": 173, + "owner_newly_false": [ + "H5_V_identity" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "scatter_ADDs": [ + 527, + 97, + 94 + ], + "word_sha256": "23f1912469a34f27372761ee40c439cea19fff39925bd70c505bec723c0dbf07" + } + }, + "inputs": { + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/e8-bit-p111/data/bitE8mut-p111.json.gz": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858", + "research/r439-abc-star-composition/candidate.json.gz": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066", + "research/r439-abc-zrewrite-seed16/CANDIDATE-WORD.json": "66b34404f39f5f612c2aaadd53ae33eb9f5993ec2065c82e23d7467cce03a226", + "research/r439-b509-boolean-seed05/candidate.json.gz": "14b8bde5e0b3171795574e3f52046b0e53b5c994a5af5aa77ce0485d69a82687", + "research/r439-bsection-stars-seed01/candidate.json.gz": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee", + "research/r439-bsection-stars-seed01/composition.json.gz": "0203fea9fa442ca206fe683aa5b6860adac680d63b9fb8be6bd42b39aa7b5cce", + "research/r439-bsection-stars-seed01/pair_control.json.gz": "628ebfebe215e153338e88e2e324040d139a111eebfb090929697c7a0b6f3f59", + "research/r439-five-cycle-seed9f01/CANDIDATE.json.gz": "286fb2e8b397909bd74257ef911b4a76a633e169493d481a9ca40379ae9072b9", + "research/r439-five-wire-prefix/candidate.json.gz": "3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091", + "research/r439-four-wire-prefix/candidate.json.gz": "9946eaacc69f05a91ad18ca16e57cd4f78db3e0d5b23939f691c96b4a4098a2f", + "research/r439-gl5-shortest/candidate.json.gz": "4e7904d01ebdbfc60a26472b4e0d2e813c19c2fe1a4bb8ab390c12746a1da359", + "research/r439-global-prefix-admission/candidate.json.gz": "fffc0484a3572c76bf3bb5284d4a40eeb723c4b3acf3da5e2d9e113ac1747ec6", + "research/r439-helper-matching/candidate.json.gz": "60531408445a1d7c793dff6821e767739012db1d2646f49aec7fdf7fe0b979f3", + "research/r439-helper-matching/floor-word.json.gz": "4be50c06f91bc605660d4f9fba865c330f82dc4c364041870b725c220d16244e", + "research/r439-helper-stars-seed19/candidate.json.gz": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8", + "research/r439-helper-triples/candidate.json.gz": "11f5c75711090892827d536b6bf82b4001e02ebd13d10e87a1aa915a4e78704b", + "research/r439-neutral-helper-chain-seed17/CANDIDATE.json.gz": "559f948dc9f7474e314b27d70286025b21922e3f7a6fbd93b7786cc0f6a871b5", + "research/r439-neutral-mixed-shears-seed13/candidate.json.gz": "845ee7205390e8b5252187051839304c1eae197006cf80fdc9ec156d50916834", + "research/r439-post-helper-shear-seed03/candidate.json.gz": "e6a7a50662ba2c32c7fb42d7051d1300bef52f8e442f593c0081999bc0c27934", + "research/r439-six-wire-boolean/candidate.json.gz": "5c67c7949c07a89ea8394a936a155585d22e6b258997df73e36e7be47fc84cb0", + "research/r439-target-compensation/candidate.json.gz": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e", + "research/r439-target-retune-seed14/candidate.json.gz": "908f285b69b70cc998718575706b48091e856d96f23e3267060dca7a7546ac50", + "research/r439-twisted-star-absorption-seed02/absorbed-pr1062.json.gz": "38af2e18956a3f6111ddde59da59fd9ca14c7fdbe589f718056ff66a51ecd963", + "research/r439-twisted-star-absorption-seed02/absorbed-pr1188.json.gz": "0d24063702f353cf30466077ac7bc88ed19baabfade80002fafa7edcc14302e7", + "research/r439-two-sided-compensation/candidate.json.gz": "6ac771545e823c054e005429c405dbb2c01ff80fce181b714e1af5e28b6b7cb2", + "research/r439-z3to2-seed13/CANDIDATE-WORD.json": "8aedb3be192baae884c80a2ff3d15d9f32ae8c8055dff170bebca2f87e75539a" + }, + "instances": { + "PR1062": { + "file": "candidate-1062.json.gz", + "payload_sha256": "3a9cba324837a3f486ced7dc2b4df38c0c59b884c1763057194eb13096e9b687" + }, + "PR1188": { + "file": "candidate-1188.json.gz", + "payload_sha256": "e7dd976535977adb327cfe03847324eef05f0d76b38bf120a17a79facac495bf" + } + }, + "new_kappa_claim": false, + "outside": { + "PR1127": { + "ADDs": 23495, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-z3to2-seed13/CANDIDATE-WORD.json", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR1221": { + "ADDs": 24283, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-b509-boolean-seed05/candidate.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR555": { + "ADDs": 24305, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/e8-bit-p111/data/bitE8mut-p111.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR589": { + "ADDs": 24305, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR904": { + "ADDs": 24051, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-four-wire-prefix/candidate.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR936": { + "ADDs": 23711, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-five-wire-prefix/candidate.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR952": { + "ADDs": 23673, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-six-wire-boolean/candidate.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + }, + "PR980": { + "ADDs": 23433, + "D_runs": [ + [ + "yh", + 111 + ] + ], + "deferral": "vacuous (R = I)", + "path": "research/r439-global-prefix-admission/candidate.json.gz", + "scatter_ADDs": 527, + "target_basis_gates": 0 + } + }, + "reorder": { + "PR1062": { + "adjacent_transpositions": 305, + "commuting": 270, + "commuting_swap_boundary_exact": true, + "commuting_swap_checked": [ + 0, + 1 + ], + "non_commuting": 35, + "operator_changes_iff_non_commuting": true + }, + "PR1188": { + "adjacent_transpositions": 305, + "commuting": 270, + "commuting_swap_boundary_exact": true, + "commuting_swap_checked": [ + 0, + 1 + ], + "non_commuting": 35, + "operator_changes_iff_non_commuting": true + } + }, + "selected_heuristic": { + "ADDs": [ + 24305, + 24190 + ], + "B": [ + 1113070, + 1117988 + ], + "F": [ + 49347, + 49347 + ], + "basis_gates_each_way": 79, + "bridge": { + "cuts": 2353, + "cuts_with_target_difference": 2241, + "max_targets_differing": 79, + "states_equal_after_undo": true, + "z_reads_of_targets_in_window": 0 + }, + "local_bits": [ + 93, + 93 + ], + "method": "Prim minimum spanning tree over the 111 scatter rows plus a zero root, edge cost 2 + Hamming distance; scatter basis G (R = G, V = G^-1); heuristic, not optimal", + "nine_stage_bits": [ + 177, + 177 + ], + "owner_false": [ + "H2_D_frame0_targets_from_helpers", + "H5_V_identity", + "K_equals_D" + ], + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "roots": 32, + "scatter_ADDs": [ + 527, + 254 + ], + "scatter_related_cost": 412, + "tree_edges": 79, + "word_sha256": "85c9c49b558a9aae2c02966d674009e0d910e67ba52690c84bc89791ae843f21" + }, + "status": "PASS_R439_DEFERRED_TARGET_BASIS" +} diff --git a/research/r439-deferred-native/vendor/pr2115/PROOF.md b/research/r439-deferred-native/vendor/pr2115/PROOF.md new file mode 100644 index 0000000000..a4e52fd2ba --- /dev/null +++ b/research/r439-deferred-native/vendor/pr2115/PROOF.md @@ -0,0 +1,462 @@ +# Deferred target basis (H5-tw): proofs + +This note proves four statements and records one refinement: + +1. the replacement lemma H5-tw, with its converse; +2. that deferring the target-basis undo turns every lineage word into a word meeting H5-tw, with a + unique scatter listing; +3. the cut-by-cut bridge, with an argued physical reading that needs no premise beyond those the base + words already use; +4. maximality of the deferral under fixed ordered frame paths, among prefix splits of the literal undo + order; +5. the order-ideal refinement: splitting the undo at a commutation-closed down-set. On every word the + search finds a split three scatter ADDs below full deferral, and the split is fully checked on + four words. It is found by search and is not claimed optimal. + +`verify.py` checks every finite fact used here, on every committed lineage word (as of base +c6765481). + +## Notation + +A word has `n = 2v + r` registers: sources `x` (v of them), targets `y` (v) and helpers `h` (r). +Write `z = (x, h)`. Here `v = 111`, `r = 439` and `n = 661`. The word runs D, then A, then the +scatter, then B, then C. The scatter is realised literally: COPY one retained helper into a clean +temporary at the zero frame, ADD that temporary into the listed targets, then ERASE it. Each ADD +`d ^= s` is an elementary transvection over F2. + +As in PR1868, a finite product of transvections acts on `M^n` for any F2-module M through its F2 +coefficient matrix. "Boundary" means the complete coefficient matrix on all 661 columns, with +arbitrary ("dirty") helper inputs. + +The kept clauses come from the inherited interleaved lemma. eumemic's PR543 states it (restated in +`research/e8-bit-r420/README.md`), and eumemic's PR555 adaptation `xcheck_p.py` checks it: + +- **H1**: no gate whose destination is a z register reads a target. +- **H3**: A writes only z registers. The scatter reads only retained helpers and writes only targets. + Each B gate either writes a z register from z registers, or writes a target (from any sources). +- **C clause**: every C gate has a z destination, reads only z registers and runs at the full frame. +- **D-shape** (the structural part of H2, as in PR1194 and PR1868): every D gate is at the zero frame + and reads and writes only targets and helpers. D contains no COPY, ERASE or climb. + +By H1 no helper gate in D reads a target, so D's operator has the form + + (x, y, h) -> (x, R y + N h, T h) + +for a v-by-v matrix R, a v-by-r matrix N and an r-by-r matrix T. By H1 and H3 the raw word +`W0' = (A, scatter, B)` has the block form + + z' = U' z, y' = V y + J x + K' h. + +The inherited H2 target clause is `R = I`: D adds to the targets without changing their basis. This +is also PR1194's "complete restoration of every target basis at D's boundary". The inherited H5 is +`V = I`. + +## 1. The replacement lemma H5-tw + +**Contract H5-tw.** Keep H1, H3, the C clause and the D-shape. Replace the pair (H2 target clause +`R = I`, H5 `V = I`) and the K check by: + + (i) V R = I, + (ii) J = I, + (iii) V N = K' T, + (iv) C U' (I_x ⊕ T) = I on z. + +**Lemma.** Under the kept clauses, the complete word maps `(x, y, h) -> (x, y + x, h)` on every +F2-module if and only if (i)–(iv) hold. + +*Proof.* D sends `(x, y, h)` to `(x, R y + N h, T h)`. Applying `W0'` gives + + z' = U' (x, T h) = U' (I ⊕ T) z, + y' = V (R y + N h) + J x + K' T h = V R y + J x + (V N + K' T) h. + +C reads and writes only z registers, so it leaves y unchanged and sends z' to `C U' (I ⊕ T) z`. +The final state is therefore + + (z, y) -> (C U' (I ⊕ T) z, V R y + J x + (V N + K' T) h). + +If (i)–(iv) hold, this is `(z, y + x)`, since `V N + K'T = 0` over F2. Every coefficient lies in F2, +so the identity holds on every M. + +Conversely, suppose the boundary `(x, y, h) -> (x, y + x, h)` holds. Evaluate on the F2 unit columns: + +- the target rows on the target columns give `V R = I`; +- the target rows on the source columns give `J = I`; +- the target rows on the helper columns give `V N + K'T = 0`; +- the z rows give `C U' (I ⊕ T) = I`. ∎ + +**Remarks.** + +- **Invertibility.** `V R = I` forces R and V to be invertible, with `V = R^-1`. +- **The inherited case.** With `R = I`, (i) is H5, so the inherited contract is the case `R = V = I`. + - (iii) with `V = T = I` is PR1194's `N = K`. + - (iii) with `V = I` and general T is PR1868's K-tw. +- **The cleanup (iv).** + - Under the literal H4 (C is the reversed list of z-gates of A and B), `C = U'^-1`, so (iv) holds if + and only if `T = I`. + - PR1868's H4-tw is (iv) itself. + - So the converse proves (iv) from the boundary; it is not assumed through the C clause, which only + fixes C's shape. +- **The listing is unique.** The scatter listing is determined by the rest of the word. Suppose a word + keeps D, A, B and C and changes only the listing, from L to L'. + - The retained totals are nine distinct registers of an invertible state, so their columns c are + linearly independent. + - The final targets change by `V_B (L' + L) c`, where `V_B` is the invertible target block of + everything between the scatter and the end. + - So L is the only listing that meets the boundary. + +## 2. The deferral meets H5-tw + +**Shape of the lineage words.** Every committed PR915-lineage word has a D section of the form + + helper-star preparations, P_E, reads, U_E, helper restorations. + +- `P_E` is the target-basis preparation: 306 target-from-target gates (307 on PR1040 and PR1449). + Its product is E. +- The reads are 111 gates, target-from-helpers. +- `U_E` is the undo: exactly `P_E` reversed, gate by gate, so its product is `E^-1`. + +All of these gates are at the zero frame. There are small layout variations: + +- the helper parts are empty on PR915's word; +- on PR1047 and PR1449 one helper gate sits on each side of the reads; +- on PR1449 the preparation is not contiguous. + +The argument only uses three facts: + +- the target gates before the first read are exactly `P_E`; +- the target gates after the last read are exactly `U_E`; +- no target-from-target gate sits among the reads. + +`verify.py` checks all three on every word. + +**The base word W.** W satisfies the inherited target clauses `R = I` and `V = I`. Let the reads add +`M h~` to the targets, where `h~ = T_s h` is the helper state at the reads and `T_s` is the +helper-star preparation. Then W's D target operator is + + y -> E^-1 (E y + M T_s h) = y + N h, N = E^-1 M T_s. + +W also satisfies (iii) and (iv): + +- the 17 words with `T = I` satisfy PR1194's `N = K`, with literal H4; +- PR1868's two absorbed words satisfy its K-tw and H4-tw. + +**The deferred word W'.** W' makes three changes: + +- it deletes `U_E` from D; +- it replaces the scatter listing S (rows over the nine retained totals) by `E S`; +- it runs the same `U_E` gates, at the zero frame, as the first gates of B. + +**The deferred word's blocks.** + +- *D.* D' is D without `U_E`. Its target operator is `y -> E y + M T_s h = E (y + N h)`, so + `R' = E`, `N' = E N` and `T' = T`. +- *Up to the undo.* A does not touch targets (H1, H3). The scatter adds `E S c`, where c holds the + nine COPY values (functions of z only). The undo then maps the targets by `E^-1`. So after the undo + the targets hold `E^-1 y + S c`, exactly what W's targets hold after its own scatter on input + `E^-1 y`. B is unchanged. +- *The raw word.* Hence `W0''(y) = W0(E^-1 y)`, which gives `V'' = V E^-1 = E^-1`, `J'' = J = I`, + `K'' = K'` and `U'' = U'`. + +Therefore: + + V'' R' = E^-1 E = I, + V'' N' = E^-1 E N = N = K' T, + J'' = I, + +and C, U' and T are unchanged, so (iv) is inherited. W' meets H5-tw with `R = E` and `V = E^-1`. +It fails H5 (`V ≠ I`) and the H2 target clause (`R ≠ I`). By the uniqueness remark, `E S` is the +only listing for this placement. + +`verify.py` computes R, N, T, V, J and K' directly from the words, not from this derivation. It +checks: + +- `R = E` and `V = E^-1`, the latter as the matrix of the literal undo gates; +- (i)–(iv), and the D-shape; +- that the base word is the `R = V = I` case; +- that T is unchanged. + +The controls exhibit the converse: each failing control violates at least one equation, and its +dirty endpoint fails. + +| control | failed equations | dirty endpoint | +|---|---|---| +| old listing S | J, K | wrong on all 111 targets | +| dropped undo gate | V R, K | wrong on 6 targets | +| undo in preparation order | V R, J, K | wrong on 111 targets | +| one wrong E S row | J, K | wrong on 6 targets | +| swapped non-commuting undo pair | V R, K | wrong on 24 targets | + +Here "K" abbreviates `V N = K'T`. Every control fails the dirty endpoint. + +## 3. The bridge, cut by cut + +Align W and W' as follows: + +- the common D gates; +- W's undo, which W' skips; +- the common helper restorations and A; +- the nine COPY blocks (W adds column j of S, W' adds column j of E S); +- W''s deferred undo, which W skips; +- the common B and C. + +**Invariant.** At every cut in this alignment: + +1. every non-target register has the same value and the same frame in W and W'; +2. every target is at the zero frame in both words; +3. W''s target vector equals `M_c` times W's target vector. + +Here `M_c` is I before W's undo. During W's undo it is the running product, and it equals E from the +end of W's undo through the last COPY block. During W''s undo it is again a running product, and it +returns to I. + +*Proof.* Induction over the cuts: + +- *Common z gates.* By H1 they read no target, so they see identical operands in both words. +- *Undo gates.* These are the only target-from-target gates in the window. A W-only gate G updates + `M <- M G`, and a W'-only gate updates `M <- G M`. Both run at the zero frame on registers that + are at the zero frame. +- *COPY blocks.* A block copies the same retained total (a z register, equal in both words) and adds + `S_j c_j` in W and `E S_j c_j = M (S_j c_j)` in W'. +- *Frames.* Targets never move before B: A and the scatter do not climb them, and the exporter places + every scatter ADD at the zero frame. + +After W''s undo, `M = I`, so the complete states agree in value and frame. The remaining +instructions (B and C) are identical. + +**What `verify.py` replays.** It replays both words in lockstep with frames. The deferred side is the +deferred word itself: its D and A must equal the replayed steps, and its B must start with the replayed +undo. It checks the invariant at every cut. A listing other than `M S` breaks the invariant at the +first COPY block it affects; the old-S control is rejected exactly there. + +For example, there are 3,585 cuts on PR1062, of which 2,931 have twisted targets, and 3,136 on PR1188, +with 2,482 twisted. The verifier also checks that no z gate reads a target in the window and that +`M = E` when the scatter starts. + +**Physical reading (argued, not proved).** The physical realization of W is inherited: + +- For the 17 words with `T = I`, `verify.py` re-checks two facts. W's D has the same complete + operator as PR589's D. The PR1194-style proof-only splice, W's A/scatter/B/C with PR589's + target-only D, passes every inherited owner flag. +- For PR1868's two absorbed words, PR1868's own per-cut bridge applies. + +We argue that W' needs no new physical premise. W' differs from W, at every cut, only on targets. They +differ by a linear map of the targets, and the twisted targets are: + +- held at the zero frame; +- read by no z gate. + +The gates that realize this map in W' are of kinds the inherited interface already admits after A: + +- **Undo gates.** The deferred undo consists of B target writes from target sources, which the + inherited H3 permits ("writes a target", any sources). They run under the inherited common-label + realization at the zero frame, where every operand already sits. +- **Scatter ADDs.** W's own scatter ADDs are zero-frame target writes made after A's climbs and the + COPYs, which is the same situation as the deferred undo and the `E S` listing. + +Nothing at a nonzero frame differs, and no register climbs carrying a different value. + +This differs from PR1194's substitution, which was restricted to frame-zero D prefixes. Here the +twisted window extends through A and the scatter, though the targets stay at frame zero and unread +throughout. + +**Contrast with PR1868.** There, three helpers climbed out of the zero frame while holding +`centre + leaf`. That needed the common-frame / climb-additivity premise, applied newly to helpers. +Here no twisted register ever climbs. + +## 4. Maximality under fixed frame paths + +In this section **B means W's B**, which is W''s B after the deferred undo. `verify.py` computes these +facts on W's B, and establishes them on all 19 words: + +- **(F1) Target-frame disjointness.** For each target, take the set of nonzero frames on its ordered + frame path. These sets are pairwise disjoint: none of the 6,105 target pairs share a nonzero frame. +- **(F2) Every first B touch climbs.** Every target's first B touch runs at a nonzero frame. The very + first B gate, B[0], is such a climb. +- **(F3) Target-column confinement.** No B target write reads a target, and none runs at the zero + frame. B's own target block (B alone, from the identity) is I. +- **(F4) The undo covers every target.** All 111 targets are undo operands. + +**Proposition 1 (the undo cannot run later).** Keep the gates and the ordered per-register frame +paths. Then every target-from-target gate runs at the zero frame, before the first B climb of either +of its operands. + +*Proof.* A gate at frame f needs both operands at f at that moment. With fixed paths, f lies on both +operands' paths, and by F1 the only common frame is the zero frame. Frames never descend, and by F2 +each target leaves the zero frame at its first B touch. ∎ + +Consequences: + +- The undo block cannot follow B[0]. Its target, register 111, is an undo operand (F4). +- Each undo gate can pass only B gates that touch neither of its operands. Such a move is a + commutation, and changes no value, frame or count. + +The control that moves the undo after B[0] is rejected by the frame replay (register 111 would +descend from frame 127 to 0). Ignoring frames, its endpoint is also wrong, on 28 targets. + +**Proposition 2 (no B-side absorption).** No undo gate can be absorbed into B. + +*Proof.* In the single-edge sense of PR1868, absorption would delete an undo gate `t ^= s` and +compensate in a later gate writing t. In B, such gates are B target writes at nonzero frames f (F3). +Compensating there needs s at f, so f would have to lie on s's path, which F1 excludes. ∎ + +The census covers every pair (undo gate, B gate writing its destination): 585 pairs per word (587 on +PR1040, 586 on PR1449). None of them is frame-legal. + +More generally, B's target block is I (F3), so B supplies no target-from-target mixing. All of +`E^-1` must therefore be realized by zero-frame target gates that run before the first climbs. The +deferred undo is one such placement. The remaining freedom is: + +- the choice of circuit for `E^-1` (an open question); +- reorderings that leave its product unchanged. On PR1062 and PR1188, 270 of the 305 adjacent + transpositions commute, and those keep the boundary. The other 35 change the operator, and the + checked one breaks the endpoint; +- **where to split the undo between D and B** (below). + +**Prefix-split census.** Suppose the first k undo gates, in the literal undo order, stay in D and the +rest are deferred. The scatter then costs `nnz(E_k S)`, where `E_k` is the basis after those k gates. +Among these prefix splits of the literal undo order only, full deferral (k = 0) attains the minimum +over all split points (307, or 308 where E has 307 gates) on every word: + +- **Ties.** The first five undo gates leave `E S` itself unchanged, and the first six keep + `nnz(E_k S) = 97`, so k ≤ 6 tie. On PR1449 the counts are six and seven, so k ≤ 7 tie. On PR1040 the + minimum is unique. +- **Per-column choice.** Restricted to the two bases I and E for each COPY column, it would not help. + The old column weights are `[63, 55, 55, 55, 63, 63, 55, 55, 63]`. The E-basis weights are + `[17, 17, 8, 4, 8, 11, 13, 6, 13]`, or `[17, 16, 8, 4, 8, 10, 13, 6, 13]` on PR1040, so E is + better on every column. Such a choice would also need the undo inside the scatter, which the word + format cannot express. + +**Scope.** These statements assume fixed ordered frame paths. If paths may change, `verify.py` counts, +for each of the 213 B target writes at frame f, the other targets that could be co-located at f +under three criteria: + +| criterion | writes with a partner | max partners | +|---|---:|---:| +| loose upper bound: the target's final frame contains f | 102 | 58 | +| also: its frame at that moment lies inside f | 102 | 55 | +| also: f fits monotonically between its own earlier and later fixed touches | 94 | 7 | + +Any such visit inserts a climb into that target's path, which changes the paid profile. That class is +outside this census. + +## 5. The order-ideal refinement + +Full deferral is not optimal once commuting reorders of the undo are allowed (pre-PR proof review). + +**Construction.** Let I be an **order ideal** of the undo's dependency poset: a set of undo gates +closed under "every earlier undo gate it does not commute with". Then: + +- the undo sequence is commutation-equivalent to (the gates of I, in order) followed by (the rest, in + order); +- with `G_I` the product of the gates in I, the rest compose to `E^-1 G_I^-1`. + +The ideal-split word keeps the gates of I at the end of D, at the zero frame, lists the scatter as +`G_I E S`, and runs the rest first in B. + +**It meets the same lemma.** Its D target operator is `G_I E (y + N h)`, so: + +- `R = G_I E`; +- `V = E^-1 G_I^-1`, hence `V R = I`; +- `V N' = N = K'T`; +- J, K', U', T and C are unchanged. + +The bridge is the same with `M = G_I E` during A and the scatter. + +**Search, pinned in EXPECTED.json.** `verify.py` enumerates every order ideal of size at most 4, and +then runs a greedy strict descent from the empty ideal: + +| | 306-gate words | PR1040 | +|---|---|---| +| minimal gates | 61 | 62 | +| ideals of size 0–4 | 1, 61, 1,854, 37,461, 566,500 | 1, 62, 1,915, 39,313, 603,838 | +| best ideal | {31, 51, 52} | {32, 52, 53} | +| scatter nnz | 97 → 94 | 95 → 92 | + +PR1449 gives 1, 62, 1,915, 39,315, 603,961 ideals, and its best ideal is {32, 52, 53} with nnz 94. +The greedy descent reaches the same ideal on every word, and no ideal of size 4 improves on size 3. + +**Fully checked words.** On PR1062, PR1188, PR1040 and PR1868's absorbed PR1188 word, `verify.py` +builds the best split found and applies the deferred word's checks: + +- boundary both ways; +- identical frame paths and MOVE records; +- paid profile from frames and from the exporter; +- guards; +- owner checker, with exactly `H5_V_identity` newly false; +- H5-tw identities with `R = G_I E` and `V` the matrix of the remaining gates; +- the per-cut bridge. + +| word | base | full deferral | ideal split | +|---|---:|---:|---:| +| PR1062 | 11,500 | 11,070 | **11,067** | +| PR1188 | 10,492 | 10,062 | **10,059** | +| PR1040 | 11,780 | 11,348 | **11,345** | +| PR1868 absorbed PR1188 | 10,489 | 10,059 | **10,056** | + +They match the counts an independent pre-PR reviewer found. F, B and the guard bits equal the full-deferral values. + +This is a refinement **found by search, not an optimum.** The only pinned search evidence is the exhaustive +search over ideals of size at most 4 and the greedy descent above; whether larger ideals go lower is open. +Full deferral stays the headline construction because its contract is the cleanest (`R = E`, `V = E^-1`). + +## 6. Accounting + +The scatter falls from 527 to 97 ADDs. The undo's 306 ADDs (307 on PR1040 and PR1449) move from D to +B; none is deleted. So the complete local count falls by 430. On PR1040 it falls by 432: its E differs +(PR1040's extra target step), and its E S listing has 95 ones. + +| quantity | change | +|---|---| +| F | unchanged on every word | +| B | falls on every word | +| guard bits | never rise | +| frames, climbs, COPY ranks | unchanged | +| exporter MOVE records (2,911) | identical | +| paid profile `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, rank mass 5,129 | unchanged | + +On PR941's floor-calibration word the nine-stage guard moves from 193 to 192 bits. That word is the +only base word that misses the guard, and the guard check must reject it (a pinned control). Its +deferred word meets the guard. + +## 7. The selected-word heuristic (PR589) + +PR589 has no target-basis block: its D is the 111 reads, so the deferral itself is vacuous there. A +scatter basis G still fits H5-tw, with `R = G` and `V = G^-1`. + +**Construction.** Run Prim's algorithm over the 111 scatter rows plus a zero root: + +- edge cost is `2 + Hamming distance` (one gate in G and one in `G^-1`, plus the changed row); +- root cost is the row weight. + +The tree has 79 edges and 32 roots. G is the 79 transvections `a ^= parent(a)`, children before +parents, placed after the D reads at the zero frame. `G^-1` is G reversed, as the first gates of B. +The listing is `G S`, with 254 ones. + +**Cost and checks.** The scatter-related cost falls from 527 to `158 + 254 = 412`, and the word from +24,305 to 24,190 ADDs. `verify.py` applies the same checks: + +- boundary; +- frames and MOVE records; +- exporter paid profile and rank mass; +- guards (93/177 bits, unchanged; the reverse bound B rises from 1,113,070 to 1,117,988); +- H5-tw identities; +- the bridge to PR589 itself. + +**Owner flags.** PR589 passes every owner flag. The heuristic word makes three newly false: + +- `H2_D_frame0_targets_from_helpers` and `K_equals_D`: the same syntactic departure every lineage word + already has, caused by target-from-target gates in D. +- `H5_V_identity`. + +This is a heuristic (an MST over one fixed cost model), not an optimum. + +## 8. What is not proved here + +- **Native and hosted replay.** Native 5/9/11-stage C++ replay was not run on the deferred words. + Hosted emission and invoice were not run either; for the deferred PR1122 word, PR1806's PR1122 + nine-stage hosted invoice is the obvious route. The undo now appears in B's exporter phase (4) + rather than D's (1), and any phase-specific expectation of those tools is unchecked. +- **Inherited obligations.** The all-size compiler, the common-label/mutable-source realization, + rounding/tape and the analytic obligations remain inherited. +- **Adoption.** Whether H5-tw is accepted as the interface is a maintainer decision. The lemma and + the argued bridge are offered as the case for it. diff --git a/research/r439-deferred-native/vendor/pr2115/README.md b/research/r439-deferred-native/vendor/pr2115/README.md new file mode 100644 index 0000000000..65f1c7c1ba --- /dev/null +++ b/research/r439-deferred-native/vendor/pr2115/README.md @@ -0,0 +1,469 @@ +# Deferred target basis: `V R = I` replaces H5 together with the H2 target clause + +**Replacement-interface result with finite R439 instances. No new κ, and the bit side does not +bind.** The selected result, the selected bit supplier (PR589) and `upstream/` are unchanged. + +## The interface result + +Three statements of the interface keep two clauses fixed: the inherited interleaved lemma (eumemic's +PR543, `research/e8-bit-r420/README.md`) and the two later R439 replacements of H2/K. The clauses are: + +- the target clause of H2: D adds to the targets without changing their basis, `R = I`; +- H5: the raw word `W0' = (A, scatter, B)` has target-to-target block `V = I`. + +The two replacements are woklerx's PR1194 semantic D (H2-sem) and PR1868's twisted helper contract. +PR1194 states the first clause as "complete restoration of every helper and target basis at D's +boundary". + +This package replaces that pair by their product. D may leave the targets in any basis R, provided +`W0'` applies `R^-1` before the targets climb: + +| | inherited / PR1194 / PR1868 | H5-tw (this package) | +|---|---|---| +| D operator | `(x, y + N h, T h)` (`T = I` except PR1868) | `(x, R y + N h, T h)` | +| D shape | zero frame, source-free, no COPY/ERASE/climb | same | +| target basis | `R = I` and `V = I` | **`V R = I`** | +| source response | `J = I` | `J = I` | +| helper response | `N = K` (PR1194), `N = K'T` (PR1868) | **`V N = K'T`** | +| cleanup | z-only at the full frame; literal H4 (`T = I`) or PR1868's H4-tw | z-only at the full frame; `C U'(I ⊕ T) = I` | +| H1, H3 | kept | kept | + +**Lemma (H5-tw, with its converse).** Assume: + +- H1, H3 and the D shape; +- C is z-only at the full frame; +- D acts as `(x, y, h) -> (x, R y + N h, T h)`, and `W0'` has block form + `z' = U'z`, `y' = V y + J x + K' h`. + +Then the complete word acts as `(z, y) -> (C U'(I ⊕ T) z, V R y + J x + (V N + K'T) h)`. So it maps +`(x, y, h) -> (x, y + x, h)` on every F2-module **if and only if** all four of these hold: + + V R = I, J = I, V N = K'T, C U'(I ⊕ T) = I. + +Each equation is read off the unit columns, so all four are necessary. The inherited contract is the +case `R = V = I`. Under the literal H4, the last equation holds exactly when `T = I`; PR1868's H4-tw +is that equation itself. [PROOF.md](PROOF.md) section 1 gives the proof. + +**The bridge, cut by cut.** A deferred word W' differs from its base word W only on the targets, +and only by the target basis. From W's undo to W''s deferred undo, every target of W': + +- sits at the zero frame; +- is read by no z gate (H1): the only gates touching it are scatter ADDs into it and the undo gates; +- holds `M` times W's target values, where `M = E` during A and the scatter. + +The undo runs at the zero frame, after which the complete states (values and frames) are equal and +the remaining instructions are identical. `verify.py` replays the deferred word's own D, A and B +prefix against W in lockstep. It checks this invariant at every cut on every word, for example +3,585 cuts on PR1062 and 3,136 on PR1188. + +W itself is anchored as before. For the 17 words with `T = I`, its D has PR589's D operator, and the +PR1194-style splice passes every inherited owner flag. PR1868's two words use its own bridge. + +**We argue that no new physical premise is needed** (PROOF.md section 3). The deferred undo consists +of zero-frame B target writes from target sources, which the inherited H3 admits. W's own scatter +ADDs are already zero-frame target writes made after A's climbs. + +This differs from PR1194's substitution, which was restricted to frame-zero D prefixes. Here the +twisted window extends through A and the scatter, with the targets held at frame zero and unread. + +It also differs from PR1868. There, three helpers climbed out of the zero frame holding a twisted +value, which needed the helper common-frame / climb-additivity premise. Here no twisted register +ever climbs. + +**Maximality (fixed ordered frame paths).** Here B means W's B, which is W''s B after the deferred +undo. On every word: + +- the nonzero frame sets of the 111 targets are pairwise disjoint (0 of 6,105 pairs share one); +- every target's first B touch climbs out of the zero frame, the first at B[0]; +- no B target write reads a target, and B's own target block is I. + +Hence every target-from-target gate must run at the zero frame before its operands' first climbs. +The deferred undo is one such placement. + +- **Timing.** The undo cannot follow B[0], whose target is an undo operand. +- **Absorption.** No undo gate can be absorbed into a B target write. Of the 585 (undo gate, B write) + pairs per word (587 on PR1040, 586 on PR1449), none is frame-legal. +- **Prefix splits.** Among prefix splits of the literal undo order only, full deferral is a best + split: keeping a prefix of the undo in D never makes the scatter cheaper. + +**Full deferral is not optimal once commuting reorders are allowed.** The pre-PR proof review found +a better split, which the same lemma covers. Keep an order ideal (a commutation-closed down-set) of +the undo's dependency poset at the end of D, list the scatter in the resulting basis, and run the rest +of the undo first in B. See "Order-ideal refinement" below and [PROOF.md](PROOF.md) sections 4–5, +which also give the scope limit when paths may change. + +## The construction + +Every committed PR915-lineage R439 word has a D section of this shape: + + helper-star preparations, P_E (306 gates), helper reads (111), U_E = P_E reversed, helper restorations + +All of it runs at the zero frame. `P_E` has 307 gates on PR1040 and PR1449, and PR915's word has no +helper stars. The deferred word makes three changes: + +1. it deletes `U_E` from D; +2. it runs the same gates, at the zero frame, as the first gates of B; +3. it replaces the scatter listing S (111 rows over the nine retained totals) by the rows of `E S`. + +`E S` is the unique listing for this placement (PROOF.md section 1). Its consequences: + +- **Twisted window.** During A and the scatter the targets hold E times their original values. +- **Contract.** `R = E` and `V = E^-1`. +- **Unchanged.** T, J, K', U' and C are all unchanged. +- **Scatter.** `E S` has 55 nonzero rows and 97 ones, against 527 ones in S. +- **Count.** The complete local ADD count falls by 430 (432 on PR1040; see below). The undo's ADDs + move from D to B; none is deleted. +- **Frames and bounds.** Frame paths, COPY ranks, MOVE records and the paid profile are unchanged. + F is unchanged, and B falls. + +## Census of every committed lineage word (as of base c6765481) + +All 19 distinct committed lineage words were found by scanning `research/` for R439 word files and +deduplicating vendor copies by canonical hash. To repeat the scan (it needs git), run: + +```sh +python3 research/r439-deferred-target-basis-seed06/verify.py --census-scan +``` + +It lists every committed R439 word and reports any word missing from the verifier's lists. At c6765481 +it reports 27 distinct words (19 lineage and 8 outside), all listed. + +Every number below is recomputed live by `verify.py` and pinned in [EXPECTED.json](EXPECTED.json). + +| word (PR, author) | ADDs base → deferred | saving | F | B base → deferred | local/nine-stage bits | +|---|---:|---:|---:|---:|---| +| PR915 (Gareth Davidson), `r439-target-compensation` | 13,208 → **12,778** | 430 | 49,347 | 9,534,616 → 8,742,940 | 100/189 → 99/189 | +| PR926 (Gareth Davidson) | 11,980 → 11,550 | 430 | 71,907 | 10,562,318 → 9,770,642 | 102/192 → 101/192 | +| PR941 (Gareth Davidson) | 11,949 → 11,519 | 430 | 70,083 | 10,548,832 → 9,757,156 | 101/192 → 101/192 | +| PR941 floor-calibration word | 11,948 → 11,518 | 430 | 73,603 | 10,518,760 → 9,727,084 | 102/**193** → 101/192 | +| PR965 (Ross Richardson) | 11,840 → 11,410 | 430 | 72,399 | 10,464,656 → 9,672,980 | 102/192 → 101/192 | +| PR967 (Sricharan Vagvala) | 11,783 → **11,353** | 430 | 72,847 | 10,394,084 → 9,602,408 | 102/192 → 101/192 | +| PR1040 (woklerx) | 11,780 → 11,348 | **432** | 72,847 | 10,394,084 → 9,602,408 | 102/192 → 101/192 | +| PR1047 (woklerx) | 11,769 → 11,339 | 430 | 72,847 | 10,394,084 → 9,602,408 | 102/192 → 101/192 | +| PR1449 (Hanson Sun, @bbMisk) | 11,781 → 11,351 | 430 | 72,847 | 10,394,084 → 9,602,408 | 102/192 → 101/192 | +| PR1062 (Sagar Thakrar) | 11,500 → **11,070** | 430 | 25,717 | 5,911,840 → 5,024,524 | 95/182 → 95/181 | +| PR1062 composition word | 11,515 → 11,085 | 430 | 24,625 | 5,846,566 → 4,971,904 | 95/181 → 95/180 | +| PR1062 pair-control word | 11,715 → 11,285 | 430 | 24,563 | 5,892,602 → 5,005,286 | 95/181 → 95/180 | +| PR1543 (ToikY) | 11,489 → **11,059** | 430 | 25,885 | 5,977,064 → 5,089,748 | 96/182 → 95/181 | +| PR1709 (Cinna Davis) | 11,488 → 11,058 | 430 | 27,061 | 5,921,344 → 5,034,028 | 96/182 → 95/181 | +| PR1868 absorbed PR1062 (Sagar Thakrar), `T ≠ I` | 11,497 → 11,067 | 430 | 25,717 | 5,858,638 → 4,976,508 | 95/182 → 95/181 | +| PR1122 (Gareth Davidson) | 10,652 → **10,222** | 430 | 15,223 | 3,910,388 → 2,996,128 | 92/176 → 91/174 | +| PR1208 (ToikY), `r439-abc-zrewrite-seed16` | 10,542 → **10,112** | 430 | 13,721 | 3,663,878 → 2,774,762 | 91/174 → 91/173 | +| PR1188 (Gareth Davidson) | 10,492 → **10,062** | 430 | 13,667 | 3,758,418 → 2,825,146 | 91/175 → 91/173 | +| PR1868 absorbed PR1188 (Sagar Thakrar), `T ≠ I` | 10,489 → **10,059** | 430 | 13,667 | 3,748,680 → 2,816,834 | 91/175 → 91/173 | + +Bold ADD counts are the eight pinned in `verify.py`'s probe table (from the unpublished exploratory +probe); all eight reproduce exactly. On every word `verify.py` checks all of the following: + +- **Boundary.** `(x, y, h) -> (x, y + x, h)` on all 661 dirty columns, forward and reverse, through + the literal COPY/ERASE stream, for both the base and the deferred word. +- **Frames.** The ordered per-register frame paths and the exporter's 2,911 MOVE records are + identical. +- **Paid profile.** Every lineage word has the PR589 profile `{1:1323, 2:1342, 3:79, 4:44, 5:102, + 6:11, 7:19}`, rank mass 5,129. It is computed from the frame paths and, separately, by the pinned + exporter (`research/e8-bit-carrier-skeleton/code/bit/export_records.py`), which runs with exit code 0. +- **Guards.** The exporter's ADD count and F/B match the literal replay. Both strict guards + (`64 F^3 B^2 < 2^104`, `2^18 F^5 B^4 < 2^192`) hold on every deferred word, and the guard bits + never rise. +- **Owner checker.** The unchanged `research/e8-bit-p111-tuned/code/xcheck_p.py` accepts geometry + and endpoint. Exactly one flag becomes newly false, `H5_V_identity`, beside the inherited + `H2_D_frame0_targets_from_helpers` and `K_equals_D`. PR1868's words also keep their inherited + `H4_C_literal_reverse_at_full` and `C_is_U_inverse`. +- **Identities.** `V R = I`, `V N = K'T`, `J = I` and `C U'(I ⊕ T) = I` hold, with `R = E` and `V` + equal to the matrix of the literal undo gates. The base word is the `R = V = I` case. + +**Not reproduced as stated.** An exploratory estimate of 430 on every word does not hold for +PR1040: its E differs (PR1040's extra target step), its `E S` listing has 95 ones, and the saving is +432. PR1449 also has 307 preparation gates, split by a helper gate, but its listing has 97 ones and it +saves 430. Every other probe number reproduces. + +**Composition with PR1868.** PR1868's absorbed PR1188 word is merged. Deferral on it gives +**10,489 → 10,059**, the lowest full-deferral count in this census. + +**Words outside the lineage.** Eight committed R439 words have no target-basis block: PR555, PR589, +PR904, PR936, PR952, PR980, PR1127 and PR1221. Their D is the 111 helper reads, so `R = I` and the +deferral is vacuous; `verify.py` checks the shape. + +Some packages carry moves or certificates rather than a committed word. They are not censused here: + +- PR1045 and PR1400 (helper fusion and descent moves); +- PR1704 (two-copy scatter). + +## Order-ideal refinement (found by search, not optimal) + +Call a set I of undo gates an **order ideal** when it contains, with each gate, every earlier undo gate +that the gate does not commute with. Keeping such an I in D is then commutation-equivalent to splitting +the undo there. The ideal-split word keeps I at the end of D (at the zero frame), lists the scatter as +`G_I E S`, where `G_I` is the product of the gates in I, and runs the rest of the undo first in B. It +meets the same lemma, with `R = G_I E` and `V = E^-1 G_I^-1`. + +`verify.py` runs two searches on every lineage word: + +- an exhaustive search over all ideals of size at most 4 (566,500 of size 4 on the 306-gate words); +- a greedy strict descent. + +Both find the size-3 ideal {31, 51, 52} with scatter nnz 94 against 97 ({32, 52, 53} on PR1040 and +PR1449, with 92 and 94). No size-4 ideal does better. + +On four words it builds the split and applies every check of the deferred word: boundary both ways, +paths and MOVE records, exporter profile, guards, owner checker (exactly `H5_V_identity` newly false), +H5-tw identities and the per-cut bridge. + +| word | base | full deferral | ideal split | +|---|---:|---:|---:| +| PR1062 | 11,500 | 11,070 | **11,067** | +| PR1188 | 10,492 | 10,062 | **10,059** | +| PR1040 | 11,780 | 11,348 | **11,345** | +| PR1868 absorbed PR1188 | 10,489 | 10,059 | **10,056** | + +F, B and the guard bits equal the full-deferral values. They match the counts an independent pre-PR reviewer found. + +Full deferral remains the headline construction, because its contract is the cleanest (`R = E`, +`V = E^-1`). The ideal split is a refinement under the same lemma. It was found by search, and no +optimality is claimed. + +## Committed instances + +[candidate-1062.json.gz](candidate-1062.json.gz) and [candidate-1188.json.gz](candidate-1188.json.gz) +are the fully deferred PR1062 and PR1188 words. They are canonical JSON, gzip mtime 0, rebuilt +deterministically by `verify.py --write`. The verifier requires the decompressed payload to equal +the rebuilt word byte for byte. The gzip containers are also byte-identical under CPython 3.12.15. +They differ under 3.14.8, as CONTRIBUTING.md anticipates, while the payloads still match. The +ideal-split words are rebuilt in memory and pinned by SHA-256 in EXPECTED.json. + +## Selected-word heuristic (PR589) + +PR589 has no target basis, but a scatter basis G fits the same contract, with `R = G` and +`V = G^-1`. G comes from a minimum spanning tree over the scatter rows plus a zero root, with edge +cost `2 + Hamming distance`. It has 79 transvections, placed after the D reads at the zero frame, and +`G^-1` runs first in B. + +The scatter-related cost falls from 527 to 412 (158 basis gates plus 254 listing ones), and the word +from 24,305 to 24,190 ADDs. The same checks pass: + +- boundary, frames and exporter profile; +- guards: 93/177 bits, unchanged, while the reverse bound B rises from 1,113,070 to 1,117,988; +- H5-tw identities and the bridge to PR589. + +PR589 itself passes every owner flag, so here three flags become newly false: + +- `H2_D_frame0_targets_from_helpers` and `K_equals_D`: the lineage's syntactic departure, caused by + target gates in D; +- `H5_V_identity`. + +**This is a heuristic, not an optimum, and no supplier change is proposed.** + +## Controls + +The PR1062 and PR1188 instances carry these controls. All must fail or be rejected. + +1. **Deferral with the old listing S.** The dirty endpoint is wrong on all 111 targets, and + `J = I` and `V N = K'T` fail. +2. **Undo moved after B[0]**, the first B climb of an undo operand. The frame replay rejects it: + register 111 would descend from frame 127 to 0. With frames ignored, the endpoint is wrong on 28 + targets. +3. **First undo gate dropped.** The endpoint is wrong on 6 targets; `V R = I` and `V N = K'T` fail. +4. **Reordered undo.** + - *Preparation order instead of its reverse:* the endpoint is wrong on all 111 targets, and all + three target equations fail. + - *Adjacent swaps (honest census):* 305 per instance. 270 swap commuting gates and keep the + operator; a checked one keeps the boundary exact. The other 35 change the operator; the first + (gates 7 and 8) breaks the endpoint on 24 targets. So the order matters only through the product + `E^-1`. +5. **One wrong `E S` row** (row 1, bit 0 flipped). The endpoint is wrong on 6 targets. +6. **Corrupted source pin.** The SHA-256 check rejects it. + +**Check-level controls.** Each must be rejected by the intended check, which is matched by its error +message. + +| check | control (per instance unless noted) | +|---|---| +| bridge structure | the deferred word with its last D gate dropped | +| bridge invariant | the old-S word | +| bridge, undo complete | the swapped-undo word | +| owner delta | `(base, base)`, which has no newly false flag | +| frame paths | a legal frame raise of B[500], frame 508 → 422 | +| paid profile | the same raise, which also changes the profile | +| exporter profile | the base word's exporter profile against the raised profile | +| maximality | the census run with the deferred word as its own base | +| precision guard (once) | the PR941 floor-calibration base word, 193 nine-stage bits | + +**Mutation run.** We ran 26 mutants of copies of the verifier (not shipped). Disabling the body of +any check (guards, paths, profile, exporter profile, owner delta, bridge invariant, bridge structure, +undo completion or maximality) now makes the verifier fail. + +Six mutants still pass: + +- **Call-site removals (2).** One drops the base-word guard call; the other forces the owner delta. + Their outputs stay pinned in EXPECTED.json. +- **Equivalent mutant (1).** Changing `<` to `<=` at the guard caps makes no difference, because no + word sits exactly at a cap. +- **Redundant pins (2).** Removing the review-number pin, or the F/B-equality check, for the ideal + splits is covered: those values are also pinned in EXPECTED.json. +- **gzip mtime (1).** A changed gzip mtime passes, as CONTRIBUTING.md requires. + +## Reproduce + +From the repository root (standard library only; about 40–95 s per run on an Apple-silicon Mac, +depending on the interpreter): + +```sh +python3 -I -B research/r439-deferred-target-basis-seed06/verify.py +python3 -I -O -B research/r439-deferred-target-basis-seed06/verify.py +python3 scripts/research_package.py --package research/r439-deferred-target-basis-seed06 --check-only +python3.12 scripts/research_package.py --package research/r439-deferred-target-basis-seed06 +``` + +The expected final line is: + +```text +PASS_R439_DEFERRED_TARGET_BASIS words=19 outside=8 instances=2 ideal_splits=4 columns=661 controls=33 no_new_kappa (… s) +``` + +All 29 inputs are pinned by SHA-256 and git blob in [SOURCES.json](SOURCES.json): 27 words, the owner +checker and the exporter. The verifier refuses drifted bytes. + +- **Owner checker.** It runs from its verified bytes in-process. It raises its own `Reject`, not + `assert`. +- **Exporter.** It runs from its verified bytes in a child interpreter without `-O`. +- **Checks.** They raise `ValueError`, so `-O` cannot weaken them. The report must equal + EXPECTED.json exactly. +- **Portability.** The report is identical under CPython 3.12.15 and 3.14.8. + +`--write` regenerates EXPECTED.json and the two payloads. `--census-scan` repeats the word census. + +## Task and scope + +The card is `bit-helper-contract` (scope key 3475f46c8358c6a9211b), and the scope status is +**changed**. The card asks for an H2/K replacement for a helper operation. This package also relaxes +H5 (`V = I`), which the card keeps, and its object is the target-basis block, not a helper operation. +It also broadens to every committed lineage word, instead of narrowing to one helper-star instance as +the card's allowed variation suggests. TASK.json records the full reason. + +## Scope and limits + +- **The new result.** It is the interface lemma H5-tw with its converse, the argued cut-by-cut + bridge, the maximality census among prefix splits, the order-ideal refinement and the finite + instances. The ADD savings are finite consequences. They do not change the paid profile, the + selected moment or κ. +- **Scope of maximality.** It is proved for fixed ordered frame paths and prefix splits of the literal + undo order. If paths may change, `verify.py` counts the other targets that could be co-located at a + B target write's frame, under three criteria: + - *loose upper bound* (the target's final frame contains the write frame): 102 of 213 writes, up to + 58 targets; + - *with the target's current frame inside the write frame:* 102 writes, up to 55; + - *monotone through the target's own fixed touches:* 94 writes, up to 7. + + Any such move changes that target's path and the paid profile, so it is not covered. +- **Not run.** + - Native 5/9/11-stage C++ replay and hosted emission/invoice were not run on the deferred words. + For the deferred PR1122 word, PR1806's PR1122 nine-stage hosted-invoice replay is the obvious + route. + - The undo now sits in B's exporter phase rather than D's, and any phase-specific expectation of + those tools is unchecked. + - The all-size compiler, common-label/mutable-source realization, rounding/tape and analytic + obligations remain inherited. +- **Adoption.** Whether H5-tw becomes the interface is a maintainer decision. The owner checker's H5 + is literal, and it flags every deferred word. + +## Related and concurrent work + +- **PR1704** (Ross Richardson, merged, `research/bit-two-copy-scatter`) is the nearest construction. + It rewrites the same 527-ADD scatter of PR1062's word, using two simultaneously live COPY + temporaries under a replacement copied-workspace contract, and reaches 527 → 407. + - It is a different mechanism, under a different interface: this package keeps one temporary and + the inherited COPY/ERASE contract. PR1704's README explicitly excludes target-basis changes. + - **The two savings are not additive.** Both rewrite the same block. After deferral the scatter has + 97 ADDs, and PR1704's −120 was computed on S, not on `E S`. +- **PR1194** (woklerx) and **PR1868** keep `R = V = I`. This package keeps their D-shape and cleanup + clauses, replaces the target-basis pair by `V R = I` and generalizes K to `V N = K'T`. +- **PR794** (commdata2338, open) is R420 target-basis compensation. Its preparation, reads and undo + all stay inside D, as in PR915, and it does not defer the undo. +- **PR2037** (commdata2338, open) routes R439 H2/K work through the retained semantic-D evidence. +- **PR1806** (mtpsl, merged) is the complete PR1122 nine-stage hosted invoice. It is the hosted route + for the deferred PR1122 word. +- **PR1580 and PR1592** (Arham Tahir, merged) exclude terminal helper-star restoration and arbitrary + terminal star compensation under fixed frames. They are the contrasting deferral results: those + move helper restorations to the end, while this package moves a target-basis undo past A and the + scatter. +- **Same-card and nearby work.** + - Discussion #1166, cycle 18 (Cinna Davis, @1337isnot1337): a post-read one-gate star compensation + run on PR1062's word, which was not pushed. + - PR2033 (ToikY, open): a helper-sharing pair on PR1062's star word. + - PR1913 (Adam Gall, merged) and PR1937 (Aaron Wang, open): helper-star absorption corrections. + + All of these are helper side. +- **PR1435** (woklerx) bounds late mixing of the retained totals before the COPY by its paid COPY + frames. That is helper side, not target basis. +- **Overlap search.** `gh pr list --state all --search` was run for: scatter, "target basis", H5, + V_identity, "deferred undo", 10,062, 11,070 and "twisted target". It found no PR that defers the + undo or lists the scatter in the target basis. The last five terms returned nothing relevant. + `scripts/find_overlap.py` with "deferred undo", "H5_V_identity", "twisted target" and "deferred + target" returned no matches. This is not a novelty certificate. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **A joint basis for the reads and the scatter.** + - *Why it matters:* E was chosen by PR915's application of PR794's greedy search, for the D reads + alone. Once the undo is deferred, the same basis also prices the scatter (`nnz(E S)`). + - *First step:* add `nnz(E S)` to that search's objective, under the same prefix guards. +2. **A shorter circuit for `E^-1`, and better order-ideal splits.** + - *Why it matters:* maximality fixes where target-from-target gates may run, not the circuit for + `E^-1` or the best split. The ideal search is exhaustive only up to size 4. + - *First step:* resynthesize `E^-1` at the zero frame with a bounded linear-circuit search, and + extend the ideal search (larger sizes, or a joint split and resynthesis). +3. **Composition with other rewrites.** + - An exploratory probe suggests the deferral also composes with a shear-descent D rewrite, but no + number is claimed until it is verified. + - Whether a two-copy pairing in the style of PR1704 still pays on the 97-ADD `E S` listing is + open. +4. **Native and hosted replay.** + - *First step:* run PR1188's native checkers (or PR1902's audit harness) on + `candidate-1188.json.gz`, or PR1806's hosted-invoice replay on the deferred PR1122 word. + - *Blocker:* a host with Boost or PR1509's checked stand-in. +5. **An optimal scatter basis on PR589.** The MST basis is a heuristic, and an exact or better bound + for this cost model is open. + +## Credit + +- **Target-basis lineage.** + - Gareth Davidson (@bitplane): PR915 guarded target-basis compensation on R439, the E block this + package defers; also PR926, PR941, PR1122 and PR1188, and the outside words PR904, PR952 and + PR980. + - commdata2338: PR794 (open), the guarded target-basis method and the greedy prefix-guarded search + that PR915 transfers to R439. + - Scott Woolsey Biggart (@swbiggart): PR713, the first restored target basis, on R420. + - Sagar Thakrar: PR716, optimal disjoint R420 target pairs. + - Dugongue: #476 and #478, the reversible donor-receiver target identity. The deferral stretches + that identity across the scatter. +- **Lineage words.** + - Sricharan Vagvala (@theon199): PR967 helper stars. + - Ross Richardson: the PR923 frame-520 circuit inside the words; PR965 helper triples; PR936. + - Aaron Wang (@navinor): the PR1015 B circuits inside the words; PR1127. + - Sagar Thakrar: PR1062 and PR1868. + - woklerx: PR1040 and PR1047. + - Hanson Sun (@bbMisk): PR1449 and PR1221. + - ToikY: PR1543 and PR1208. + - Cinna Davis (@1337isnot1337): PR1709. + - DreamingOfClouds: PR589 tuning, on eumemic's PR555 word, built on DreamingOfClouds' PR545 + punctured unit. +- **Interface and checkers.** + - eumemic: PR543, the R420 word and the H1–H5 interleaved lemma in `research/e8-bit-r420`; PR555 + and its checker adaptation `xcheck_p.py`. + - Zhihao Chen: PR425 (open), the scalar-interface lemma. + - Mikhail R. Gadelha: PR686 (open), the first semantic D-boundary substitution. + - woklerx: PR1194 semantic D. + - Arham Tahir (@Arham-Tahir64): PR1311 bridge. + - Dylan Crow: the exporter `export_records.py` (per its header, carried in eumemic's PR493 + package). + - Hanson Sun (@bbMisk): PR1902 native audit of PR1868's words. +- **Nearest construction.** Ross Richardson's PR1704 two-copy scatter: a different mechanism, not + additive with this one. +- **Review.** The pre-PR review found the order-ideal refinement, the bridge's reliance on the base + word, and the missing check-level controls, all fixed here. + +Prepared by Sagar Thakrar with substantial Anthropic Claude assistance (Claude Code, including +subagents for the exploratory probe, its independent checks, the pre-PR review and package assembly). +No independent human review. New work is Apache-2.0. diff --git a/research/r439-deferred-native/vendor/pr2115/candidate-1188.json.gz b/research/r439-deferred-native/vendor/pr2115/candidate-1188.json.gz new file mode 100644 index 0000000000..e72404c457 Binary files /dev/null and b/research/r439-deferred-native/vendor/pr2115/candidate-1188.json.gz differ diff --git a/research/r439-deferred-native/verify.py b/research/r439-deferred-native/verify.py new file mode 100644 index 0000000000..a4d5b05804 --- /dev/null +++ b/research/r439-deferred-native/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Exact PR2115 phase transfer and opt-in native replay. + +Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance. +Apache-2.0. Predecessor construction and reused checkers are credited in README. +""" +import argparse +import copy +import hashlib +import os +from pathlib import Path +import runpy +import struct +import subprocess +import sys +import tempfile + +C = runpy.run_path(str(Path(__file__).with_name("common.py"))) +HERE, ROOT = C["HERE"], C["ROOT"] +need, same, load, write, digest = (C[k] for k in ("need", "same", "load", "write", "digest")) +L = runpy.run_path(str(HERE / "literal.py")) +BASE_WORD = "research/r439-gl5-shortest/candidate.json.gz" +CANDIDATE = HERE / "vendor/pr2115/candidate-1188.json.gz" +PROFILE = {"1": 1323, "2": 1342, "3": 79, "4": 44, "5": 102, "6": 11, "7": 19} + + +def phase_bill(word): + return {str(i + 1): sum(map(len, word[phase])) if phase == "scatter" + else sum(len(g[2]) for g in word[phase]) + for i, phase in enumerate(("D", "A", "scatter", "B", "C"))} + + +def rebuild(base): + """Reconstruct the exact full deferral; do not import PR2115's generator.""" + v = base["v"] + runs = [] + for i, gate in enumerate(base["D"]): + frame, dst, srcs = gate + need(frame == 0, "D zero frame") + ty = "yy" if v <= dst < 2*v and all(v <= s < 2*v for s in srcs) else "other" + if not runs or runs[-1][0] != ty: + runs.append([ty, []]) + runs[-1][1].append(i) + same([(t, len(indices)) for t, indices in runs], + [("other", 236), ("yy", 306), ("other", 111), ("yy", 306), ("other", 236)], + "pinned D block pattern") + prep = [base["D"][i] for i in runs[1][1]] + undo = [base["D"][i] for i in runs[3][1]] + same(undo, list(reversed(prep)), "literal target undo") + rows = [set(r) for r in base["scatter"]] + for _, dst, srcs in prep: + for src in srcs: + rows[dst-v].symmetric_difference_update(rows[src-v]) + result = copy.deepcopy(base) + removed = set(runs[3][1]) + result["D"] = [g for i, g in enumerate(base["D"]) if i not in removed] + result["B"] = copy.deepcopy(undo + base["B"]) + result["scatter"] = [sorted(row) for row in rows] + return result, undo + + +def rejected(action, label, expected=None): + try: + action() + except ValueError as exc: + if expected is not None: + need(expected in str(exc), label + ": wrong failure: " + str(exc)) + return label + raise ValueError("control accepted: " + label) + + +def finite(): + sources = C["pins"]() + base, candidate = load(ROOT / BASE_WORD), load(CANDIDATE) + rebuilt, undo = rebuild(base) + same(rebuilt, candidate, "complete reconstructed candidate payload") + prices = {label: L["literal_price"](word) for label, word in (("0", base), ("1", candidate))} + for price in prices.values(): + L["require_admission"](price) + same([prices[k]["ADDs"] for k in ("0", "1")], [10492, 10062], "complete ADDs") + same([prices[k]["F"] for k in ("0", "1")], [13667, 13667], "F") + same([prices[k]["B"] for k in ("0", "1")], [3758418, 2825146], "B") + old, new = phase_bill(base), phase_bill(candidate) + same({k: new[k]-old[k] for k in old}, {"1": -306, "2": 0, "3": -430, "4": 306, "5": 0}, + "phase transfer invoice") + owner = runpy.run_path(str(ROOT / "research/e8-bit-p111-tuned/code/xcheck_p.py")) + flags = {} + for key, word in (("0", base), ("1", candidate)): + _, _, fl, h, c, _ = owner["check"](word) + flags[key] = sorted(k for k, v in dict(h, **c).items() if not v) + need(fl["columns"] == 661, "owner column domain") + same(flags["0"], ["H2_D_frame0_targets_from_helpers", "K_equals_D"], "baseline flags") + same(flags["1"], ["H2_D_frame0_targets_from_helpers", "H5_V_identity", "K_equals_D"], "deferred flags") + controls = [] + dropped = copy.deepcopy(candidate) + del dropped["B"][0] + controls.append(rejected(lambda: L["execute"](dropped), "missing undo gate", "dirty full-word boundary")) + wrong = copy.deepcopy(candidate) + wrong["scatter"] = copy.deepcopy(base["scatter"]) + controls.append(rejected(lambda: L["execute"](wrong), "old scatter", "dirty full-word boundary")) + reversed_undo = copy.deepcopy(candidate) + reversed_undo["B"][:306] = list(reversed(undo)) + controls.append(rejected(lambda: L["execute"](reversed_undo), "wrong undo order", "dirty full-word boundary")) + late = copy.deepcopy(candidate) + late["B"] = [candidate["B"][306]] + undo + candidate["B"][307:] + try: + owner["check"](late) + except owner["Reject"] as exc: + need("climb" in str(exc), "late undo wrong failure") + controls.append("undo after first target climb") + else: + raise ValueError("late undo accepted by frame checker") + C["pins"]() + result = dict(status="PASS_R439_DEFERRED_FINITE", payloads={"0": digest(base), "1": digest(candidate)}, + prices=prices, phase_ADDs={"0": old, "1": new}, undo_gates=len(undo), + all_dirty_columns=661, directions=2, owner_false=flags, controls=controls, + sources=sources, new_kappa_claim=False) + return result, {"0": base, "1": candidate} + + +def records(path): + raw = path.read_bytes() + need(len(raw) % 24 == 0, "record alignment") + return list(struct.iter_unpack("<6i", raw)) + + +def phase_binding(rows, expected): + observed = {str(i): 0 for i in range(1, 6)} + for row in rows: + if row[0] == 1: + need(str(row[5]) in observed, "unknown ADD phase") + observed[str(row[5])] += 1 + same(observed, expected, "exported ADD phases") + return observed + + +def record_binding(rows, expected_sha256): + raw = b"".join(struct.pack("<6i", *row) for row in rows) + actual = hashlib.sha256(raw).hexdigest() + same(actual, expected_sha256, "complete exported record binding") + return actual + + +def full(finite_result, words, output): + output.mkdir(parents=True, exist_ok=False) + inputs = output / "words" + inputs.mkdir() + for label, word in words.items(): + write(inputs / (label + ".json.gz"), word) + N = runpy.run_path(str(HERE / "native.py")) + native = output / "native" + report = N["run"](ROOT, inputs, finite_result["prices"], native) + # Neither unchanged C++ engine uses the ADD phase label in its semantic + # calculation. Bind phases separately; do not infer an H5 theorem. + phase_reports, record_hashes = {}, {} + expected_records = load(HERE / "vendor/pr2115/EXPECTED.json")["census"]["PR1188"]["exporter"] + for label in ("0", "1"): + rows = records(native / label / "records/249-records.bin") + phase_reports[label] = phase_binding(rows, finite_result["phase_ADDs"][label]) + record_hashes[label] = record_binding(rows, expected_records["base" if label == "0" else "deferred"]["record_sha256"]) + same(dict(report[label]["paid_histogram"]), {int(k): v for k, v in PROFILE.items()}, "native profile") + need(report[label]["rank_mass"] == 5129, "native rank mass") + control_root = output / "controls" + control_root.mkdir() + env = {k: v for k, v in os.environ.items() if k != "PYTHONOPTIMIZE"} + results = [] + + def execute(args, log, expect=None): + with log.open("x") as stream: + done = subprocess.run([str(x) for x in args], stdout=stream, stderr=subprocess.STDOUT, env=env) + text = log.read_text() + if expect: + need(done.returncode != 0 and expect in text, "native control failed for wrong reason: " + str(log)) + else: + need(done.returncode == 0, "native positive failed: " + str(log)) + return done.returncode + + hub = ROOT / C["HUB"] + for name in ("missing-undo", "old-scatter", "late-undo"): + word = copy.deepcopy(words["1"]) + if name == "missing-undo": + del word["B"][0] + elif name == "old-scatter": + word["scatter"] = copy.deepcopy(words["0"]["scatter"]) + else: + word["B"] = [word["B"][306]] + word["B"][:306] + word["B"][307:] + folder = control_root / name + folder.mkdir() + path = folder / "word.json.gz" + write(path, word) + lowered, cin, cout = (folder / x for x in ("records", "cin", "cout")) + execute([sys.executable, "-I", "-B", hub / "code/bit/export_records.py", path, lowered], folder / "export.log") + execute([sys.executable, "-I", "-B", hub / "code/bit/regression/stage_cohort.py", lowered, lowered, cin, cout], + folder / "stage.log") + if name == "late-undo": + rc = execute([native / "legality", cin, cout, folder / "legality.json"], folder / "reject.log", + "illegal or mispriced MOVE") + reason = "illegal or mispriced MOVE" + else: + reason = "local defining-decoder full formal column" + rc = execute([native / "columns-4", cout / "COHORT249-RECORDS.bin", folder / "columns.json"], + folder / "reject.log", reason) + results.append(dict(control=name, rejected=True, reason=reason, returncode=rc)) + + # Both native mathematical engines accept changing only 306 phase labels. + # The explicit phase binding must reject it. This names their coverage limit. + folder = control_root / "phase-label-only" + folder.mkdir() + rows = records(native / "1/cout/COHORT249-RECORDS.bin") + seen = 0 + changed = [] + for row in rows: + if row[0] == 1 and row[5] == 4 and seen < 306: + row = row[:5] + (1,) + seen += 1 + changed.append(row) + need(seen == 306, "phase-only mutation count") + source = native / "1/cout" + for path in source.iterdir(): + if path.name.startswith("COHORT249-"): + (folder / path.name).write_bytes(path.read_bytes()) + raw = folder / "COHORT249-RECORDS.bin" + raw.write_bytes(b"".join(struct.pack("<6i", *r) for r in changed)) + execute([native / "legality", native / "1/cin", folder, folder / "legality.json"], folder / "legality.log") + execute([native / "columns-4", raw, folder / "columns.json"], folder / "columns.log") + rejected(lambda: phase_binding(changed, finite_result["phase_ADDs"]["1"]), "phase-only relabel", "exported ADD phases") + rejected(lambda: record_binding(changed, record_hashes["1"]), "phase-only trace", "complete exported record binding") + results.append(dict(control="phase-label-only", native_engines_accept=True, phase_binding_rejects=True, labels_changed=seen)) + # Even preserving all phase counts does not establish the literal trace. + changed = list(rows) + first = next(i for i, r in enumerate(rows) if r[0] == 1 and r[5] == 1) + fourth = next(i for i, r in enumerate(rows) if r[0] == 1 and r[5] == 4) + changed[first] = rows[first][:5] + (4,) + changed[fourth] = rows[fourth][:5] + (1,) + phase_binding(changed, finite_result["phase_ADDs"]["1"]) + rejected(lambda: record_binding(changed, record_hashes["1"]), "count-preserving phase exchange", + "complete exported record binding") + results.append(dict(control="count-preserving-phase-exchange", phase_counts_accept=True, record_binding_rejects=True)) + C["pins"]() + result = dict(status="PASS_R439_DEFERRED_NATIVE", finite_payloads=finite_result["payloads"], + finite_result_sha256=digest(finite_result), native=report, + exported_phase_ADDs=phase_reports, record_sha256=record_hashes, native_controls=results, + native_omitted_bridge_controls=96, new_kappa_claim=False) + write(output / "RESULT.json", result) + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--native", action="store_true") + parser.add_argument("--output", type=Path) + parser.add_argument("--write", action="store_true", help="Explicitly regenerate the appropriate committed receipt") + args = parser.parse_args() + result, words = finite() + target = HERE / "FINITE.json" + if args.write and not args.native: + target.unlink(missing_ok=True) + write(target, result) + else: + same(load(target), result, "finite receipt") + if args.native: + if args.output: + native_result = full(result, words, args.output.resolve()) + else: + with tempfile.TemporaryDirectory(prefix="r439-deferred-") as tmp: + native_result = full(result, words, Path(tmp) / "replay") + target = HERE / "NATIVE.json" + if args.write: + target.unlink(missing_ok=True) + write(target, native_result) + else: + same(load(target), native_result, "native receipt") + print("PASS_R439_DEFERRED_NATIVE words=2 stages=5,9,11 controls=96+5 no_new_kappa") + else: + need(args.output is None, "--output requires --native") + print("PASS_R439_DEFERRED_FINITE columns=661 directions=2 phase_transfer=306 saving=430 no_new_kappa") + + +if __name__ == "__main__": + main()