From dce137e540acd2b689281afe222cd32c0ec1f1ae Mon Sep 17 00:00:00 2001 From: Greer Guthrie <149740518+g-guthrie@users.noreply.github.com> Date: Mon, 12 Oct 2026 22:47:44 -0500 Subject: [PATCH] research: bound selector batching with full volume accounting Prepared with substantial OpenAI Codex assistance. --- .github/workflows/selector-batching.yml | 34 + research/selector-batching/CERTIFICATE.json | 1022 +++++++++++++++++++ research/selector-batching/CLAIM.json | 48 + research/selector-batching/NOTICE.md | 27 + research/selector-batching/README.md | 244 +++++ research/selector-batching/SOURCE-PINS.json | 37 + research/selector-batching/VALIDATION.json | 28 + research/selector-batching/verify.py | 420 ++++++++ 8 files changed, 1860 insertions(+) create mode 100644 .github/workflows/selector-batching.yml create mode 100644 research/selector-batching/CERTIFICATE.json create mode 100644 research/selector-batching/CLAIM.json create mode 100644 research/selector-batching/NOTICE.md create mode 100644 research/selector-batching/README.md create mode 100644 research/selector-batching/SOURCE-PINS.json create mode 100644 research/selector-batching/VALIDATION.json create mode 100644 research/selector-batching/verify.py diff --git a/.github/workflows/selector-batching.yml b/.github/workflows/selector-batching.yml new file mode 100644 index 0000000000..2b5f932e0a --- /dev/null +++ b/.github/workflows/selector-batching.yml @@ -0,0 +1,34 @@ +name: Selector batching exact check + +on: + pull_request: + paths: + - 'research/selector-batching/**' + - '.github/workflows/selector-batching.yml' + push: + paths: + - 'research/selector-batching/**' + - '.github/workflows/selector-batching.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-replay: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + strategy: + matrix: + python-version: ['3.11', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - name: Replay all columns and negative controls, including under optimization + run: | + python3 -I -O -B research/selector-batching/verify.py + git diff --exit-code diff --git a/research/selector-batching/CERTIFICATE.json b/research/selector-batching/CERTIFICATE.json new file mode 100644 index 0000000000..a9fcc64792 --- /dev/null +++ b/research/selector-batching/CERTIFICATE.json @@ -0,0 +1,1022 @@ +{ + "assignment_seed": 22, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "budget": { + "bill_mutations_rejected": [ + "omit_volume_factor", + "omit_selector_cost", + "omit_dirty_restoration" + ], + "f1_complete_ratio": { + "lower": "1999572058995382190519621/1000000000000000000000000", + "upper": "999786029497691095259811/500000000000000000000000" + }, + "f1_even_if_selector_is_free": { + "lower": "1499003977340941911115311/1000000000000000000000000", + "upper": "93687748583808869444707/62500000000000000000000" + }, + "f1_incorrect_unweighted_profile": { + "1": 1, + "3": 1 + }, + "f1_naive_ratio": { + "lower": "99978602949769109525981/100000000000000000000000", + "upper": "999786029497691095259811/1000000000000000000000000" + }, + "f1_original_profile": { + "2": 2 + }, + "f1_volume_weighted_profile": { + "1": 2, + "3": 2 + }, + "fixed_two_lanes": [ + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 3, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 2, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 1, + "ratio_to_original": { + "lower": "1999572058995382190519621/1000000000000000000000000", + "upper": "999786029497691095259811/500000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 5, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 4, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 2, + "ratio_to_original": { + "lower": "375027885950180766263341/250000000000000000000000", + "upper": "300022308760144613010673/200000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 9, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 8, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 4, + "ratio_to_original": { + "lower": "312552373590188176078507/250000000000000000000000", + "upper": "1250209494360752704314029/1000000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 17, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 16, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 8, + "ratio_to_original": { + "lower": "225035801523541321481379/200000000000000000000000", + "upper": "70323687976106662962931/62500000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 33, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 32, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 16, + "ratio_to_original": { + "lower": "1062625945021007428935883/1000000000000000000000000", + "upper": "265656486255251857233971/250000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 65, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 64, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 32, + "ratio_to_original": { + "lower": "1031331022720680638164171/1000000000000000000000000", + "upper": "257832755680170159541043/250000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 257, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 256, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 128, + "ratio_to_original": { + "lower": "503920867453246274360153/500000000000000000000000", + "upper": "1007841734906492548720307/1000000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 2049, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 2048, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 1024, + "ratio_to_original": { + "lower": "125122737453044865181507/125000000000000000000000", + "upper": "1000981899624358921452057/1000000000000000000000000" + } + } + ], + "interpretation": "Comparison of inherited cost bounds, not a lower bound on actual algorithms.", + "sigma": "39934471731507676525497/40000000000000000000000", + "two_lanes_with_slot_scaled_selector": [ + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 2, + 3, + "joined transform" + ], + [ + 2, + 1, + "inverse selector" + ] + ], + "data_axes": 2, + "joined_volume_over_V": 2, + "selector_axes": 1 + }, + "f": 1, + "ratio_to_original": { + "lower": "1999572058995382190519621/1000000000000000000000000", + "upper": "999786029497691095259811/500000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 4, + 6, + "joined transform" + ], + [ + 4, + 2, + "inverse selector" + ], + [ + 2, + 4, + "dirty padding restoration" + ] + ], + "data_axes": 4, + "joined_volume_over_V": 4, + "selector_axes": 2 + }, + "f": 2, + "ratio_to_original": { + "lower": "2499572058995382190519621/500000000000000000000000", + "upper": "4999144117990764381039243/1000000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 8, + 9, + "joined transform" + ], + [ + 8, + 3, + "inverse selector" + ], + [ + 6, + 6, + "dirty padding restoration" + ] + ], + "data_axes": 6, + "joined_volume_over_V": 8, + "selector_axes": 3 + }, + "f": 3, + "ratio_to_original": { + "lower": "2199657647196305752415697/200000000000000000000000", + "upper": "5499144117990764381039243/500000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 16, + 12, + "joined transform" + ], + [ + 16, + 4, + "inverse selector" + ], + [ + 14, + 8, + "dirty padding restoration" + ] + ], + "data_axes": 8, + "joined_volume_over_V": 16, + "selector_axes": 4 + }, + "f": 4, + "ratio_to_original": { + "lower": "22996576471963057524156971/1000000000000000000000000", + "upper": "5749144117990764381039243/250000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 32, + 15, + "joined transform" + ], + [ + 32, + 5, + "inverse selector" + ], + [ + 30, + 10, + "dirty padding restoration" + ] + ], + "data_axes": 10, + "joined_volume_over_V": 32, + "selector_axes": 5 + }, + "f": 5, + "ratio_to_original": { + "lower": "46993152943926115048313943/1000000000000000000000000", + "upper": "5874144117990764381039243/125000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 64, + 18, + "joined transform" + ], + [ + 64, + 6, + "inverse selector" + ], + [ + 62, + 12, + "dirty padding restoration" + ] + ], + "data_axes": 12, + "joined_volume_over_V": 64, + "selector_axes": 6 + }, + "f": 6, + "ratio_to_original": { + "lower": "94986305887852230096627887/1000000000000000000000000", + "upper": "5936644117990764381039243/62500000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 128, + 21, + "joined transform" + ], + [ + 128, + 7, + "inverse selector" + ], + [ + 126, + 14, + "dirty padding restoration" + ] + ], + "data_axes": 14, + "joined_volume_over_V": 128, + "selector_axes": 7 + }, + "f": 7, + "ratio_to_original": { + "lower": "95486305887852230096627887/500000000000000000000000", + "upper": "7638904471028178407730231/40000000000000000000000" + } + }, + { + "bill": { + "active_lanes": 2, + "calls": [ + [ + 256, + 24, + "joined transform" + ], + [ + 256, + 8, + "inverse selector" + ], + [ + 254, + 16, + "dirty padding restoration" + ] + ], + "data_axes": 16, + "joined_volume_over_V": 256, + "selector_axes": 8 + }, + "f": 8, + "ratio_to_original": { + "lower": "95736305887852230096627887/250000000000000000000000", + "upper": "382945223551408920386511549/1000000000000000000000000" + } + } + ] + }, + "operator_mutations_rejected": [ + { + "name": "omit_selector", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 3, + "actual_numerator": [ + -2, + 2 + ], + "column": 0, + "expected_denominator_power": 2, + "expected_numerator": [ + 0, + 2 + ], + "row": 0 + } + }, + { + "name": "forward_selector", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 4, + "actual_numerator": [ + 0, + 0 + ], + "column": 0, + "expected_denominator_power": 2, + "expected_numerator": [ + 0, + 2 + ], + "row": 0 + } + }, + { + "name": "wrong_selector_axis", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 4, + "actual_numerator": [ + 0, + 0 + ], + "column": 0, + "expected_denominator_power": 2, + "expected_numerator": [ + 2, + 0 + ], + "row": 1 + } + }, + { + "name": "wrong_global_phase", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 4, + "actual_numerator": [ + -8, + 0 + ], + "column": 0, + "expected_denominator_power": 2, + "expected_numerator": [ + 0, + 2 + ], + "row": 0 + } + }, + { + "name": "wrong_normalization", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 4, + "actual_numerator": [ + 0, + 16 + ], + "column": 0, + "expected_denominator_power": 2, + "expected_numerator": [ + 0, + 2 + ], + "row": 0 + } + }, + { + "name": "omit_padding_restoration", + "rejected_by": "full operator identity", + "witness": { + "actual_denominator_power": 6, + "actual_numerator": [ + 0, + 32 + ], + "column": 12, + "expected_denominator_power": 2, + "expected_numerator": [ + 4, + 0 + ], + "row": 12 + } + } + ], + "operator_replays": [ + { + "active_lanes": 2, + "all_columns": 4, + "data_axes": 1, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 4, + "reference_matrix_sha256": "9123faf6c87b00ab926fae2e1a4565970cb14135f540c2582af81dc4678cc21a", + "selector_axes": 1, + "target_active_row_support": 2 + }, + { + "active_lanes": 2, + "all_columns": 4, + "data_axes": 1, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 4, + "reference_matrix_sha256": "2352b220b6eb19a587368175ecc7e29ca3a32cd4768d65d0e44b86fab4de80bb", + "selector_axes": 1, + "target_active_row_support": 2 + }, + { + "active_lanes": 4, + "all_columns": 8, + "data_axes": 1, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 8, + "reference_matrix_sha256": "a6bfd29582825e923f9af20e2f8bad081a5851fd68a573b8b9137d5d110d3184", + "selector_axes": 2, + "target_active_row_support": 2 + }, + { + "active_lanes": 4, + "all_columns": 8, + "data_axes": 1, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 8, + "reference_matrix_sha256": "6e80686a2c285d3008b963a4dabb4c5045a0548c5aa70cb4252e4884dce2317f", + "selector_axes": 2, + "target_active_row_support": 2 + }, + { + "active_lanes": 2, + "all_columns": 8, + "data_axes": 2, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 8, + "reference_matrix_sha256": "8610d69f465a474b18f24fdba67b4af299520105f7ad7d6dfd199d761124549f", + "selector_axes": 1, + "target_active_row_support": 4 + }, + { + "active_lanes": 2, + "all_columns": 8, + "data_axes": 2, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 8, + "reference_matrix_sha256": "7a14959f5fa70fd9188823342b31b3d2c02cd0344896328b041d1db162620931", + "selector_axes": 1, + "target_active_row_support": 4 + }, + { + "active_lanes": 4, + "all_columns": 16, + "data_axes": 2, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 16, + "reference_matrix_sha256": "3112f1b0127138b925c6e9a6c641f4d7d3ec2798b6a232906ace70fac24521fb", + "selector_axes": 2, + "target_active_row_support": 4 + }, + { + "active_lanes": 4, + "all_columns": 16, + "data_axes": 2, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 16, + "reference_matrix_sha256": "f506f1b0a92395fdddd2e293e32c646edac77239faf843cdc8d67622ecd0465d", + "selector_axes": 2, + "target_active_row_support": 4 + }, + { + "active_lanes": 2, + "all_columns": 16, + "data_axes": 3, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 16, + "reference_matrix_sha256": "c96690b6581ddb406df2140803fa5339786a4d27a4a08d2f66e502cd93cdfd7d", + "selector_axes": 1, + "target_active_row_support": 8 + }, + { + "active_lanes": 2, + "all_columns": 16, + "data_axes": 3, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 16, + "reference_matrix_sha256": "a3c6d560029c708d1b49be2acc562bf098726cc83fbbd42ba29e7013edbe47ac", + "selector_axes": 1, + "target_active_row_support": 8 + }, + { + "active_lanes": 4, + "all_columns": 32, + "data_axes": 3, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 32, + "reference_matrix_sha256": "dcead21a30018401ca2b88309938f78b4de5990c33a3d8cdca0f1fb2e5db2513", + "selector_axes": 2, + "target_active_row_support": 8 + }, + { + "active_lanes": 4, + "all_columns": 32, + "data_axes": 3, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 32, + "reference_matrix_sha256": "1151132acbfea803ae4175fbed16b385b11c5322cb1077553d8376bf54232083", + "selector_axes": 2, + "target_active_row_support": 8 + }, + { + "active_lanes": 2, + "all_columns": 32, + "data_axes": 4, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 32, + "reference_matrix_sha256": "49f9a3fb4ae5ac1e4d48ad12ac1be33511a516466b4b9dbbb1f6ff94d44d57ca", + "selector_axes": 1, + "target_active_row_support": 16 + }, + { + "active_lanes": 2, + "all_columns": 32, + "data_axes": 4, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 32, + "reference_matrix_sha256": "657569137f1a9d4abcea39ec64c169cf5793d9a1f02847c127faa88d02d36ee2", + "selector_axes": 1, + "target_active_row_support": 16 + }, + { + "active_lanes": 4, + "all_columns": 64, + "data_axes": 4, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 64, + "reference_matrix_sha256": "18ba970d1fbc9b84c1704a4f42bf922d18d80b5c47b94f0d92db8daae9ec47d3", + "selector_axes": 2, + "target_active_row_support": 16 + }, + { + "active_lanes": 4, + "all_columns": 64, + "data_axes": 4, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 64, + "reference_matrix_sha256": "af250647eb16c49e3e0749c712506b290b022cbec55d3f4936c4f1a90653f514", + "selector_axes": 2, + "target_active_row_support": 16 + }, + { + "active_lanes": 2, + "all_columns": 64, + "data_axes": 5, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 64, + "reference_matrix_sha256": "c5816e5245a5276e3e893db9d9ffed174f1b1697fb6c4985352e35e46fb5a737", + "selector_axes": 1, + "target_active_row_support": 32 + }, + { + "active_lanes": 2, + "all_columns": 64, + "data_axes": 5, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 64, + "reference_matrix_sha256": "5ce3f10b55136441f3dfff42cd9bbbe245cf4bcf1f59fceebe8800b3d298d55a", + "selector_axes": 1, + "target_active_row_support": 32 + }, + { + "active_lanes": 4, + "all_columns": 128, + "data_axes": 5, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 128, + "reference_matrix_sha256": "3bb8a73db24a76123bd5f4a93a91e7ba39ba080326d38be41760d68dee13a318", + "selector_axes": 2, + "target_active_row_support": 32 + }, + { + "active_lanes": 4, + "all_columns": 128, + "data_axes": 5, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 128, + "reference_matrix_sha256": "dadb1ba389f30ea817aeda6002e6f0201a3b1f2bdac4d162c3fc38190a6ab5c8", + "selector_axes": 2, + "target_active_row_support": 32 + }, + { + "active_lanes": 2, + "all_columns": 128, + "data_axes": 6, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 128, + "reference_matrix_sha256": "84a937741c145364179510b11bd857fc361a993e6149aac39a6bd281193b3738", + "selector_axes": 1, + "target_active_row_support": 64 + }, + { + "active_lanes": 2, + "all_columns": 128, + "data_axes": 6, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 128, + "reference_matrix_sha256": "4c2d4249b90ef52cd4e9a17318847fe7db886b0737e37461179d94a8f695a632", + "selector_axes": 1, + "target_active_row_support": 64 + }, + { + "active_lanes": 4, + "all_columns": 256, + "data_axes": 6, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 256, + "reference_matrix_sha256": "50ba4fcde53590d96c2957dc762c6e26a530531112f7c6df9962a2acff363cd7", + "selector_axes": 2, + "target_active_row_support": 64 + }, + { + "active_lanes": 4, + "all_columns": 256, + "data_axes": 6, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 256, + "reference_matrix_sha256": "acff3d606195c2a3f5b73d9f72c74b5d79a63a7fb0229d5a69e1789312ac8f33", + "selector_axes": 2, + "target_active_row_support": 64 + }, + { + "active_lanes": 3, + "all_columns": 8, + "data_axes": 1, + "direction": 1, + "dirty_padding_columns": 2, + "raw_row_support": 8, + "reference_matrix_sha256": "855f61b71df78845ab09a851a0c082fa6eaf11ee4b47062820199aee74fe07a1", + "selector_axes": 2, + "target_active_row_support": 2 + }, + { + "active_lanes": 3, + "all_columns": 8, + "data_axes": 1, + "direction": -1, + "dirty_padding_columns": 2, + "raw_row_support": 8, + "reference_matrix_sha256": "ebb73aeace6fb44e1e918efc5c4147105adfc860d856ffbbc84baf589b6ccb51", + "selector_axes": 2, + "target_active_row_support": 2 + }, + { + "active_lanes": 3, + "all_columns": 16, + "data_axes": 2, + "direction": 1, + "dirty_padding_columns": 4, + "raw_row_support": 16, + "reference_matrix_sha256": "f017cfed7f0eb2f9d8c611efc7c29a24e91e48cec530d6ce94c2e830b9e47784", + "selector_axes": 2, + "target_active_row_support": 4 + }, + { + "active_lanes": 3, + "all_columns": 16, + "data_axes": 2, + "direction": -1, + "dirty_padding_columns": 4, + "raw_row_support": 16, + "reference_matrix_sha256": "53aa7304d7b7e2577d5d5d25194168f5cf9f5addeb36b7d104298423537b7b6e", + "selector_axes": 2, + "target_active_row_support": 4 + }, + { + "active_lanes": 3, + "all_columns": 32, + "data_axes": 3, + "direction": 1, + "dirty_padding_columns": 8, + "raw_row_support": 32, + "reference_matrix_sha256": "cad2def73f8825c7eff62b51d948b0f4b6096f4e2cb543546817c0d42578b64f", + "selector_axes": 2, + "target_active_row_support": 8 + }, + { + "active_lanes": 3, + "all_columns": 32, + "data_axes": 3, + "direction": -1, + "dirty_padding_columns": 8, + "raw_row_support": 32, + "reference_matrix_sha256": "e8f043b068708f8470afd5ee295b97f11d0f46f34feaa295b1bc9e2ae11f5865", + "selector_axes": 2, + "target_active_row_support": 8 + }, + { + "active_lanes": 3, + "all_columns": 64, + "data_axes": 4, + "direction": 1, + "dirty_padding_columns": 16, + "raw_row_support": 64, + "reference_matrix_sha256": "902ff171bc64a9820ff575edc73f8eb19d80849902a42d8b3e927f95f96c8c18", + "selector_axes": 2, + "target_active_row_support": 16 + }, + { + "active_lanes": 3, + "all_columns": 64, + "data_axes": 4, + "direction": -1, + "dirty_padding_columns": 16, + "raw_row_support": 64, + "reference_matrix_sha256": "c3705d7e991f3f518cc1d890d88f0d356593555710882cd7cd705912e2ac9a61", + "selector_axes": 2, + "target_active_row_support": 16 + }, + { + "active_lanes": 2, + "all_columns": 512, + "data_axes": 8, + "direction": 1, + "dirty_padding_columns": 0, + "raw_row_support": 512, + "reference_matrix_sha256": "23cf439c4b50fbe78fe6076a43c4fdc8b3deef644af319c3d13d0b02be23910a", + "selector_axes": 1, + "target_active_row_support": 256 + }, + { + "active_lanes": 2, + "all_columns": 512, + "data_axes": 8, + "direction": -1, + "dirty_padding_columns": 0, + "raw_row_support": 512, + "reference_matrix_sha256": "0751137ca29c30353c9d09106b290fbf460fd99b5920022f5ec7c1de5ad52f43", + "selector_axes": 1, + "target_active_row_support": 256 + } + ], + "schema": "selector-batching/1", + "scope": "Finite exact evidence plus the written all-size bound comparison in README.md; no new kappa or full theorem verification.", + "status": "PASS_SELECTOR_BATCHING_IDENTITIES_AND_VOLUME_OBSTRUCTION", + "supplier_reference": { + "accepted_kappa_at_base": "51110230636731/31250000000000000", + "complex_saving": "65528268492323474503/40000000000000000000000", + "eligible_consecutive_pairs": 32, + "paid_profiles": { + "backward": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "forward": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + } + }, + "program_payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "provider": "jp8", + "scope": "Reads pinned native receipts; does not rerun the full supplier or assert legal co-scheduling.", + "seed_selected_pair": [ + [ + 14512, + [ + "climb", + "B", + 159, + 525, + 526, + 2 + ] + ], + [ + 14513, + [ + "climb", + "B", + 25, + 524, + 526, + 2 + ] + ] + ], + "seed_selected_rank": 2, + "sigma": "39934471731507676525497/40000000000000000000000", + "supplier_pr": 626 + }, + "total_dirty_padding_columns": 60, + "total_exact_columns": 2776, + "total_exact_matrix_entries": 753568 +} diff --git a/research/selector-batching/CLAIM.json b/research/selector-batching/CLAIM.json new file mode 100644 index 0000000000..7ab0a342cc --- /dev/null +++ b/research/selector-batching/CLAIM.json @@ -0,0 +1,48 @@ +{ + "track": "Complex supplier", + "assignment_seed": 22, + "random_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_at_utc": "2026-10-13T03:21:13.972500+00:00", + "claim_recorded_at_utc": "2026-10-13T03:28:00.082427+00:00", + "expected_finish_at_utc": "2026-10-13T04:01:00+00:00", + "coordination": "No pinned sprint coordination issue; only open issue #650 requests Discussions. Claim recorded locally.", + "open_prs_inspected": 487, + "max_open_pr_number": 667, + "candidates": [ + { + "task": "More signed K-triangle packet elimination", + "disposition": "Not selected: pending PR646 already measures the eight-triangle R480 construction and its unfavorable complete profile." + }, + { + "task": "Target-hosted face delivery", + "disposition": "Not selected: pending PR651 studies the delivery-layer rigidity and prior PR571 factory bound." + }, + { + "task": "Volume-aware selector-axis batching of equal-rank complex children", + "disposition": "Selected: no matching open PR scope found. Distinct from within-array tensor batching in notes/batched-complex-rows.tex, PR451 split-residual routing, and PR665 spectral dilation." + } + ], + "object": "Two rank-2 paid climbs from the accepted PR626 jp8 forward local program; selector-axis pooling into one larger C tensor.", + "seed_diversification": "Even seed selects jp8; 22 mod 7 selects rank 2 from sorted nonzero paid ranks; 22 mod 32 selects consecutive equal-rank climbs feeding one addition (events 14512 and 14513).", + "hypothesis": "A single larger tensor call could reduce the paid complex recursion profile for multiple independent equal-width streams.", + "method": "Exact Gaussian-dyadic operator replay; closed-form tensor-entry reference; complete volume-weighted recurrence including inverse selector and restoration of padded dirty lanes. Grant legal co-scheduling and routing optimistically.", + "expected_deliverable": "One source-pinned research note and reproducible exact certificate with meaningful mutation controls. No kappa claim if even the favorable complete budget loses.", + "stopping_rule": "Stop construction search once the complete optimistic bound cannot improve; verify the scoped obstruction and package it. Reserve at least the final quarter for verification/handoff.", + "status": "completed", + "completed_at_utc": "2026-10-13T03:44:46.002191+00:00", + "result": "Scoped negative result. Exact selector circuit and dirty padding repair pass; the complete volume-weighted recursive budget cannot improve the equal-width calls. No new kappa.", + "verification": { + "operator_cases": 34, + "exact_columns": 2776, + "exact_matrix_entries": 753568, + "dirty_padding_columns": 60, + "operator_controls": 6, + "invoice_controls": 3 + }, + "presubmission_overlap_check": { + "open_prs": 495, + "through_pr": 675, + "result": "No matching selector-batching scope found. New PR673 concerns nonlinear dirty echo composition; PR675 concerns owner windows and bridges." + } +} diff --git a/research/selector-batching/NOTICE.md b/research/selector-batching/NOTICE.md new file mode 100644 index 0000000000..8b3f012950 --- /dev/null +++ b/research/selector-batching/NOTICE.md @@ -0,0 +1,27 @@ +# Attribution and license + +Prepared by **Greer Guthrie (g-guthrie)** with substantial **OpenAI Codex** +assistance in research, implementation, exact checks and writing. +New material is licensed under the repository's Apache-2.0 license. + +This experiment reads existing source files in place and retains their +original notices. It does not redistribute a modified supplier or claim +credit for the accepted construction. + +- Jeremy Kothe: #622/#623 K-triangle provider construction and schedules. +- Chafik Boukhalfa (chafreaky): #626 owner repair and independent invoice. +- eumemic: the #543 bit supplier retained by the accepted record. +- icekylinx: the native complex circuit/Clifford machinery, normal forms, + compiler lineage, and signed whole-residual batching. +- DreamingOfClouds: the cold-helper and native residual-wrapper lineage. +- Rohan Arun and the other predecessors credited in the selected maintainer + review: the complete native complex recurrence and supplier accounting. +- The original OpenAI manuscript and repository contributors: the complex + kernel and weighted, volume-linear recursion framework. + +Related work consulted for scope: Dominik Scholz's #571 packet-factory +obstruction, Jeremy Diviney's #646 signed K-triangles, higherbeing's #651 +delivery rigidity, chafreaky's #451 split-residual audit, and +Mister-Meeseeks's #665 spectral-dilation note. No code from those pending +PRs is copied here. The simple tensor factorization and support argument +are standard linear algebra, with no originality claim. diff --git a/research/selector-batching/README.md b/research/selector-batching/README.md new file mode 100644 index 0000000000..167f5ca029 --- /dev/null +++ b/research/selector-batching/README.md @@ -0,0 +1,244 @@ +# Selector batching of equal-rank complex children: the volume charge + +**Scoped negative result; no new κ or supplier.** A pair of paid rank-2 +children in the accepted #626 complex supplier suggests the replacement +`2 C_2 -> C_3 + C_1`. That unweighted profile appears to improve the moment. +The actual joined array has twice the volume: its profile in units of one +original stream is **`2 C_3 + 2 C_1`**. The tempting saving disappears. + +This note supplies an exact circuit, arbitrary-dirty-padding restoration, +an all-size comparison of the inherited cost bounds, and an independently +implemented finite checker. It does not claim that batching is impossible +or that these bounds are lower bounds on actual execution time. + +## Reproduce + +From this repository, using Python 3.11 or later and only its standard library: + +```sh +python3 -B research/selector-batching/verify.py +``` + +Expected first line: + +```text +PASS_SELECTOR_BATCHING_IDENTITIES_AND_VOLUME_OBSTRUCTION +``` + +The command takes about three seconds on the contributor's macOS machine. +It checks every pinned source, reconstructs both native paid histograms and +the seed-selected pair, replays 34 complete finite operators against closed +Kronecker entries, rejects six operator and three invoice mutations, and +compares the entire result with [CERTIFICATE.json](CERTIFICATE.json). +There are 2,776 basis columns / 753,568 matrix entries, including 60 arbitrary +dirty-padding columns. Assertions are not used as admission predicates; +`python3 -I -O -B research/selector-batching/verify.py` also checks them. +`--output /path/to/new-receipt.json` optionally writes a fresh identical receipt. +The [local validation receipt](VALIDATION.json) records an optimized replay +from a relocated minimal checkout with a recompressed source, plus rejection +of a changed native source and a corrupted expected certificate. The selected +record's separate inventory/proof binding check also passed. + +## Exact reference and task selection + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +At that base the maintainer-reviewed record is #626 with #543, conditional +`κ = 51110230636731/31250000000000000`. This note does not change that record. + +The operating-system draw was **22**, assigning the complex-supplier track. +Three candidates were considered: more K-triangles, target-hosted face +delivery, and selector-axis batching. Pending #646 already measures the +eight-triangle construction; #651 investigates delivery rigidity. The third +scope was selected after inspecting 487 open PRs through #667, the review +ledger and the negative-result archive. No pinned coordination issue existed; +[CLAIM.json](CLAIM.json) records the local claim and stopping rule. + +The even seed selects `jp8`; `22 mod 7` selects rank 2 from its sorted paid +ranks. Among the 32 consecutive equal-rank climb pairs feeding one addition, +pair 22 consists of these zero-based forward-program events: + +```text +14512: ['climb', 'B', 159, 525, 526, 2] +14513: ['climb', 'B', 25, 524, 526, 2] +``` + +The following scalar adds register 25 into register 159. The stored native +`jp8` profile in each orientation is +`{1:2512, 2:400, 3:448, 4:160, 5:70, 6:8, 8:8}`. This is a pair of **paid +climbs**, not a pair of helper-width entries incorrectly added to the invoice. +The exact local program and SPEC are bound in [SOURCE-PINS.json](SOURCE-PINS.json). +The gzip input is pinned by its complete decompressed payload; container +headers are not mathematical evidence. These are retained native receipts, +not a new cold replay of the whole supplier. + +The two residuals have different frame transitions. For the proposed cost +comparison we grant legal co-scheduling and their reduction to identical +coordinate normal forms, without charging extra frame wrappers or routing. +This is deliberately favorable to batching. No replacement of these events +in the actual scalar word is asserted to be legal or implemented. + +## The literal operator + +Use the repository's complex kernel + +```text +C = ((1+i) I + (1-i) X)/2, C_d = C tensor ... tensor C (d factors). +``` + +`C_0 = I`. The pinned Clifford implementation and signed-child note use +this convention. For `n >= 1`, join `q = 2^s` lanes, each with `2^n` +active coordinates; additional spectator fibers are unchanged. The lane +index is the high `s` bits. The desired operation on all lanes is +`I_q tensor C_n`. The exact circuit is + +```text +(C_s^-1 tensor I) C_(n+s) = I_q tensor C_n. +``` + +The full transform runs first, then the inverse selector. This follows +from the tensor-product identity `C_(n+s) = C_s tensor C_n`, so it holds +for every size and every input, not just the finite replays. The inverse +selector is itself a recursive complex operation. It can use the existing +forward-child convention `C_s^-1 = (-i)^s Z_S C_s Z_S`: one width-s child, +two address-sign passes, and the exact global phase. The checker executes +the conjugated Gaussian coefficients directly and checks both directions. + +**Monomial routing alone cannot supply the inverse selector.** Every entry +of `C_(n+s)` is nonzero, whereas a row of `I_q tensor C_n` has only `2^n` +nonzeros. Invertible monomial pre/post maps preserve the number of nonzero +entries per row (up to row permutation). For `s > 0` these support counts +differ. This excludes a single dense tensor child with only permutations +and nonzero diagonal scalings around it, even if those maps mix lane and +data coordinates. It does not exclude a nonmonomial encoding or additional +arithmetic. The tensor factorization and support argument are the written +all-size arguments; the finite checker is not a formal proof of them. + +### Arbitrarily dirty padding + +For `k < q` useful lanes, the other `q-k` lanes cannot be assumed zero. +After the two operations above every padded lane also contains `C_n z`. +Apply `C_n^-1` on each unused lane to restore its arbitrary initial value. +The complete endpoint is then + +```text +(I_k tensor C_n) direct-sum I_((q-k) 2^n). +``` + +The checker includes `k=3, q=4` and propagates every initial padding column. +Omitting restoration leaves the useful outputs correct but corrupts padding; +its negative control specifically fails on a dirty input column. No clean +workspace assumption is hidden in the correct operator. + +## Complete recursive bill and all-size comparison + +Let `V` be one original lane's volume, including its spectator fibers. +Use the same inherited normalized child cost bound `A V d^sigma`, with +`0 < sigma < 1`, for every call. The volume factor is essential: a routine +acting on the joined array sees **`qV`**, not `V`. + +| Operation | Width | Volume in units of V | +|---|---:|---:| +| Original k independent children | n | k | +| Joined tensor child | n+s | q | +| Inverse selector child | s | q | +| Restore dirty padding | n | q-k | + +Thus the literal proposal substitutes the recursive budget + +```text +B_original = A V k n^sigma +B_joined = A V [q (n+s)^sigma + q s^sigma + (q-k) n^sigma] + E. +``` + +`E` denotes nonnegative gather/scatter and source-access work, coordinate +and frame changes, sign/phase passes, coefficient temporaries and their +restoration, and descriptor/precision work. The joined operation needs +`q` full lane volumes, including `q-k` padded ones. The finite circuit uses +no other logical lane; it is not a fixed-tape implementation or a new +proof of the inherited realization contract. We grant all work in `E` +for free here. The recursive bill alone already rejects the hypothesis, +so implementing or estimating those costs more closely cannot rescue this +particular bound comparison. For a constant-size selector one may instead +use direct butterflies; granting the entire selector operation for free +is even more favorable and gives the same conclusion. + +Indeed `q >= k`, `s > 0` and `sigma > 0` imply + +```text +q (n+s)^sigma > k n^sigma. +``` + +Even the joined child alone exceeds the original numerical budget under +the same cost model. This is an inequality between available upper-bound +expressions, **not** a lower bound on the optimal cost of either operator. + +Two scaling regimes must be distinguished: + +1. **A fixed number of streams.** For the selected pair, `k=q=2`, `s=1` + and `n=2f`. The ratio is + `(1+1/(2f))^sigma + (1/(2f))^sigma > 1`, tending to 1 as `f` grows. + The leading moment contribution stays `2 * 2^sigma`. It does not become + `3^sigma + 1`. A finite positive overhead must not be described as a + strictly larger leading exponent; the asymptotic leading budget ties. +2. **A selector slot scaled with f.** To obtain the ranks `3f` and `f` + literally, one needs `s=f` selector bits, hence `q=2^f` lanes. Keeping + only two useful lanes introduces `2^f-2` dirty padded lanes. Already + the joined-child ratio is `2^(f-1) (3/2)^sigma > 1`; restoration adds + further work. Ignoring that growing volume is not a uniform compiler. + +The fixed-lane argument also applies group by group to any partition into +equal-width batches. It does not cover fusing genuinely consecutive +operators on the same stream, changing the scalar network or owner map, +or a different recursion algorithm with independently proved costs. + +### The false gain at the current supplier exponent + +Use the source-bound complex endpoint +`b = 65528268492323474503/40000000000000000000000`, `sigma = 1-b`. +At `f=1`, the ratios to the original two calls are: + +| Accounting | Ratio (rounded for display) | +|---|---:| +| Incorrect unweighted `C_3 + C_1` | 0.999786029497691095 | +| Complete volume-weighted `2 C_3 + 2 C_1` | 1.999572058995382190 | +| Joined child alone; inverse selector and all other work free | 1.499003977340941911 | + +The wrong profile preserves the apparent rank mass (`3+1 = 2+2`) and +therefore looks particularly plausible. The real volume-weighted mass is +`2*3 + 2*1 = 8`, versus 4 originally. The displayed decimals are backed by +exact rational enclosures in the certificate, using atanh/Taylor remainder +bounds. Square-root probes independently check the enclosure routine by +squaring its endpoints. No floating-point search or solver claim is used. + +## Coverage, controls and limits + +The finite domain is all columns in both directions for `n=1..6, s=1..2, +k=2^s`; `n=1..4, s=2, k=3`; and `n=8, s=1, k=2`. The deterministic stopping +rule is completion of these 34 cases, the rational fixed-lane screens +`f in {1,2,4,8,16,32,128,1024}`, and slot-scaled screens `f=1..8`. +The infinite-size comparison comes from the displayed inequalities, +not from extrapolating these finite cases. + +Negative controls remove the selector, use its wrong direction, act on +the wrong axis, change the global phase or normalization, omit dirty +restoration, omit joined volume, omit selector cost, and omit restoration +cost. The first six retain concrete failing matrix entries. The operator +engine uses Gaussian integer butterfly updates; its reference computes +each Kronecker entry as a product of `(1+i)` and `(1-i)`, independently. +No supplier verifier is changed, imported, or weakened. + +This note adds a current-source-bound counterexample to unweighted +cross-stream batching, a padding repair, and a uniform scaling diagnosis. +The historical [sparse fusion audit](../../docs/research/sparse-fusion-audit.md) +already rejects partitioning one active-position set into separately charged +batches. The [signed whole-residual construction](../../notes/batched-complex-rows.tex) +instead combines tensor factors **within the same array volume** and is +unaffected. PR451's split-residual obstruction and PR665's spectral-dilation +experiment concern different interfaces. No claim of priority for the +elementary tensor identity or linear-volume accounting is made. + +Local validation does not include a full supplier replay, repository-wide +`make verify`, Linux CI or Lean. The focused Linux workflow reports its status +separately on the PR. This package supplies no new owner assignment, tape +realization, precision/recovery theorem or improved multiplication exponent. +See [NOTICE.md](NOTICE.md) for attribution and assistance disclosure. diff --git a/research/selector-batching/SOURCE-PINS.json b/research/selector-batching/SOURCE-PINS.json new file mode 100644 index 0000000000..15d74c93ef --- /dev/null +++ b/research/selector-batching/SOURCE-PINS.json @@ -0,0 +1,37 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": { + "docs/research/community-k492-review.md": { + "representation": "file-bytes", + "sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + }, + "docs/research/sparse-fusion-audit.md": { + "representation": "file-bytes", + "sha256": "631c852e068adf8d2943bf8f7373d822f423c2180ed0c8d413188a30ff51d75a" + }, + "notes/batched-complex-rows.tex": { + "representation": "file-bytes", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": { + "representation": "gzip-payload", + "sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b" + }, + "research/complex-k492-owner-repair/code/hpe_adapters_local.py": { + "representation": "file-bytes", + "sha256": "eb0b5c6c7161e18dc22168da3211448d321586edd15bcfb4b4741174d36993cf" + }, + "research/complex-k492-owner-repair/code/hpe_emit_local.py": { + "representation": "file-bytes", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + "research/complex-k492-owner-repair/data/SPEC.json": { + "representation": "file-bytes", + "sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + }, + "research/complex-multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/vendor/clifford/clifford_exact.py": { + "representation": "file-bytes", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + } +} diff --git a/research/selector-batching/VALIDATION.json b/research/selector-batching/VALIDATION.json new file mode 100644 index 0000000000..21abdcd5c5 --- /dev/null +++ b/research/selector-batching/VALIDATION.json @@ -0,0 +1,28 @@ +{ + "platform": "macOS-26.4.1-arm64-arm-64bit-Mach-O", + "python": "3.14.6", + "checks": [ + { + "check": "relocated minimal checkout with a recompressed source", + "exit_code": 0, + "evidence": "PASS_SELECTOR_BATCHING_IDENTITIES_AND_VOLUME_OBSTRUCTION", + "seconds": 2.53 + }, + { + "check": "corrupted native source rejected under -I -O", + "exit_code": 1, + "evidence": "source pin mismatch: research/complex-k492-owner-repair/data/SPEC.json", + "seconds": 0.055 + }, + { + "check": "corrupted expected certificate rejected under -I -O", + "exit_code": 1, + "evidence": "recomputed certificate differs from CERTIFICATE.json", + "seconds": 2.548 + } + ], + "normal_replay": "PASS (separately run)", + "optimized_replay": "PASS (separately run)", + "scope": "Local standalone package checks, not a fresh full supplier replay or repository-wide suite.", + "selected_record_check": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" +} diff --git a/research/selector-batching/verify.py b/research/selector-batching/verify.py new file mode 100644 index 0000000000..3c1b207509 --- /dev/null +++ b/research/selector-batching/verify.py @@ -0,0 +1,420 @@ +#!/usr/bin/env python3 +"""Exact, volume-aware selector batching experiment. Apache-2.0. + +Prepared by Greer Guthrie with substantial OpenAI Codex assistance. +This checks finite identities and a bound comparison, not a multiplication theorem. +No implementation from the supplier's Clifford checker is imported. +""" + +import argparse +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +BASE = "66849e1475c930fd7732b1a0067ffee7e1e95f60" +SEED = 22 +SUPPLIER = "research/complex-k492-owner-repair/data/SPEC.json" +PROGRAM = ("research/community-k492-audit/pr626/replay/mixed-global/base/" + "providers/jp8/LOCAL-PROGRAMS.json.gz") +STATUS = "PASS_SELECTOR_BATCHING_IDENTITIES_AND_VOLUME_OBSTRUCTION" + + +class VerificationError(Exception): + pass + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def source_bytes(root, relative, pin): + data = (root / relative).read_bytes() + if pin["representation"] == "gzip-payload": + data = gzip.decompress(data) + else: + require(pin["representation"] == "file-bytes", "unknown source representation") + require(hashlib.sha256(data).hexdigest() == pin["sha256"], + "source pin mismatch: " + relative) + return data + + +def check_sources(root): + pins = json.loads((HERE / "SOURCE-PINS.json").read_text()) + require(pins["base_commit"] == BASE, "wrong base commit") + return {name: source_bytes(root, name, pin) for name, pin in pins["files"].items()} + + +def supplier_reference(sources): + spec = json.loads(sources[SUPPLIER]) + programs = json.loads(sources[PROGRAM]) + profiles = {} + for orientation, events in sorted(programs.items()): + # These are the two paid event forms emitted by hpe_emit_local.py. + profile = Counter() + for event in events: + if event[0] == "climb": + require(len(event) == 6, "malformed climb") + profile[event[5]] += 1 + elif event[0] == "center": + require(len(event) == 5, "malformed center") + profile[event[4]] += 1 + profile = dict(sorted(profile.items())) + require(profile == {int(r): count for r, count in + spec["providers"]["jp8"]["expected_profile"].items()}, + "native paid profile does not match the supplier") + profiles[orientation] = {str(r): count for r, count in profile.items()} + require(set(profiles) == {"backward", "forward"}, "missing orientation") + ranks = sorted(map(int, profiles["forward"])) + rank = ranks[SEED % len(ranks)] + events = programs["forward"] + pairs = [] + for i, event in enumerate(events[:-2]): + following = events[i + 1] + if (event[0] == following[0] == "climb" and + event[-1] == following[-1] == rank and event[4] == following[4]): + scalar = events[i + 2] + if (scalar[0] == "scalar" and scalar[1][0] == "add" and + {tuple(scalar[1][1]), tuple(scalar[1][2])} == + {("L", event[2]), ("L", following[2])}): + pairs.append([[i, event], [i + 1, following]]) + require(rank == 2 and len(pairs) == 32, "seed-selected scope drifted") + pair = pairs[SEED % len(pairs)] + require([item[0] for item in pair] == [14512, 14513], "selected pair drifted") + saving = Q(spec["expected"]["complex_lower"]) + require(0 < saving < 1, "invalid saving") + return { + "supplier_pr": 626, + "provider": "jp8", + "program_payload_sha256": hashlib.sha256(sources[PROGRAM]).hexdigest(), + "paid_profiles": profiles, + "eligible_consecutive_pairs": len(pairs), + "seed_selected_rank": rank, + "seed_selected_pair": pair, + "complex_saving": str(saving), + "sigma": str(1 - saving), + "accepted_kappa_at_base": spec["expected"]["kappa"], + "scope": "Reads pinned native receipts; does not rerun the full supplier or assert legal co-scheduling.", + } + + +def gaussian_mul(a, b): + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +@lru_cache(maxsize=None) +def tensor_entry(n, distance, direction): + """Independent closed-form Kronecker entry, numerator over 2**n.""" + value = (1, 0) + for _ in range(n - distance): + value = gaussian_mul(value, (1, direction)) + for _ in range(distance): + value = gaussian_mul(value, (1, -direction)) + return value + + +def coordinate_layer(vector, axis, direction, n, only_padding_from=None): + """Integer Gaussian butterfly; each step adds one power of two to denominator.""" + out = [(0, 0)] * len(vector) + bit = 1 << axis + for i in range(len(vector)): + if i & bit: + continue + j = i | bit + if only_padding_from is not None and i >> n < only_padding_from: + out[i] = tuple(2 * a for a in vector[i]) + out[j] = tuple(2 * a for a in vector[j]) + continue + a, b = vector[i] + c, d = vector[j] + # (u+v +/- i(u-v))/2; inverse changes direction from +1 to -1. + out[i] = (a + c - direction * (b - d), b + d + direction * (a - c)) + out[j] = (a + c + direction * (b - d), b + d - direction * (a - c)) + return out + + +def run_column(n, s, k, column, direction=1, mutant=None): + q = 1 << s + require(n >= 1 and s >= 1 and 1 <= k <= q, "invalid circuit dimensions") + vector = [(0, 0)] * (1 << (n + s)) + vector[column] = (1, 0) + denominator = 0 + # C_(n+s) on the joined q-lane array. + for axis in range(n + s): + vector = coordinate_layer(vector, axis, direction, n) + denominator += 1 + # The inverse selector is a paid C_s with sign/phase wrappers. + if mutant != "omit_selector": + axes = list(range(n, n + s)) + if mutant == "wrong_selector_axis": + axes[0] = 0 + for axis in axes: + sign = direction if mutant == "forward_selector" else -direction + vector = coordinate_layer(vector, axis, sign, n) + denominator += 1 + # Padded lanes contain arbitrary dirt, so undo their unwanted C_n. + if k < q and mutant != "omit_padding_restoration": + for axis in range(n): + vector = coordinate_layer(vector, axis, -direction, n, k) + denominator += 1 + if mutant == "wrong_global_phase": + vector = [(-b, a) for a, b in vector] + if mutant == "wrong_normalization": + vector = [(2 * a, 2 * b) for a, b in vector] + return vector, denominator + + +def reference_entry(n, k, row, column, direction): + row_lane, col_lane = row >> n, column >> n + if col_lane >= k: + return ((1 << n, 0) if row == column else (0, 0)) + if row_lane != col_lane: + return (0, 0) + return tensor_entry(n, (row ^ column).bit_count(), direction) + + +def first_mismatch(n, s, k, direction=1, mutant=None): + for column in range(1 << (n + s)): + vector, denominator = run_column(n, s, k, column, direction, mutant) + for row, actual in enumerate(vector): + expected = reference_entry(n, k, row, column, direction) + if tuple(a << n for a in actual) != tuple(a << denominator for a in expected): + return {"column": column, "row": row, + "actual_numerator": list(actual), "actual_denominator_power": denominator, + "expected_numerator": list(expected), "expected_denominator_power": n} + return None + + +def operator_replays(): + # Exhaust every basis column of every case, rather than sample input vectors. + cases = [(n, s, 1 << s) for n in range(1, 7) for s in (1, 2)] + cases += [(n, 2, 3) for n in range(1, 5)] + [(8, 1, 2)] + receipts = [] + for n, s, k in cases: + size = 1 << (n + s) + for direction in (1, -1): + digest = hashlib.sha256() + for column in range(size): + vector, denominator = run_column(n, s, k, column, direction) + for row, actual in enumerate(vector): + expected = reference_entry(n, k, row, column, direction) + require(tuple(a << n for a in actual) == + tuple(a << denominator for a in expected), + f"operator mismatch at {(n, s, k, direction, row, column)}") + digest.update(canonical([row, column, list(expected)])) + # Support is invariant under invertible monomial pre/post maps. + # C_(n+s) is dense; each desired active row has only 2**n nonzeros. + require(all(tensor_entry(n + s, d, direction) != (0, 0) + for d in range(n + s + 1)), "unexpected zero in tensor kernel") + receipts.append({"data_axes": n, "selector_axes": s, "active_lanes": k, + "direction": direction, "all_columns": size, + "dirty_padding_columns": ((1 << s) - k) * (1 << n), + "raw_row_support": size, "target_active_row_support": 1 << n, + "reference_matrix_sha256": digest.hexdigest()}) + return receipts + + +def operator_controls(): + controls = [] + for name, n, s, k in [ + ("omit_selector", 2, 1, 2), + ("forward_selector", 2, 1, 2), + ("wrong_selector_axis", 2, 1, 2), + ("wrong_global_phase", 2, 1, 2), + ("wrong_normalization", 2, 1, 2), + ("omit_padding_restoration", 2, 2, 3), + ]: + witness = first_mismatch(n, s, k, mutant=name) + require(witness is not None, "invalid operator accepted: " + name) + if name == "omit_padding_restoration": + require(witness["column"] >= k * (1 << n), "dirty control missed dirty input") + controls.append({"name": name, "rejected_by": "full operator identity", "witness": witness}) + return controls + + +@lru_cache(maxsize=None) +def log_bounds(x): + """Exact atanh-series bounds, reduced to [1,2]; no floating point.""" + require(x > 0, "log domain") + if x < 1: + lo, hi = log_bounds(1 / x) + return -hi, -lo + shifts = 0 + while x > 2: + x /= 2 + shifts += 1 + t = (x - 1) / (x + 1) + count = 40 + lo = 2 * sum((t ** (2 * j + 1) / (2 * j + 1) for j in range(count)), Q(0)) + hi = lo + 2 * t ** (2 * count + 1) / ((2 * count + 1) * (1 - t * t)) + if shifts: + a, b = log_bounds(Q(2)) + lo += shifts * a + hi += shifts * b + return lo, hi + + +def exp_bounds(x): + if x < 0: + lo, hi = exp_bounds(-x) + return 1 / hi, 1 / lo + count = 60 + require(x < count + 2, "exp tail bound outside its domain") + term = total = Q(1) + for j in range(1, count + 1): + term = term * x / j + total += term + next_term = term * x / (count + 1) + return total, total + next_term / (1 - x / (count + 2)) + + +@lru_cache(maxsize=None) +def power_bounds(base, exponent): + require(base > 0 and 0 <= exponent <= 1, "power domain") + if exponent == 0: + return Q(1), Q(1) + if exponent == 1: + return base, base + lo, hi = log_bounds(base) + return exp_bounds(exponent * lo)[0], exp_bounds(exponent * hi)[1] + + +def compact_interval(bounds): + lo, hi = bounds + grid = 10 ** 24 + lower = (lo.numerator * grid) // lo.denominator + upper = -((-hi.numerator * grid) // hi.denominator) + require(lower <= upper, "reversed interval") + return {"lower": str(Q(lower, grid)), "upper": str(Q(upper, grid))} + + +def bill(n, s, k): + q = 1 << s + # Weights are volumes in units of ONE original lane's volume V. + return {"data_axes": n, "selector_axes": s, "active_lanes": k, + "joined_volume_over_V": q, + "calls": [[q, n + s, "joined transform"], [q, s, "inverse selector"]] + + ([[q - k, n, "dirty padding restoration"]] if q > k else [])} + + +def check_bill(invoice): + n, s, k = (invoice[name] for name in ("data_axes", "selector_axes", "active_lanes")) + require(n >= 1 and s >= 1 and 1 <= k <= 1 << s, "bad bill dimensions") + # Independently check each operation's domain cardinality against the input + # lanes. In particular the joined operator acts on every selector value. + lanes = len(range(1 << s)) + require(invoice["joined_volume_over_V"] == lanes, "joined array volume omitted") + calls = {why: (volume, width) for volume, width, why in invoice["calls"]} + require(len(calls) == len(invoice["calls"]), "duplicate call type") + required = {"joined transform", "inverse selector"} + if k < lanes: + required.add("dirty padding restoration") + require(set(calls) == required, "required operator omitted from bill") + require(calls["joined transform"] == (lanes, n + s), "wrong joined transform domain") + require(calls["inverse selector"] == (lanes, s), "wrong inverse selector domain") + if k < lanes: + require(calls["dirty padding restoration"] == (lanes - k, n), + "wrong dirty restoration domain") + + +def ratio_bounds(n, s, k, sigma): + invoice = bill(n, s, k) + check_bill(invoice) + lo = hi = Q(0) + for volume, width, _ in invoice["calls"]: + a, b = power_bounds(Q(width, n), sigma) + lo += Q(volume, k) * a + hi += Q(volume, k) * b + return lo, hi + + +def budget_certificate(sigma): + # At sigma=1/2, square the endpoints to independently validate the engine. + for base in (Q(1, 2), Q(3, 2), Q(2), Q(5)): + lo, hi = power_bounds(base, Q(1, 2)) + require(0 < lo <= hi and lo * lo <= base <= hi * hi, "sqrt enclosure failed") + correct = ratio_bounds(2, 1, 2, sigma) + naive = (correct[0] / 2, correct[1] / 2) + require(naive[1] < 1 < correct[0], "false-saving control did not separate") + fixed = [] + for f in (1, 2, 4, 8, 16, 32, 128, 1024): + ratio = ratio_bounds(2 * f, 1, 2, sigma) + require(ratio[0] > 1, "fixed-lane budget unexpectedly improves") + fixed.append({"f": f, "bill": bill(2 * f, 1, 2), "ratio_to_original": compact_interval(ratio)}) + scaled = [] + for f in range(1, 9): + ratio = ratio_bounds(2 * f, f, 2, sigma) + require(ratio[0] > 1, "slot-scaled selector budget unexpectedly improves") + scaled.append({"f": f, "bill": bill(2 * f, f, 2), "ratio_to_original": compact_interval(ratio)}) + mutations = [] + for name in ("omit_volume_factor", "omit_selector_cost", "omit_dirty_restoration"): + invoice = bill(2, 2, 3) if name == "omit_dirty_restoration" else bill(2, 1, 2) + if name == "omit_volume_factor": + invoice["joined_volume_over_V"] = 1 + invoice["calls"] = [[1, width, why] for _, width, why in invoice["calls"]] + else: + omitted = "inverse selector" if name == "omit_selector_cost" else "dirty padding restoration" + invoice["calls"] = [call for call in invoice["calls"] if call[2] != omitted] + try: + check_bill(invoice) + except VerificationError: + mutations.append(name) + else: + raise VerificationError("invalid bill accepted: " + name) + return {"sigma": str(sigma), "f1_original_profile": {"2": 2}, + "f1_incorrect_unweighted_profile": {"1": 1, "3": 1}, + "f1_volume_weighted_profile": {"1": 2, "3": 2}, + "f1_naive_ratio": compact_interval(naive), "f1_complete_ratio": compact_interval(correct), + "f1_even_if_selector_is_free": compact_interval(power_bounds(Q(3, 2), sigma)), + "fixed_two_lanes": fixed, "two_lanes_with_slot_scaled_selector": scaled, + "bill_mutations_rejected": mutations, + "interpretation": "Comparison of inherited cost bounds, not a lower bound on actual algorithms."} + + +def make_certificate(root): + sources = check_sources(root) + reference = supplier_reference(sources) + replays = operator_replays() + controls = operator_controls() + budget = budget_certificate(Q(reference["sigma"])) + return {"schema": "selector-batching/1", "status": STATUS, "base_commit": BASE, + "assignment_seed": SEED, "supplier_reference": reference, + "operator_replays": replays, + "total_exact_columns": sum(r["all_columns"] for r in replays), + "total_exact_matrix_entries": sum(r["all_columns"] ** 2 for r in replays), + "total_dirty_padding_columns": sum(r["dirty_padding_columns"] for r in replays), + "operator_mutations_rejected": controls, "budget": budget, + "scope": "Finite exact evidence plus the written all-size bound comparison in README.md; no new kappa or full theorem verification."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo-root", type=Path, default=HERE.parents[1]) + parser.add_argument("--output", type=Path, help="write an identical receipt to a new file after verification") + args = parser.parse_args() + certificate = make_certificate(args.repo_root.resolve()) + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(certificate == expected, "recomputed certificate differs from CERTIFICATE.json") + if args.output: + with args.output.open("x") as handle: + json.dump(certificate, handle, indent=2, sort_keys=True) + handle.write("\n") + print(STATUS) + print(f"{len(certificate['operator_replays'])} full operator cases; " + f"{certificate['total_exact_columns']} exact columns; " + f"{certificate['total_dirty_padding_columns']} dirty padding columns; " + "6 operator and 3 invoice mutations rejected") + + +if __name__ == "__main__": + main()