Skip to content

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 into
CrocSwap:mainfrom
petalas:research/w2-1018b-scatter-boundary-decision
Oct 20, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/w2-1018b-scatter-boundary-decision

Conversation

@petalas

@petalas petalas commented Oct 18, 2026

Copy link
Copy Markdown
Contributor

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/. Card supplier-boundary-audit, scope refined to the archived package's own stated next step. Base 20ecf2891d80b5acf18d980b2164fb44ea7faa90 (canonical main, fetched this round). Branch research/w2-1018b-scatter-boundary-decision.

What is established, and at what strength

  1. Exact divergence class (measured). Sweeping appended occurrences m = 0..6 of one index in row 0 of the pinned tuned word: the checker accepts exactly even m; the exporter emits one extra record for every m >= 1 (membership); parity-normalised export matches the mutant export for every m except 2, 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.
  2. Archived receipt reproduced byte-for-byte. Baseline 27,234 records ea44aa04…ef09a; pair mutant 27,235 records 5629b522…dce744; one changed target register 111 with the archived 98-column difference support and input column 472.
  3. Producer guarantee measured. decoder_rows (gen_p3) builds rows from itertools.combinations (strictly increasing), pwordl.build copies rows, tune/apply.py never mentions scatter, 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.
  4. Successor decision. Enforce simple supports in both stages while the retained generator is the only producer; if multiplicity ever becomes meaningful, canonicalise rows to parity in the exporter. Both options must declare integer index types: true is accepted as 1 by both stages, a float index crashes the checker with an uncaught TypeError while the exporter silently lowers it, and a string index never matches the exporter.

Route and independence

The pinned xcheck_p.py and export_records.py run 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 archived RESULT.json is 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):

python3.12 -B scripts/research_package.py --package research/scatter-boundary-decision
# PASS_REGISTERED_RESEARCH_PACKAGE research/scatter-boundary-decision outcome=completed (44 s)
python3.12 -B scripts/check_research_commit.py --package research/scatter-boundary-decision --check-source-history
# PASS_RESEARCH_COMMIT_BYTES {..., "files": 16, "source_history_commits": ["20ecf2891…"]}
python3.12 -I -Werror -B research/scatter-boundary-decision/verify.py
# PASS_SCATTER_BOUNDARY_DECISION columns=661 hazard=[2,4,6] no_new_kappa (21 s)
python3.12 -I -O -Werror -B research/scatter-boundary-decision/test_verify.py
# 7 tests OK (23 s)

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.

…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
@petalas

petalas commented Oct 18, 2026

Copy link
Copy Markdown
Contributor Author

CI outcome: plan pass (1m54s) and replay (research/scatter-boundary-decision) pass (2m20s) on head 911f8800ba7a4b03603ef62c5ffc6240e53cb5fd (run 39167854785). The same two registered commands also pass locally under the CPython 3.12 virtualenv interpreter.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants