diff --git a/research/scatter-export-parity-audit/NATIVE.json b/research/scatter-export-parity-audit/NATIVE.json new file mode 100644 index 0000000000..867a37ccfb --- /dev/null +++ b/research/scatter-export-parity-audit/NATIVE.json @@ -0,0 +1,297 @@ +{ + "arithmetic_backend": "checked_cpp_int_128_standin", + "fixtures": { + "baseline": { + "columns": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121525, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "local_scalar_stream": "COHORT249-RECORDS.bin", + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24305, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27234, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "records_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + "paired_duplicate": { + "columns": { + "exit_code": 2, + "rejection": "local defining-decoder full formal column" + }, + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24306, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27235, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "records_sha256": "5629b522bb0381127e3514396f034f308e0aa797f134f833e4d8feb678dce744" + }, + "single_occurrence": { + "columns": { + "exit_code": 2, + "rejection": "local defining-decoder full formal column" + }, + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24306, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27235, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "records_sha256": "5629b522bb0381127e3514396f034f308e0aa797f134f833e4d8feb678dce744" + } + }, + "paired_and_single_records_equal": true, + "status": "PASS_SCATTER_EXPORT_NATIVE_PARITY_CONTROL" +} diff --git a/research/scatter-export-parity-audit/README.md b/research/scatter-export-parity-audit/README.md new file mode 100644 index 0000000000..b95c516825 --- /dev/null +++ b/research/scatter-export-parity-audit/README.md @@ -0,0 +1,145 @@ +# Selected scatter lists and record-export parity + +Appending `[0,0]` to row 0 of the selected PR589 bit word passes the complete +symbolic checker but changes the exported F2 operator. Native record legality +also accepts it. The native formal-column checker rejects the exported word. +This is a counterexample to a cross-stage implication, with a two-entry fixture +and an exact dirty-input witness. It does not invalidate the selected result. + +The selected generator produces distinct row entries, its tuned word satisfies +that condition, and its complete replay binds the original bytes. No production +source, frozen input or selected-frontier record is changed here. + +## Exact result and proof + +The pinned tuned word has `v=111`, `R=439`, nine retained totals and 661 local +input columns. Its first scatter row is `[4,5,6,7,8]`, and retained index 0 names +helper register 472. Change only that row to `[4,5,6,7,8,0,0]`. + +The complete [symbolic checker](../e8-bit-p111-tuned/code/xcheck_p.py) XORs a +copied total once per list occurrence in `Word.replay`. The +[record exporter](../e8-bit-carrier-skeleton/code/bit/export_records.py) emits +one ADD if `k in row`. If an index occurs `m` times, their coefficients over F2 +are respectively `m mod 2` and `[m>0]`. For independent abstract copied values, +the two scatter operators agree exactly when every positive multiplicity is +odd. Distinct entries are a sufficient boundary condition. Repeated odd +multiplicities can also agree, so uniqueness is not asserted necessary. + +Two added occurrences cancel in the symbolic word. All label/lattice checks, +all 661 dirty-state columns, H1-H5 and all four conclusion flags still pass. +The scatter occurrence count rises from 527 to 529. The exporter instead emits +one extra ADD, raising its stream from 27,234 to 27,235 records. The record +legality check still accepts rank mass 5,129 and nine COPY/ERASE pairs. + +Set only input register 472 to one. The original export leaves target 111 at +zero; the mutant leaves it at one. Helper 472 remains one in both. The exact +full-column oracle finds that only output register 111 differs, and records +its complete difference support in [RESULT.json](RESULT.json). The actual +native checker fails at `local defining-decoder full formal column`. + +Appending a single `[0]` is rejected by the symbolic checker with +`targets not y + x: [0]`, yet exports byte-identically to the paired mutant. +Thus two is minimal among append-only repetitions of this initially absent +index that retain this symbolic endpoint. This is not a minimum over arbitrary +word edits. Removing even multiplicities from this specific row recovers the +original word and its exact record bytes. No general signed-ring normalization +or compiler repair is claimed. + +The package's `validate_scatter` is a tested sufficient guard requiring simple +support lists. It rejects repeated, noninteger and out-of-range indices before +export. It is an opt-in repair candidate, not an installed production change. + +## Source boundary and existing protection + +[gen_p3.decoder_rows](../e8-bit-p111-tuned/code/gen_p3.py) searches +`itertools.combinations`, so its rows contain no duplicates. +[pwordl.build](../e8-bit-p111-tuned/code/pwordl.py) serializes those rows, and +[tune/apply.py](../e8-bit-p111-tuned/tune/apply.py) changes only A/C after copying +the base. The pinned [tune/verify.sh](../e8-bit-p111-tuned/tune/verify.sh) binds +the rebuilt word before its checker/export/native stages. The synthetic mutant +is outside that selected producer, and the later column check independently +rejects its endpoint. Symbolic checking or record legality alone does not +replace that later check. + +These source observations are pinned and inspected, not a fresh execution of +the generator, tuner or complete supplier chain. The original source bytes +match the selected PR1094 source manifest. [SOURCES.json](SOURCES.json) also +pins the exact native sources and the checked arithmetic stand-in. + +## Reproduce + +The registered hook requires Python 3.12. The direct audit also runs on newer +Python versions. Both use only the standard library, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/scatter-export-parity-audit +python3 -I -O -Werror -B research/scatter-export-parity-audit/verify.py +``` + +The first command runs the primary audit and eight behavioral test groups. +Normal replay is read-only. `verify.py --emit` prints a reconstructed receipt. +The oracle directly interprets the unchanged exporter's packed records, with +661 independent F2 basis bits. MOVE is ignored only in this scalar projection; +COPY creates a fresh temporary and ERASE closes it. This is not an independent +frame, hosting, precision or native compilation proof. + +Optional native replay, with a C++17 compiler: + +```sh +python3 -I -Werror -B research/scatter-export-parity-audit/native.py +``` + +It compiles the actual unchanged legality and five-stage column checkers with +`HDIM=8, NCOPY=9, VPORTS=111, RHELP=439`, using the authenticated +[checked cpp_int stand-in](../bit589-checked-cpp-int-seed92/README.md). +That backend is checked 128-bit arithmetic which refuses overflow. This is not +a fresh system-Boost build. The three native fixtures and complete deterministic +receipts are in [NATIVE.json](NATIVE.json). Only elapsed times and the temporary +stream path are normalized after checking their format. Native replay is +optional because the generic hook does not provision a compiler. + +## Open next questions + +Choose the scatter schema for a separately versioned successor checker and +exporter. If rows are simple supports, enforce uniqueness at both boundaries; +if multiplicity is meaningful, define its coefficient semantics and test that +lowering. Start by adding this two-entry fixture to the successor's full +symbolic/export/native sequence. Adoption requires new manifests and reviewed +source bindings; frozen packages should stay unchanged. No additional search +or new supplier construction follows from this audit. + +## Scope, credit and verification limits + +Base main `d878e1f048823de10e57e3dc58522d345a5fcd8d`, priority revision 5. +[TASK.json](TASK.json) records the refined `supplier-boundary-audit` card, +overlap coverage, freshness and remaining obligations. The canonical +[Discussion2976](https://github.com/CrocSwap/integer-mult-bounds/discussions/2976) +contains the claim and artifact handoff. Existing scatter-lifecycle, record +mutation and owner-binding work is credited there; none is replaced here. + +Credit eumemic for the punctured generator, word checker and PR543/PR555/PR589 +lineage; DreamingOfClouds for the punctured-star and retained bit-supplier +construction lineage; Dylan Crow for the exporter and native checkers; and +Douglas Colkitt for the selected source bindings and review. Existing source +notices and licenses remain unchanged. This contribution adds the paired-list +counterexample, exact source-to-record witness, guard and replay controls. + +Nick Petalas. Apache-2.0. Substantial automated assistance in research, +implementation, checking and writing. Separate internal source inspection and +review do not constitute independent human or proof-assistant review. Full +selected cold replay, all-size transfer and hosted CI are not claimed. + +## Engineering constraints + +Build the Lever led to the retained record interpreter and native replay; +Prove It Works required the actual full symbolic checker, exporter and native +rejection. Power-of-Ten checks keep the new functions below 60 lines, bound +inputs to 24 pinned files of at most 5 MiB and streams to 30,000 records, and +use explicit checks under `-O`. Registered commands have finite timeouts. + +Rules 3, 8 and 9 require managed-runtime and authenticated-code deviations: +Python allocates bounded fixture objects and dispatches pinned modules and +subprocesses. The source hashes, fixed 661-column/three-fixture domain, +subprocess deadlines, explicit closure and corruption controls bound their +scope. Frozen source loops are audit subjects, unchanged here. Reassess these +controls before enlarging the domain or adopting a production compiler change. diff --git a/research/scatter-export-parity-audit/RESULT.json b/research/scatter-export-parity-audit/RESULT.json new file mode 100644 index 0000000000..fa50f464d0 --- /dev/null +++ b/research/scatter-export-parity-audit/RESULT.json @@ -0,0 +1,160 @@ +{ + "baseline": { + "records": 27234, + "records_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a", + "symbolic": { + "columns": 661, + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "scatter_terms": 527 + } + }, + "columns": 661, + "duplicate_guard": "duplicate scatter index", + "mutant": { + "appended_indices": [ + 0, + 0 + ], + "records": 27235, + "records_sha256": "5629b522bb0381127e3514396f034f308e0aa797f134f833e4d8feb678dce744", + "symbolic": { + "columns": 661, + "conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "scatter_terms": 529 + }, + "witness": { + "actual_bit": 1, + "difference_support": [ + 0, + 3, + 5, + 6, + 9, + 11, + 14, + 15, + 20, + 21, + 23, + 25, + 26, + 28, + 30, + 31, + 36, + 37, + 39, + 41, + 42, + 44, + 49, + 50, + 51, + 53, + 55, + 57, + 61, + 62, + 63, + 68, + 69, + 72, + 73, + 74, + 77, + 78, + 83, + 85, + 87, + 88, + 89, + 92, + 93, + 97, + 99, + 101, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 222, + 228, + 240, + 247, + 266, + 268, + 272, + 276, + 278, + 288, + 298, + 304, + 308, + 332, + 334, + 338, + 342, + 346, + 357, + 358, + 360, + 381, + 385, + 391, + 393, + 401, + 405, + 413, + 417, + 423, + 425, + 433, + 437, + 447, + 451, + 455, + 457, + 461, + 472, + 484, + 499, + 504 + ], + "expected_bit": 0, + "input_column": 472, + "output_register": 111 + } + }, + "normalized_export_equals_baseline": true, + "retained_register": 472, + "status": "PASS_SELECTED_SCATTER_EXPORT_PARITY_AUDIT", + "target_row": 0 +} diff --git a/research/scatter-export-parity-audit/SOURCES.json b/research/scatter-export-parity-audit/SOURCES.json new file mode 100644 index 0000000000..3a959d97da --- /dev/null +++ b/research/scatter-export-parity-audit/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "d878e1f048823de10e57e3dc58522d345a5fcd8d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/bit589-checked-cpp-int-seed92/include/boost/multiprecision/cpp_int.hpp", + "usage": "input", + "git_blob": "bc9634fd9090bdc2f6071a92472cc09306a0a9df", + "sha256": "2cb97050101cfd286ccfc7caa62221c63a2bcd3102f7d5f916ccef0953fb4426" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp", + "usage": "input", + "git_blob": "00c5a3a5d81d083582f60f33dd2e7bea5049c37f", + "sha256": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce" + }, + { + "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/gen_p3.py", + "usage": "input", + "git_blob": "ab21c9c19fc2386f273cd568b46282efcdd77fff", + "sha256": "438b83f10d70ceca7cf78049420204b7de2dc61682f913c50a62596106ad84cd" + }, + { + "path": "research/e8-bit-p111-tuned/code/pwordl.py", + "usage": "input", + "git_blob": "a90bed93e227c3916aca67817794f35e24123ceb", + "sha256": "6d8fccd44508e4705b6446e0a64482a5221a3efc5663c5ca7ae90d44581ac50a" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/apply.py", + "usage": "input", + "git_blob": "65849f369bdcb0b2ad87566d102e5c776b3994eb", + "sha256": "806ae4cb2648e4f05dcf56bd089891fd3ba33a6ee5fe76d3329e322c6770c1a1" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/verify.sh", + "usage": "input", + "git_blob": "92310cbc220ece46c72f2131ddcc8d802bd35c56", + "sha256": "efb1051d3e2c6119574a29a8e4efbe316307b5901d05079d029e12fae9ff1fb1" + } + ] +} diff --git a/research/scatter-export-parity-audit/TASK.json b/research/scatter-export-parity-audit/TASK.json new file mode 100644 index 0000000000..06518fca46 --- /dev/null +++ b/research/scatter-export-parity-audit/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 5, + "base_commit": "d878e1f048823de10e57e3dc58522d345a5fcd8d", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "refined", + "actual_scope": "Does full symbolic acceptance of the selected bit word imply parity-preserving record export for repeated scatter indices?", + "scope_change_reason": "Refine the selected-supplier acceptance card to one bit-word checker/exporter boundary, with an exact paired-null scatter fixture and native rejection control.", + "bottleneck_link": "The selected bit supplier depends on both symbolic and native column checks. This counterexample proves one cannot substitute symbolic acceptance or record legality for the exported endpoint check.", + "budget_minutes": 60, + "stop_rule": "One pinned baseline, the paired-null mutant, one-occurrence and source/receipt controls, full local F2 endpoint, actual native guard, and focused upstream PR. No supplier search or frontier change.", + "outcome": "completed", + "evidence": "RESULT.json, NATIVE.json, verify.py, native.py and eight behavioral test groups", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in source investigation, implementation, verification and writing; no independent human review.", + "open_questions": [ + { + "question": "Which explicit scatter-list schema should a successor checker/exporter enforce?", + "why_it_matters": "Symbolic multiplicity parity and membership lowering differ outside the unique-row producer domain.", + "first_step": "Pin a separately versioned successor and add this paired-list fixture to full symbolic/export/native tests; enforce uniqueness or specify coefficient semantics.", + "blocked_by": "Production adoption requires reviewed successor manifests and source bindings; frozen packages remain unchanged." + } + ], + "draw_seed": "386dec589270946a6a7432d75cca800e", + "method": "Construct a two-entry semantically null scatter edit, run the full symbolic checker and unchanged exporter, independently interpret every F2 input column, and verify native rejection.", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2976", + "freshness": { + "upstream_commit": "47fa55b3cd8c7cf8879206f33569bc59d637dad8", + "priority_revision": 5, + "checked_at_utc": "2026-10-16T15:38:37.518303+00:00", + "relevant_changes": "No changes to AGENTS.md, autoresearch.md, catalogue, selected record or either audited bit package since the scientific base." + }, + "overlap": { + "checked_at_utc": "2026-10-16T15:38:56.849063+00:00", + "open_prs": 227, + "closed_prs": 2435, + "discussion_records": 1675, + "complete_pagination": true, + "terms": [ + "duplicate scatter", + "scatter parity", + "export_records" + ], + "limitations": "Metadata and top-level package notes only; no exhaustive diff or unpublished-work coverage.", + "related_packages": [ + "research/r420-scatter-lifecycle", + "research/e8-bit-p111-tuned/code/mutants_p.py", + "research/e8-bit-p111-tuned/code/mutrec_b.py" + ], + "warnings": [], + "result": "No competing duplicate-scatter result identified; the canonical claim itself and related export/lifecycle work matched." + }, + "validation": { + "registered_replay": "PASS on CPython 3.12.15", + "direct_optimized": "PASS on CPython 3.14.8", + "native": "PASS on CPython 3.12.15 and 3.14.8, Apple clang 21.0.0, authenticated checked cpp_int stand-in", + "behavioral_tests": 8, + "workflow_tests": { + "run": 158, + "skipped": 18, + "environment": "CPython 3.12.15 on macOS; 18 tests skipped by existing platform/environment guards." + }, + "lint": "Ruff 0.17.1 check and format pass", + "review": "Separate read-only internal review reran primary, eight behavioral groups, source pins and native replay; no blocking finding. Generic Python-version wording corrected.", + "hosted_ci": "Pending separate upstream evidence; all reported execution is local." + } +} diff --git a/research/scatter-export-parity-audit/VERIFY.json b/research/scatter-export-parity-audit/VERIFY.json new file mode 100644 index 0000000000..b77fd95c73 --- /dev/null +++ b/research/scatter-export-parity-audit/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit589-checked-cpp-int-seed92/include/boost/multiprecision/cpp_int.hpp", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.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/gen_p3.py", + "research/e8-bit-p111-tuned/code/pwordl.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/tune/apply.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/tune/verify.sh" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Selected positive full symbolic and exact exported F2 endpoint, paired-null counterexample, all 661 columns, duplicate guard and parity-normalized source control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 90, + "checks": "Eight behavioral groups, including source corruption, independent literal record oracle, malformed lists, one-occurrence rejection, optimized read-only replay and typed receipt rejection." + } + ] +} diff --git a/research/scatter-export-parity-audit/native.py b/research/scatter-export-parity-audit/native.py new file mode 100644 index 0000000000..99e350dffd --- /dev/null +++ b/research/scatter-export-parity-audit/native.py @@ -0,0 +1,241 @@ +"""Optional actual native replay with the checked cpp_int stand-in, not Boost. + +The two unchanged C++ checkers compile with their selected dimensions. The +explicit stand-in uses checked 128-bit arithmetic and refuses overflow. This +is a finite cross-stage control, not a fresh system-Boost or supplier replay. +All compiler inputs are authenticated by the primary verifier before work. + +Power-of-Ten deviation: Python allocates bounded fixture/receipt objects and +dispatches authenticated external programs. Two builds and twelve fixed child +calls have explicit deadlines; three streams contain at most 30,000 records. +Frozen compiler code and its existing diagnostics remain unchanged. Reassess +those bounds before adding fixtures, targets, compiler flags or input files. +Nick Petalas. Apache-2.0. +""" + +import argparse +import copy +import gzip +import hashlib +import json +import math +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +import verify + +BIT = "research/e8-bit-carrier-skeleton/code/bit/" +CHECKERS = BIT + "checkers/" +STAGE = BIT + "regression/stage_cohort.py" +PORTABLE = "research/e8-bit-carrier-skeleton/portable-include/" +STANDIN = "research/bit589-checked-cpp-int-seed92/include/" +NATIVE_INPUTS = ( + CHECKERS + "columns_h.cpp", + CHECKERS + "legality_h.cpp", + CHECKERS + "json.hpp", + STAGE, + PORTABLE + "bits/stdc++.h", + STANDIN + "boost/multiprecision/cpp_int.hpp", +) +LEGALITY_STATUS = "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" +COLUMNS_STATUS = "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" +REJECTION = "local defining-decoder full formal column" +BASE_SHA = "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" +MUTANT_SHA = "5629b522bb0381127e3514396f034f308e0aa797f134f833e4d8feb678dce744" + + +def command(arguments, *, timeout=30): + """Return a completed process; callers check its actual output contract.""" + verify.require(0 < len(arguments) <= 24, "bounded native command") + return subprocess.run( + arguments, check=False, capture_output=True, text=True, timeout=timeout + ) + + +def compile_checkers(data, directory): + verify.require(set(NATIVE_INPUTS) <= set(data), "complete native source pins") + for name in NATIVE_INPUTS: + path = directory / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(data[name]) + compiler = os.environ.get("CXX", "c++") + verify.require(bool(compiler) and len(compiler) <= 4096, "compiler executable") + flags = [ + compiler, + "-O2", + "-std=c++17", + "-DHDIM=8", + "-DNCOPY=9", + "-DVPORTS=111", + "-DRHELP=439", + ] + flags += ["-I" + str(directory / name) for name in (PORTABLE, CHECKERS, STANDIN)] + binaries = {} + for name in ("legality_h", "columns_h"): + output = directory / name + result = command( + flags + ["-o", str(output), str(directory / CHECKERS / (name + ".cpp"))], + timeout=60, + ) + verify.require( + result.returncode == 0 and output.is_file(), + "native compile failed: " + result.stderr, + ) + binaries[name] = output + return binaries + + +def legality(binary, cin, cout, receipt, count): + result = command([str(binary), str(cin), str(cout), str(receipt)]) + verify.require( + result.returncode == 0 and receipt.is_file(), + "native legality failed: " + result.stderr, + ) + value = json.loads(receipt.read_bytes()) + verify.require(value["status"] == LEGALITY_STATUS, "native legality status") + verify.require( + value["records"] == count and value["rank_mass"] == 5129, + "native legality records and mass", + ) + verify.require( + value["copies"] == value["erasures"] == 9, "native copy/erase inventory" + ) + verify.require(value["common_frame_ADDs"] == count - 2929, "native ADD recount") + return value + + +def columns(binary, stream, receipt, honest): + result = command([str(binary), str(stream), str(receipt)]) + if not honest: + verify.require( + result.returncode == 2 and result.stderr.strip() == REJECTION, + "native mutant rejection site", + ) + verify.require( + not result.stdout and not receipt.exists(), + "native rejection produces no success receipt", + ) + return {"exit_code": 2, "rejection": REJECTION} + verify.require( + result.returncode == 0 and receipt.is_file(), + "native baseline columns failed: " + result.stderr, + ) + value = json.loads(receipt.read_bytes()) + verify.require(value["status"] == COLUMNS_STATUS, "native column status") + verify.require( + value["formal_columns_checked"] == 883, + "complete native global column inventory", + ) + verify.require(value["local_scalar_stream"] == str(stream), "native stream link") + value["local_scalar_stream"] = "COHORT249-RECORDS.bin" + seconds = value.pop("seconds") + verify.require( + type(seconds) in (int, float) and math.isfinite(seconds) and seconds >= 0, + "native elapsed-time metadata", + ) + lines = result.stderr.splitlines() + verify.require(len(lines) == 5, "five native stages") + for stage, line in enumerate(lines): + prefix = "stage " + str(stage) + " PASS elapsed " + verify.require( + line.startswith(prefix) and line.endswith("s"), "native stage diagnostic" + ) + elapsed = float(line[len(prefix) : -1]) + verify.require(math.isfinite(elapsed) and elapsed >= 0, "native stage timing") + return value + + +def fixture(data, word, directory, binaries, honest): + raw = verify.export(data[verify.EXPORTER], word, directory) + expected_sha = BASE_SHA if honest else MUTANT_SHA + verify.require( + hashlib.sha256(raw).hexdigest() == expected_sha, + "native fixture record identity", + ) + values, differences = verify.replay(raw, word) + if honest: + verify.require(not differences, "native positive scalar oracle") + else: + verify.require( + verify.witness(values, differences, word)["actual_bit"] == 1, + "native dirty-input scalar oracle", + ) + records, cin, cout = directory / "records", directory / "cin", directory / "cout" + result = command( + [ + sys.executable, + "-I", + "-B", + str(directory.parent / STAGE), + str(records), + str(records), + str(cin), + str(cout), + ] + ) + verify.require(result.returncode == 0, "original cohort staging: " + result.stderr) + stream = cout / "COHORT249-RECORDS.bin" + verify.require(stream.read_bytes() == raw, "original cohort stream identity") + legal = legality( + binaries["legality_h"], cin, cout, directory / "legality.json", len(raw) // 24 + ) + scalar = columns(binaries["columns_h"], stream, directory / "columns.json", honest) + return raw, {"records_sha256": expected_sha, "legality": legal, "columns": scalar} + + +def audit(data, directory): + binaries = compile_checkers(data, directory) + word = json.loads(gzip.decompress(data[verify.WORD])) + verify.validate_scatter(word) + verify.require( + word["scatter"][0] == [4, 5, 6, 7, 8] and word["ret"][0] == 472, + "native exact mutation site", + ) + results, mutants = {}, [] + for name, added in ( + ("baseline", []), + ("paired_duplicate", [0, 0]), + ("single_occurrence", [0]), + ): + value = copy.deepcopy(word) + value["scatter"][0].extend(added) + raw, results[name] = fixture( + data, value, directory / name, binaries, name == "baseline" + ) + if added: + mutants.append(raw) + verify.require(mutants[0] == mutants[1], "paired and single native stream identity") + return { + "status": "PASS_SCATTER_EXPORT_NATIVE_PARITY_CONTROL", + "arithmetic_backend": "checked_cpp_int_128_standin", + "fixtures": results, + "paired_and_single_records_equal": True, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + data = verify.sources(verify.ROOT) + with tempfile.TemporaryDirectory(prefix="scatter-native-") as temporary: + result = audit(data, Path(temporary)) + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True, allow_nan=False)) + else: + expected = json.loads((PACKAGE / "NATIVE.json").read_bytes()) + verify.require( + json.dumps(result, sort_keys=True, allow_nan=False) + == json.dumps(expected, sort_keys=True, allow_nan=False), + "typed native deterministic receipt", + ) + print(result["status"], "native_legality_accepts=3 scalar_rejects=2") + + +if __name__ == "__main__": + main() diff --git a/research/scatter-export-parity-audit/test_verify.py b/research/scatter-export-parity-audit/test_verify.py new file mode 100644 index 0000000000..86b7495791 --- /dev/null +++ b/research/scatter-export-parity-audit/test_verify.py @@ -0,0 +1,156 @@ +"""Behavioral controls for the scatter/export boundary. Apache-2.0.""" + +import copy +import gzip +import json +import shutil +import struct +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify + + +class BoundaryTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = verify.sources(verify.ROOT) + cls.word = json.loads(gzip.decompress(cls.data[verify.WORD])) + + def test_support_guard(self): + verify.validate_scatter(self.word) + for row in ([4, 4], [True], [-1], [9], "4", list(range(10))): + mutant = copy.deepcopy(self.word) + mutant["scatter"][0] = row + with self.subTest(row=row), self.assertRaises(ValueError): + verify.validate_scatter(mutant) + mutant = copy.deepcopy(self.word) + mutant["scatter"].pop() + with self.assertRaisesRegex(ValueError, "row inventory"): + verify.validate_scatter(mutant) + + def test_single_occurrence_is_not_null(self): + checker = verify.checked_module(self.data[verify.CHECKER]) + mutant = copy.deepcopy(self.word) + mutant["scatter"][0].append(0) + with self.assertRaisesRegex(checker.Reject, r"targets not y \+ x: \[0\]"): + checker.check(mutant) + + def test_exporter_identifies_single_and_pair(self): + single, pair = copy.deepcopy(self.word), copy.deepcopy(self.word) + single["scatter"][0].append(0) + pair["scatter"][0].extend([0, 0]) + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + first = verify.export(self.data[verify.EXPORTER], single, root / "single") + second = verify.export(self.data[verify.EXPORTER], pair, root / "pair") + self.assertEqual(first, second) + self.assertEqual(len(first) // 24, 27235) + + def test_record_oracle_against_literal_endpoint(self): + base = b"".join(struct.pack("<6i", 1, 111 + i, i, 1, 0, 3) for i in range(111)) + _, differences = verify.replay(base, self.word) + self.assertEqual(differences, []) + extra = struct.pack("<6i", 1, 111, 472, 1, 0, 3) + values, differences = verify.replay(base + extra, self.word) + self.assertEqual(differences, [(111, 1 << 472)]) + self.assertEqual( + verify.witness(values, differences, self.word), + { + "output_register": 111, + "input_column": 472, + "actual_bit": 1, + "expected_bit": 0, + "difference_support": [472], + }, + ) + self.assertEqual(values[472], 1 << 472) + + def test_record_lifecycle_and_alignment(self): + for raw in ( + b"x", + struct.pack("<6i", 4, 0, 0, 0, 0, 0), + struct.pack("<6i", 2, 472, 661, 0, 0, 0), + struct.pack("<6i", 1, 111, 661, 1, 0, 0), + struct.pack("<6i", 3, 472, 661, 0, 0, 0), + ): + with self.subTest(raw=raw), self.assertRaises(ValueError): + verify.replay(raw, self.word) + + def test_each_source_corruption_rejects(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + for path, body in self.data.items(): + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(body) + self.assertEqual(verify.sources(root), self.data) + for path, body in self.data.items(): + target = root / path + target.write_bytes(body + b" ") + with ( + self.subTest(path=path), + self.assertRaisesRegex(ValueError, "source:"), + ): + verify.sources(root) + target.write_bytes(body) + self.assertEqual(verify.sources(root), self.data) + + def test_optimized_read_only_replay(self): + before = { + p.name: p.read_bytes() for p in verify.PACKAGE.iterdir() if p.is_file() + } + run = subprocess.run( + [ + sys.executable, + "-I", + "-O", + "-Werror", + "-B", + str(verify.PACKAGE / "verify.py"), + ], + check=False, + capture_output=True, + text=True, + timeout=30, + ) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn("PASS_SELECTED_SCATTER_EXPORT_PARITY_AUDIT", run.stdout) + self.assertEqual( + before, + {p.name: p.read_bytes() for p in verify.PACKAGE.iterdir() if p.is_file()}, + ) + + def test_typed_receipt_corruption(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + for name in ("verify.py", "SOURCES.json", "RESULT.json"): + shutil.copyfile(verify.PACKAGE / name, root / name) + receipt = json.loads((root / "RESULT.json").read_bytes()) + receipt["normalized_export_equals_baseline"] = 1 + (root / "RESULT.json").write_text(json.dumps(receipt)) + run = subprocess.run( + [ + sys.executable, + "-I", + "-O", + "-B", + str(root / "verify.py"), + "--root", + str(verify.ROOT), + ], + check=False, + capture_output=True, + text=True, + timeout=30, + ) + self.assertNotEqual(run.returncode, 0) + self.assertIn("typed deterministic receipt", run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/scatter-export-parity-audit/verify.py b/research/scatter-export-parity-audit/verify.py new file mode 100644 index 0000000000..3e32c1f00c --- /dev/null +++ b/research/scatter-export-parity-audit/verify.py @@ -0,0 +1,241 @@ +"""Source-bound scatter/export counterexample. Nick Petalas, Apache-2.0.""" + +import argparse +import copy +import gzip +import hashlib +import json +import struct +import subprocess +import sys +import tempfile +import types +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PREFIX = "research/e8-bit-p111-tuned/" +WORD = PREFIX + "tune/bitE8mut-p111-tuned.json.gz" +CHECKER = PREFIX + "code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" +SELECTED = "research/community-frontier1094-audit/SELECTED-SOURCE.json" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sources(root): + rows = json.loads((PACKAGE / "SOURCES.json").read_bytes())["files"] + require(0 < len(rows) <= 24, "bounded source inventory") + result = {} + for row in rows: + if row["usage"] != "input": + continue + path = row["path"] + require( + not Path(path).is_absolute() and ".." not in Path(path).parts, + "contained input", + ) + require(path not in result, "unique source input") + target = root / path + require(target.stat().st_size <= 5 * 1024 * 1024, "bounded source bytes") + body = target.read_bytes() + require(hashlib.sha256(body).hexdigest() == row["sha256"], "source: " + path) + result[path] = body + selected = json.loads(result[SELECTED])["files"] + for path in (WORD, CHECKER, EXPORTER): + require( + hashlib.sha256(result[path]).hexdigest() == selected[path], + "selected source binding: " + path, + ) + return result + + +def checked_module(body): + module = types.ModuleType("pinned_xcheck") + # Exact authenticated module; retain its checks under an optimized caller. + exec(compile(body, CHECKER, "exec", optimize=0), module.__dict__) # noqa: S102 + return module + + +def validate_scatter(word): + """Sufficient boundary guard; deliberately requires a simple support list.""" + rows, retained = word["scatter"], word["ret"] + require(type(rows) is list and len(rows) == word["v"], "scatter row inventory") + require(type(retained) is list and len(retained) == 9, "retained inventory") + for row in rows: + require(type(row) is list and len(row) <= len(retained), "scatter row shape") + require( + all(type(k) is int and 0 <= k < len(retained) for k in row), "scatter index" + ) + require(len(row) == len(set(row)), "duplicate scatter index") + + +def symbolic(checker, word): + _, labels, full, hypotheses, conclusions, _ = checker.check(word) + require(labels["labels"] == 111 and full["columns"] == 661, "selected dimensions") + require(all(hypotheses.values()) and all(conclusions.values()), "full interface") + return { + "columns": full["columns"], + "scatter_terms": full["scatter_terms"], + "hypotheses": hypotheses, + "conclusions": conclusions, + } + + +def export(body, word, directory): + directory.mkdir() + script = directory / "export_records.py" + script.write_bytes(body) + argument = directory / "word.json" + argument.write_text(json.dumps(word)) + output = directory / "records" + run = subprocess.run( + [sys.executable, "-I", "-B", str(script), str(argument), str(output)], + check=False, + capture_output=True, + text=True, + timeout=30, + ) + require(run.returncode == 0, "export failed: " + run.stderr) + records = (output / "249-records.bin").read_bytes() + require( + 0 < len(records) <= 30000 * 24 and len(records) % 24 == 0, + "bounded aligned record stream", + ) + return records + + +def replay(records, word): + """Independent F2 row-bitsets, one bit for every arbitrary input column.""" + require( + 0 < len(records) <= 30000 * 24 and len(records) % 24 == 0, + "bounded aligned record stream", + ) + n, v = 2 * word["v"] + word["R"], word["v"] + require(n == 661, "bounded column inventory") + values = [1 << i for i in range(n)] + [0] + opened = None + for op, first, second, coefficient, _frame, _phase in struct.iter_unpack( + "<6i", records + ): + require(0 <= first <= n and 0 <= second <= n, "record register") + if op == 0: + continue # Frame movement does not alter this scalar projection. + if op == 1: + require(first != n and (second != n or opened is not None), "ADD shape") + if coefficient % 2: + values[first] ^= values[second] + elif op == 2: + require(opened is None and second == n and first < n, "COPY shape") + values[n], opened = values[first], first + elif op == 3: + require(opened == first and second == n, "ERASE source binding") + values[n], opened = 0, None + else: + raise ValueError("record opcode") + require(opened is None and values[n] == 0, "temporary closes") + expected = [1 << i for i in range(n)] + for t in range(v): + expected[v + t] ^= 1 << t + differences = [ + (i, values[i] ^ expected[i]) for i in range(n) if values[i] != expected[i] + ] + return values, differences + + +def witness(values, differences, word): + require( + len(differences) == 1 and differences[0][0] == word["v"], + "only first target differs", + ) + register, delta = differences[0] + require(delta >> 472 & 1, "independent dirty-input witness") + return { + "output_register": register, + "input_column": 472, + "actual_bit": (values[register] >> 472) & 1, + "expected_bit": 0, + "difference_support": [i for i in range(661) if delta >> i & 1], + } + + +def audit(root, directory): + data = sources(root) + checker = checked_module(data[CHECKER]) + word = json.loads(gzip.decompress(data[WORD])) + validate_scatter(word) + original = symbolic(checker, word) + require( + 0 not in word["scatter"][0] and word["ret"][0] == 472, "exact mutation site" + ) + baseline = export(data[EXPORTER], word, directory / "baseline") + _, bad = replay(baseline, word) + require(not bad, "positive exported endpoint") + mutant = copy.deepcopy(word) + mutant["scatter"][0].extend([0, 0]) + changed = symbolic(checker, mutant) + require( + changed == {**original, "scatter_terms": original["scatter_terms"] + 2}, + "symbolic mutation is null except term count", + ) + broken = export(data[EXPORTER], mutant, directory / "mutant") + values, differences = replay(broken, mutant) + counterexample = witness(values, differences, mutant) + try: + validate_scatter(mutant) + except ValueError as error: + guard = str(error) + else: + raise ValueError("boundary guard accepted duplicate") + normalized = copy.deepcopy(mutant) + normalized["scatter"][0] = [ + k for k in range(9) if mutant["scatter"][0].count(k) % 2 + ] + require(normalized == word, "parity normalization recovers this exact source") + repaired = export(data[EXPORTER], normalized, directory / "normalized") + require(repaired == baseline, "normalized export byte identity") + return { + "status": "PASS_SELECTED_SCATTER_EXPORT_PARITY_AUDIT", + "columns": 661, + "retained_register": 472, + "target_row": 0, + "baseline": { + "records": len(baseline) // 24, + "records_sha256": hashlib.sha256(baseline).hexdigest(), + "symbolic": original, + }, + "mutant": { + "appended_indices": [0, 0], + "records": len(broken) // 24, + "records_sha256": hashlib.sha256(broken).hexdigest(), + "symbolic": changed, + "witness": counterexample, + }, + "duplicate_guard": guard, + "normalized_export_equals_baseline": True, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix="scatter-export-audit-") as temporary: + result = audit(args.root, Path(temporary)) + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((PACKAGE / "RESULT.json").read_bytes()) + require( + json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "typed deterministic receipt", + ) + print(result["status"], "columns=661 changed_targets=1 no_new_kappa") + + +if __name__ == "__main__": + main()