Repository navigation
Reproduce the paired-null scatter mutant and decide the multiplicity contract at the checker/exporter boundary (no new kappa) - #3801
Merged
Mister-Meeseeks merged 1 commit intoOct 20, 2026
Conversation
…he multiplicity contract Reproduces the CrocSwap#2977 paired-null scatter counterexample from the pinned selected bytes on an independent record route: the checker XORs per occurrence, the exporter lowers by membership, and the exact divergence class is positive even multiplicity. Sweeps multiplicities 0..6, matches the archived record-byte receipts and the 98-column witness, censuses the producer chain and the two pinned words (rows are simple), probes index types, and records the successor boundary decision. No new kappa. Package: research/scatter-boundary-decision
Contributor
Author
|
CI outcome: plan pass (1m54s) and replay (research/scatter-boundary-decision) pass (2m20s) on head |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Independent reproduction of the archived #2977 scatter/export counterexample, plus a tested decision for the successor checker/exporter boundary. No new κ, no supplier, no selected-frontier change.
Package:
research/scatter-boundary-decision/. Cardsupplier-boundary-audit, scope refined to the archived package's own stated next step. Base20ecf2891d80b5acf18d980b2164fb44ea7faa90(canonical main, fetched this round). Branchresearch/w2-1018b-scatter-boundary-decision.What is established, and at what strength
m = 0..6of one index in row 0 of the pinned tuned word: the checker accepts exactly evenm; the exporter emits one extra record for everym >= 1(membership); parity-normalised export matches the mutant export for everymexcept2, 4, 6. The checker XORs a copied total once per occurrence, the exporter emits one ADD when the index occurs at all, and the two lowerings agree exactly when every positive multiplicity is odd. The hazard class that can reach the exporter through a checked pipeline is exactly the positive even multiplicities.ea44aa04…ef09a; pair mutant 27,235 records5629b522…dce744; one changed target register 111 with the archived 98-column difference support and input column 472.decoder_rows(gen_p3) builds rows fromitertools.combinations(strictly increasing),pwordl.buildcopies rows,tune/apply.pynever mentionsscatter, the tuned word's rows are byte-equal to the untuned base word's rows, and both pinned words measure zero repeated rows and maximum multiplicity 1.trueis accepted as1by both stages, a float index crashes the checker with an uncaughtTypeErrorwhile the exporter silently lowers it, and a string index never matches the exporter.Route and independence
The pinned
xcheck_p.pyandexport_records.pyrun unchanged as black-box executables; the record stream is interpreted by a separately written reader whose semantics come from the exporter's own docstring, not from the archived package's replay. The archivedRESULT.jsonis pinned as a live input and compared exactly.Verification
Local, from the repository root, with
~/git/integer-mult-bounds/.venv/bin/python3.12(CPython 3.12, macOS arm64, standard library only):Registered replay commands total about 45 s locally, well inside the 10-minute CI cap. The native scalar check rejecting the mutant endpoint was rerun once from the archived package's own harness as a local black-box control (
PASS_SCATTER_EXPORT_NATIVE_PARITY_CONTROL native_legality_accepts=3 scalar_rejects=2); it is a rerun of that control, not an independently written native route, and it is not registered as a CI check.Limits
Finite reproduction and boundary decision on the pinned selected bytes; not a theorem about all bit words or producers. The row census covers the two words in the selected tuned chain only. No supplier, tariff, record or selected-frontier change; frozen packages stay unchanged. The native route is not independently re-implemented.
Credit
The counterexample, fixture and opt-in guard are Nick Petalas's (#2977); eumemic wrote the punctured generator and word checker lineage, DreamingOfClouds the punctured-star construction lineage, Dylan Crow the exporter and native checkers, and Douglas Colkitt the selected source bindings and review. This package is by Nick Petalas, produced with AI assistance. Apache-2.0. Independent human and formal proof-kernel review are unclaimed.