diff --git a/research/census-prune-source-impact/INVENTORY.json b/research/census-prune-source-impact/INVENTORY.json new file mode 100644 index 0000000000..c7d4000097 --- /dev/null +++ b/research/census-prune-source-impact/INVENTORY.json @@ -0,0 +1,387 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "faulty_engine_sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "pinned": [ + { + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "pr": 2542, + "role": "FAULTY_ENGINE", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "evidence": [ + "def cyclic_census", + "nq & 1" + ] + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "pr": 2634, + "role": "FAULTY_ENGINE", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "evidence": [ + "def cyclic_census" + ] + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "pr": 2773, + "role": "FAULTY_ENGINE", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "evidence": [ + "def cyclic_census" + ] + }, + { + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "pr": 2691, + "role": "FAULTY_NATIVE_RULE", + "sha256": "b4722f59811b9920e1f364e68a228ad5ad34cf98f9c490a3655d78dc2e9ae23b", + "evidence": [ + "nq\\s*&\\s*1", + "BUDGET\\s+27|BUDGET\\s*=\\s*27" + ] + }, + { + "path": "research/universal-f7-singleton-seedb859517b/search.py", + "pr": 2542, + "role": "RETIRED_EXCLUSION_CALLER", + "sha256": "d8bad428035806848f9e0dc6caa3193e1a9abbad6a589dff3ef0e0b66f5f006c", + "evidence": [ + "cyclic_census\\(7, 18, budget=9, simple=True" + ] + }, + { + "path": "research/universal-f7-singleton-seedb859517b/README.md", + "pr": 2542, + "role": "RETIRED_EXCLUSION_CLAIM", + "sha256": "c3c541a5019aad83b95228de4472c8ab149cec376666b431d4dab57bca72f246", + "evidence": [ + "20\\s*(<=|≤)\\s*f\\(7\\)|f\\(7\\)\\s*(>=|≥)\\s*20\\b", + "15,?775,?992" + ] + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "pr": 2634, + "role": "RETIRED_EXCLUSION_CALLER", + "sha256": "b403d815dad917440e238a7cafe4e15aa296f590e87c85c86653f06cba243055", + "evidence": [ + "cyclic_census\\(", + "budget\\s*=\\s*27|BUDGET\\s*=\\s*27" + ] + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/README.md", + "pr": 2634, + "role": "RETIRED_EXCLUSION_CLAIM", + "sha256": "01ecc4b0c133f9853144c363fa988c89ae967521de326e1c62db0ddc0d7a9bec", + "evidence": [ + "798,?901,?058" + ] + }, + { + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md", + "pr": 2691, + "role": "RETIRED_EXCLUSION_CLAIM", + "sha256": "d0435c3637b8fb756b6e05783a47e148e1737ee13faaac634a3432ccffd1228f", + "evidence": [ + "6,?305,?209,?079", + "\\(10,10\\)" + ] + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "pr": 2773, + "role": "HISTORICAL_ANCHOR_CALLER", + "sha256": "2e6b6dadb285ae30115629c7dd0ed441f4e61e1979ddacbe129ef31926114278", + "evidence": [ + "cyclic_census\\(7, 18, budget=9, simple=True", + "\"hits\": 0" + ] + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/README.md", + "pr": 2773, + "role": "STALE_CITATION", + "sha256": "753eeec4f8dd171b1662153dd4ba9b887c56f331e44af552d1dfaa36190c368b", + "evidence": [ + "20\\s*(<=|≤)\\s*f\\(7\\)|f\\(7\\)\\s*(>=|≥)\\s*20\\b", + "15,?775,?992", + "even-weight|even weight" + ] + }, + { + "path": "research/f7-17point-fourier-obstruction-seedb5e318fe/verify.py", + "pr": 2870, + "role": "HISTORICAL_ANCHOR_RECEIPT", + "sha256": "a4c03264fb68bf0ae95a684c093f36772a0a73469bd6966895042dac4c9d2644", + "evidence": [ + "\"l18_universal\": 0", + "\"l18_nodes\": 15775992" + ] + }, + { + "path": "research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json", + "pr": 2911, + "role": "HISTORICAL_ANCHOR_RECEIPT", + "sha256": "00bae824caa6b7eba6165290a9cfded9a09b63f4332dd7a8e38696c1b0f82974", + "evidence": [ + "15,?775,?992", + "universal" + ] + }, + { + "path": "research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json", + "pr": 2933, + "role": "HISTORICAL_ANCHOR_RECEIPT", + "sha256": "3400b4a2b3cbc00082d278a393832f80143d913ec7c7a2b1fcd73cf8e341fa5f", + "evidence": [ + "\"l18_universal\": 0" + ] + }, + { + "path": "research/f7-18point-tight-classes-seed4c1e7b30/README.md", + "pr": 2961, + "role": "STALE_CITATION", + "sha256": "3e539305c90e770c2794d1945497df7dd7c51ccdb6ff836d2b3438f1075687d4", + "evidence": [ + "20\\s*(<=|≤)\\s*f\\(7\\)|f\\(7\\)\\s*(>=|≥)\\s*20\\b" + ] + }, + { + "path": "research/f7-18point-avtail-seed010d26fa/README.md", + "pr": 3023, + "role": "STALE_CITATION", + "sha256": "ca9f89f813bac5180cb25ab3db2b7336966edff3e86b5d7b9cb016426cc6c9fd", + "evidence": [ + "20\\s*(<=|≤)\\s*f\\(7\\)|f\\(7\\)\\s*(>=|≥)\\s*20\\b", + "01021323", + "unaffected by that correction" + ] + }, + { + "path": "research/f7-bit0-false-prune/verify.py", + "pr": 3096, + "role": "AUDIT_CALLER", + "sha256": "eee36f4d00dba9ecd39cf35df283ee7575154ae272ce91f50f538c99912053a0", + "evidence": [ + "cyclic_census", + "01021323" + ] + }, + { + "path": "research/f7-set-word-pruning-boundary/verify.py", + "pr": 3215, + "role": "AUDIT_CALLER", + "sha256": "8ff0b6fa72e69ef892eba7922ecf61808d28c9be15ce684b436225651b187c6e", + "evidence": [ + "cyclic_census", + "01021323" + ] + }, + { + "path": "research/connector-capacity-parity-audit/verify.py", + "pr": 3224, + "role": "AUDIT_CALLER", + "sha256": "57a0ff10eb991a21b345a7c9cbfc502a64b4943c77d1e3d401febe486d8eeb54", + "evidence": [ + "cyclic_census" + ] + }, + { + "path": "research/f7-independent-full-replay/verify.py", + "pr": 3333, + "role": "AUDIT_CALLER", + "sha256": "77c59038be801a79908b543a7e1175931f7d6dd1a299dc3d9bf8716a00a35d46", + "evidence": [ + "cyclic_census" + ] + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "pr": 2973, + "role": "REPLACEMENT_ENGINE", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a", + "evidence": [ + "Hamming-weight parity", + "__builtin_popcount", + "parity\\(nq\\)" + ] + }, + { + "path": "research/f7-union-support-audit/census.cpp", + "pr": 3005, + "role": "REPLACEMENT_ENGINE", + "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949", + "evidence": [ + "std::popcount" + ] + }, + { + "path": "research/f7-independent-full-replay/replay.c", + "pr": 3333, + "role": "REPLACEMENT_ENGINE", + "sha256": "7dd0c29fbadfd54aa6ba985745bfff5703b281a5746cfe042166bfb561101a4c", + "evidence": [ + "parity" + ] + }, + { + "path": "research/f7-l22-union-census/engine/union_census.c", + "pr": 3818, + "role": "REPLACEMENT_ENGINE", + "sha256": "d34a322fc6c9fd41bc9dae337d3e84923f9dfb938c1af42de491cf536fe3cabe", + "evidence": [ + "__builtin_popcount", + "parity\\(nq\\)" + ] + }, + { + "path": "research/f7-l22-deep-shard-census/deep_census.py", + "pr": 4221, + "role": "REPLACEMENT_DRIVER", + "sha256": "9a63bed90a4ea0e1254bdd43fd35b0d4a846f71c1ad2feb7ae166e8a2082b690", + "evidence": [ + "union_census" + ] + }, + { + "path": "research/connector-covering-code/README.md", + "pr": 3058, + "role": "REPLACEMENT_SET_LEVEL", + "sha256": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4", + "evidence": [ + "f\\(7\\) >= 22 follows from sections 1-2 alone", + "uses neither the PR2542/PR2634/PR2691 censuses" + ] + } + ], + "coverage": [ + { + "prefix": "research/universal-f7-singleton-seedb859517b/", + "class": "RETIRED_WORD_EXCLUSION", + "must_trigger": true, + "reason": "PR2542 (navinor): L18 simple-cycle word exclusion and f(7)>=20 made with the bit-0/balanced budget. Replacement: PR2973 L18 (9,9) row; PR3058 sections 1-2 give f(7)>=22 with no census." + }, + { + "prefix": "research/universal-f7-singleton-l20-seed06704c39/", + "class": "RETIRED_WORD_EXCLUSION", + "must_trigger": true, + "reason": "PR2634 (navinor): byte-identical engine; partial L20 simple-cycle census with budget 27. Replacement: PR2973 five L20 rows, PR3005, PR3333." + }, + { + "prefix": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/", + "class": "RETIRED_WORD_EXCLUSION", + "must_trigger": true, + "reason": "PR2691 (NicholasStone): native nq&1 grouping with BUDGET 27; (10,10) L20 receipt. Replacement: PR2973 (10,10) row, PR3005, PR3333." + }, + { + "prefix": "research/f7-17point-cover-audit-seedcfa215c2/", + "class": "SET_LEVEL_WITH_HISTORICAL_ANCHOR", + "must_trigger": true, + "reason": "PR2773 (navinor): set-level weight-parity rows; verify.py re-runs the PR2542 L18 counters from the vendored faulty engine as a reproduction anchor; README cites 20<=f(7) from PR2542." + }, + { + "prefix": "research/f7-17point-fourier-obstruction-seedb5e318fe/", + "class": "SET_LEVEL_WITH_HISTORICAL_ANCHOR", + "must_trigger": true, + "reason": "PR2870 (navinor): set-level Fourier rows; records the PR2542 L18 counters as an anchor receipt." + }, + { + "prefix": "research/f7-18point-cover-question-seed6d34356c/", + "class": "SET_LEVEL_WITH_HISTORICAL_ANCHOR", + "must_trigger": true, + "reason": "PR2911 (navinor): set-level; L18 anchor receipt and 20<=f(7) citation." + }, + { + "prefix": "research/f7-18point-vanishing-seedfc618722/", + "class": "SET_LEVEL_WITH_HISTORICAL_ANCHOR", + "must_trigger": true, + "reason": "PR2933 (navinor): set-level; L18 anchor receipt and 20<=f(7) citation." + }, + { + "prefix": "research/f7-18point-tight-classes-seed4c1e7b30/", + "class": "SET_LEVEL_STALE_CITATION", + "must_trigger": true, + "reason": "PR2961 (navinor): set-level; cites the 20<=f(7) gap only." + }, + { + "prefix": "research/f7-18point-avtail-seed010d26fa/", + "class": "SET_LEVEL_STALE_CITATION", + "must_trigger": true, + "reason": "PR3023 (navinor): set-level; cites 20<=f(7) at its base and records the PR2973 correction." + }, + { + "prefix": "research/f7-bit0-false-prune/", + "class": "AUDIT_CALLER", + "must_trigger": true, + "reason": "PR3096 (jwr404): calls the faulty engine to exhibit the false prune." + }, + { + "prefix": "research/f7-set-word-pruning-boundary/", + "class": "AUDIT_CALLER", + "must_trigger": true, + "reason": "PR3215 (commdata2338): six-file inventory and set-level joint_covers audit." + }, + { + "prefix": "research/connector-capacity-parity-audit/", + "class": "AUDIT_CALLER", + "must_trigger": true, + "reason": "PR3224 (commdata2338): calibration call of the faulty engine." + }, + { + "prefix": "research/f7-independent-full-replay/", + "class": "AUDIT_CALLER", + "must_trigger": true, + "reason": "PR3333 (1337isnot1337): predecessor-behaviour check plus an independent corrected replay." + }, + { + "prefix": "research/f7-weight-parity-census-correction/", + "class": "REPLACEMENT", + "must_trigger": true, + "reason": "PR2973 (NicholasStone): corrected engine; cites the old receipt only as history." + }, + { + "prefix": "research/community-", + "class": "INTAKE_ARCHIVE", + "must_trigger": true, + "reason": "Maintainer intake/audit records quoting PR bodies at intake time; frozen, not claims." + }, + { + "prefix": "docs/research/pr-ledger.json", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "PR ledger stores the PR2542 title." + }, + { + "prefix": "research/half-stage-evacuation/", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "Recent-PR title snapshot." + }, + { + "prefix": "research/paired-swap-normal45/FRONTIER.json", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "Recent-PR title snapshot." + }, + { + "prefix": "research/replica-tail-gain/references/", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "Recent-PR title snapshot." + }, + { + "prefix": "research/superior-replica-kappa/references/", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "Recent-PR title snapshot." + }, + { + "prefix": "research/tensor-block-kappa/references/", + "class": "PR_TITLE_LIST", + "must_trigger": true, + "reason": "Recent-PR title snapshot." + } + ] +} diff --git a/research/census-prune-source-impact/README.md b/research/census-prune-source-impact/README.md new file mode 100644 index 0000000000..e036e5381d --- /dev/null +++ b/research/census-prune-source-impact/README.md @@ -0,0 +1,176 @@ +# Whole-tree source impact of the bit-0 word-census prune + +**Source-impact audit with a finite calibration. No new f(7) bound, no new κ, +no change to any frozen package or to the selected frontier.** + +Card `census-pruning-audit` asks whether the word-census parity error reported +in Nicholas Stone's [PR2973](../f7-weight-parity-census-correction/README.md) +invalidates an exclusion that is still relied on. Earlier packages already +reconstruct `01021323` (#3096, #3821), trace the false prune into #2542 and +inventory six named call sites plus #2691's native rule +([#3215](../f7-set-word-pruning-boundary/README.md)), and replay the corrected +census independently (#3005, #3333). #3215 states that its inventory "is not a +whole-repository dependency proof". This package does that whole-tree check. + +**Answer at base `cef4b52f2a59009865bf8eabde1be3f159063703`.** The pruning rule +is disproved. No final bound is disproved, and no exclusion that the current +f(7) line relies on uses the faulty rule. Three word exclusions are retired and +already have replacement evidence. Six set-level packages carry stale anchors +or citations of the old lower bound. Those anchors and citations need reading +notes, not revalidation. + +## 1. The disproved rule, pinned + +| Old engine | Location | Rule | +|---|---|---| +| PR2542 `cyclic_census` (Aaron Wang) | byte-identical in `universal-f7-singleton-seedb859517b/engine.py` (PR2542), `universal-f7-singleton-l20-seed06704c39/engine.py` (PR2634), `f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py` (PR2773); SHA-256 `82e4c407…175e4` | groups prefix states by `nq & 1` (coordinate bit 0) and prunes on the caller's balanced budget | +| PR2691 `f7_census.c` (Nicholas Stone) | `universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c` | the same `nq & 1` grouping with `#define BUDGET 27` | + +Corrected engines pinned as replacements are #2973 `corrected_census.c`, #3005 +`census.cpp`, #3333 `replay.c` and #3818 `union_census.c`, which #4221's driver +runs. Each groups by Hamming-weight parity (popcount). None contains the faulty +bytes, a `cyclic_census` call or `nq & 1` grouping. This is a textual source +check, not a proof that these engines are sound. + +**Calibration, recomputed independently.** `01021323` has prefix states +`0,1,3,2,6,4,12,8,0`. Its eight states are distinct and cover all 16 masks. +The weight split is `(4,4)` with within-class excess 0. The bit-0 split is +`(6,2)` with excess 8. The balanced budget is `C(4,2)+C(4,2)-7 = 5`, while +the actual-size bit-0 budget is `C(6,2)+C(2,2)-7 = 9`. The old rule therefore +prunes this word at its eighth state, and the weight-parity rule does not. + +**Faulty bytes bound to the false prune.** The verifier loads the faulty +engine from authenticated bytes. It compares the engine with a separately +written oracle on the complete `n=4, L=8` simple restored domain. Without a +budget the engine returns exactly the oracle's 22 universal words. With the +balanced budget 5 it returns 16. The six missing words are +`01021323, 01023123, 01023213, 01213203, 01231203, 01231302`. An independent +bit-0/balanced replay rejects exactly these six words. The weight-parity rule +rejects none of the 22. The count matches #3096's recorded six simple false +prunes. This is a deliberate repetition, used only to tie the hash to the +defect. + +## 2. Whole-tree inventory + +`verify.py --rescan` walked 90,399 `.md/.json/.txt/.py/.c/.cpp/.cc/.h` files +under `research/`, `docs/`, `certificates/`, `scripts/` and `tests/`. The scan +looked for files that contain the faulty bytes, define or call +`cyclic_census`, use the native `nq&1` and `BUDGET` rule in C, quote the old +receipts, or state `20 <= f(7)` / `f(7) >= 20`. The receipts are #2542 L18 +15,775,992 nodes, #2634 partial L20 798,901,058 nodes and #2691 L20 +6,305,209,079 nodes. Every matching file falls under one of 21 classified +prefixes in [INVENTORY.json](INVENTORY.json). There are **0 unclassified** +files and **0 stale prefixes**. + +| Class | Files | Packages (PR, author) | Consequence | +|---|---:|---|---| +| Retired word exclusion | 28 | #2542, #2634 (navinor); #2691 (NicholasStone) | Their L18 simple-cycle, partial L20 and `(10,10)` L20 zero-hit receipts are filter counters, not exclusions. The replacement evidence is #2973's L18 `(9,9)` row and five L20 rows, corroborated by #3005 and #3333. #3058 §1–2 gives `f(7) >= 22` with no word census. | +| Set-level, historical anchor | 28 | #2773, #2870, #2911, #2933 (navinor) | Their set-level rows split by **weight parity**, as their README quotes show, so the bit-0 error does not transfer to them. #2773's `verify.py` re-runs the old L18 call from its vendored faulty engine and asserts `hits == 0`. #2870's `verify.py` and the #2911/#2933 `ANCHOR-REPRO.json` files record the same zero (`l18_universal: 0` or `universal_words=0`). These are reproducibility anchors of an unsound filter, not exclusion evidence. | +| Set-level, stale citation | 9 | #2961, #3023 (navinor) | They state the gap `20 <= f(7) <= 24` at their base. The bound remains true through replacement evidence. #3023 already records the #2973 correction. | +| Audit caller | 6 | #3096 (jwr404), #3215, #3224 (commdata2338), #3333 (1337isnot1337) | They call the faulty engine deliberately, to exhibit the false prune. | +| Replacement | 3 | #2973 (NicholasStone) | Cites the old receipt as history only. | +| Intake archive | 33 | `research/community-*` | Frozen maintainer intake records that quote PR bodies. They are not claims. | +| PR-title list | 9 | ledger and recent-PR snapshots | Store #2542's title, which reads "f(7) >= 20". | + +Twenty-six representative files are pinned by SHA-256 with quoted evidence and +role invariants. A faulty-bytes file must carry the faulty-engine role, a +caller must call `cyclic_census`, and a replacement must not call it or group +by `nq & 1`. The #3058 row must still state that `f(7) >= 22` follows from +§1–2 and that it uses none of the #2542/#2634/#2691 censuses. + +### Which downstream exclusions need revalidation + +* **Need replacement evidence.** Exactly the three retired word exclusions + above. All three already have it in merged packages. This audit does not + re-run those replacements. +* **Need no revalidation for this error.** The set-level 17- and 18-point + results of #2773 through #3023. Their own premises, such as the Sidon floor + censuses and the Fourier and vanishing censuses, are separate obligations + and are not checked here. +* **Need a reading note only.** The L18 `universal=0` anchors in #2773, #2870, + #2911 and #2933, and the `20 <= f(7)` citations in #2773 through #3023. The + bound now rests on #2973/#3058 rather than #2542. Annotating frozen packages + is a maintainer decision, so no file is edited here. + +**Bounded repair justified:** none beyond the replacement evidence that is +already merged and a possible annotation index (open question 1). Launching +another census would not change any decision identified here. + +## Limits + +The scan is syntactic. A consumer that relies on the old result without the +faulty bytes, a `cyclic_census` call, the receipts or the `20 <= f(7)` form +would be missed, for example prose such as "length 18 is excluded" with no +numbers. PR-number citations of #2542, #2634 and #2691 appear in 60+ packages, +mostly through the copied card text in `TASK.json`. They were inspected by +hand for the `f7-*`, `connector-*` and KB3 packages, not classified by +machine. The rescan is bound to the base commit: later trees may add +consumers, so it is a manual mode, not the registered command. The registered +command checks the pinned rows, the calibration and the controls. No Lean, +Docker or seven-label census was run. Scientific acceptance of #2973, #3058 +and #4221's `f(7)=24` claim is outside this package. + +## Reproduce + +Python 3.12 standard library, from the repository root: + +```sh +python3.12 -B research/census-prune-source-impact/verify.py # ~0.1 s +python3.12 -O -B research/census-prune-source-impact/verify.py +python3.12 -I -W error -B research/census-prune-source-impact/verify.py +python3.12 -B research/census-prune-source-impact/verify.py --rescan # ~40 s, base-bound +python3 scripts/research_package.py --package research/census-prune-source-impact --check-only +python3.12 -B scripts/research_package.py --package research/census-prune-source-impact +``` + +The expected marker is +`PASS_CENSUS_PRUNE_SOURCE_IMPACT pinned=26 false_prunes_n4L8=6/22 controls=7 no_new_kappa`. +`--rescan` appends `rescan_files=90399`. `--emit` prints the observed record +without comparing it to [RESULT.json](RESULT.json). + +There are seven controls, and each must fail. They are: an audit caller +relabelled as a replacement; the native bit-0 rule relabelled as a +replacement; a tampered pin; the #3058 evidence weakened to `f(7) >= 20`; +planted unclassified consumers in a temporary tree; the balanced bit-0 budget +on `01021323`; and bit-0 grouping substituted into the corrected rule, which +loses universal words. A separate mutation run killed all seven source +mutants: an off-by-one budget, weight replaced by bit 0, a changed word, a +relabelled stale citation, a relabelled faulty engine, a removed intake +prefix and a changed recorded result. + +## Open next questions + +1. **Should frozen packages with historical L18 anchors carry a reading note?** + #2773's `verify.py` prints `REPRO PR2542 L18 ... universal_words=0` from + the unsound filter, and #2870, #2911 and #2933 store the same counter. A + reader can take these for exclusion evidence. First step: a maintainer + decides between a central annotation index keyed by the paths in + `INVENTORY.json` and successor entry points. Blocked by: the frozen-package + policy, which is a maintainer decision. +2. **Can the single-engine L22 exclusions get a second implementation?** The + current `f(7)=24` word line at L22 (#3818, #4221) rests on one C engine, + whose union prune #3899 is auditing on tiny domains. First step: extend + #3005's separately written census past its `L <= 20` gate on one small + split, such as `(11,7)`. Blocked by: #3005's length gate and unmeasured L22 + throughput. +3. **Can the rescan be made semantic?** Phrase-level citations of the old + exclusions are not machine-detected. First step: add the patterns + "length 18 excluded" and "L = 18 ... excluded" and classify any new hits. + Blocked by: nothing structural. The false-positive rate is unmeasured. + +The structured versions are in [TASK.json](TASK.json). + +## Credit + +Ross Richardson supplied the PR943 prefix-walk model. Aaron Wang (navinor) +supplied PR2542/PR2634's word engine and the PR2773–PR3023 set-level chain. +Nicholas Stone supplied PR2691's native census and PR2973's correction, which +introduced `01021323`. Nick Petalas supplied PR3005, PR3708, PR3818 and +PR4221. conorholds supplied PR3058. jwr404 supplied PR3096 and PR3821, +commdata2338 supplied PR3215 and PR3224, and 1337isnot1337 supplied PR3333. +Douglas Colkitt supplied the research-package framework. This package adds +only the whole-tree inventory, its classification and the hash-to-defect +binding. It claims no priority over any of those results. + +Prepared by JoyboyBrian with substantial assistance from Anthropic Claude +(Claude Code, Opus 5.5). No independent human review is claimed. Apache-2.0. diff --git a/research/census-prune-source-impact/RESULT.json b/research/census-prune-source-impact/RESULT.json new file mode 100644 index 0000000000..f130ec4425 --- /dev/null +++ b/research/census-prune-source-impact/RESULT.json @@ -0,0 +1,92 @@ +{ + "calibration": { + "balanced_budget": 5, + "bit0_actual_budget": 9, + "bit0_excess": 8, + "bit0_split": [ + 6, + 2 + ], + "old_rule_first_prune_prefix": 8, + "prefix_states": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8, + 0 + ], + "weight_excess": 0, + "weight_split": [ + 4, + 4 + ], + "word": "01021323" + }, + "controls": [ + "audit caller relabelled as replacement", + "native bit-0 rule relabelled as replacement", + "tampered pinned hash", + "replacement evidence weakened to f(7)>=20", + "planted unclassified consumers flagged", + "balanced bit-0 budget rejects 01021323", + "bit-0 grouping substituted into corrected rule loses universal words" + ], + "inventory_roles": [ + "AUDIT_CALLER", + "FAULTY_ENGINE", + "FAULTY_NATIVE_RULE", + "HISTORICAL_ANCHOR_CALLER", + "HISTORICAL_ANCHOR_RECEIPT", + "REPLACEMENT_DRIVER", + "REPLACEMENT_ENGINE", + "REPLACEMENT_SET_LEVEL", + "RETIRED_EXCLUSION_CALLER", + "RETIRED_EXCLUSION_CLAIM", + "STALE_CITATION" + ], + "no_new_kappa": true, + "pinned_rows": 26, + "rescan": { + "files_scanned": 90399, + "stale_prefixes": [], + "trigger_files_by_class": { + "AUDIT_CALLER": 6, + "INTAKE_ARCHIVE": 33, + "PR_TITLE_LIST": 9, + "REPLACEMENT": 3, + "RETIRED_WORD_EXCLUSION": 28, + "SET_LEVEL_STALE_CITATION": 9, + "SET_LEVEL_WITH_HISTORICAL_ANCHOR": 28 + }, + "unclassified": [] + }, + "small_domain": { + "balanced_budget": 5, + "engine_false_prunes": [ + "01021323", + "01023123", + "01023213", + "01213203", + "01231203", + "01231302" + ], + "engine_hits_with_balanced_budget": 16, + "engine_hits_without_budget": 22, + "independent_bit0_balanced_rejects": [ + "01021323", + "01023123", + "01023213", + "01213203", + "01231203", + "01231302" + ], + "length": 8, + "n": 4, + "simple_universal_words": 22, + "weight_parity_balanced_rejects": 0 + } +} diff --git a/research/census-prune-source-impact/SOURCES.json b/research/census-prune-source-impact/SOURCES.json new file mode 100644 index 0000000000..072e9d40e2 --- /dev/null +++ b/research/census-prune-source-impact/SOURCES.json @@ -0,0 +1,174 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/connector-capacity-parity-audit/verify.py", + "usage": "input", + "git_blob": "77cbca8d917b4b998b8dc635b54cae72d9e1b72a", + "sha256": "57a0ff10eb991a21b345a7c9cbfc502a64b4943c77d1e3d401febe486d8eeb54" + }, + { + "path": "research/connector-covering-code/README.md", + "usage": "input", + "git_blob": "c194503e34e43988d5f83fec70a6f94e89e3db5d", + "sha256": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/README.md", + "usage": "input", + "git_blob": "3330e0cfda89644588271ec81d0b5cf6a5d297ea", + "sha256": "753eeec4f8dd171b1662153dd4ba9b887c56f331e44af552d1dfaa36190c368b" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "usage": "input", + "git_blob": "79a3fe6e4f1f8abe9b909923a218e8dc8c825842", + "sha256": "2e6b6dadb285ae30115629c7dd0ed441f4e61e1979ddacbe129ef31926114278" + }, + { + "path": "research/f7-17point-fourier-obstruction-seedb5e318fe/verify.py", + "usage": "input", + "git_blob": "125474a8ae77352eaa8447ffc44d8afb6c0b640a", + "sha256": "a4c03264fb68bf0ae95a684c093f36772a0a73469bd6966895042dac4c9d2644" + }, + { + "path": "research/f7-18point-avtail-seed010d26fa/README.md", + "usage": "input", + "git_blob": "cb4a992f05b06bbca038ab800bd8ba81fc056b30", + "sha256": "ca9f89f813bac5180cb25ab3db2b7336966edff3e86b5d7b9cb016426cc6c9fd" + }, + { + "path": "research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json", + "usage": "input", + "git_blob": "a18001b2178f80e1dce1e304b390d9f345f26de9", + "sha256": "00bae824caa6b7eba6165290a9cfded9a09b63f4332dd7a8e38696c1b0f82974" + }, + { + "path": "research/f7-18point-tight-classes-seed4c1e7b30/README.md", + "usage": "input", + "git_blob": "21ac6ddb2951c2746974c5657ffb8ac6a20df36d", + "sha256": "3e539305c90e770c2794d1945497df7dd7c51ccdb6ff836d2b3438f1075687d4" + }, + { + "path": "research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json", + "usage": "input", + "git_blob": "b40bc927186a981e948723db60cfd62cefb57eb3", + "sha256": "3400b4a2b3cbc00082d278a393832f80143d913ec7c7a2b1fcd73cf8e341fa5f" + }, + { + "path": "research/f7-bit0-false-prune/verify.py", + "usage": "input", + "git_blob": "7ebe9fe80b17b8e17acedd68da1ba3026c8d4c64", + "sha256": "eee36f4d00dba9ecd39cf35df283ee7575154ae272ce91f50f538c99912053a0" + }, + { + "path": "research/f7-independent-full-replay/replay.c", + "usage": "input", + "git_blob": "8b918ce92f540f2bf96a3c56444b9eab080c8ebd", + "sha256": "7dd0c29fbadfd54aa6ba985745bfff5703b281a5746cfe042166bfb561101a4c" + }, + { + "path": "research/f7-independent-full-replay/verify.py", + "usage": "input", + "git_blob": "5b6a657b8f62c885543c8dc903995953e7a0c1af", + "sha256": "77c59038be801a79908b543a7e1175931f7d6dd1a299dc3d9bf8716a00a35d46" + }, + { + "path": "research/f7-l22-deep-shard-census/deep_census.py", + "usage": "input", + "git_blob": "ad980727381fe15ec3ac32991ded97fbbef403a0", + "sha256": "9a63bed90a4ea0e1254bdd43fd35b0d4a846f71c1ad2feb7ae166e8a2082b690" + }, + { + "path": "research/f7-l22-union-census/engine/union_census.c", + "usage": "input", + "git_blob": "b2742d3f711b468b287acb3fb65e8d27938e448f", + "sha256": "d34a322fc6c9fd41bc9dae337d3e84923f9dfb938c1af42de491cf536fe3cabe" + }, + { + "path": "research/f7-set-word-pruning-boundary/verify.py", + "usage": "input", + "git_blob": "dd1db288d393e96be1acc1477b8592f0cde43286", + "sha256": "8ff0b6fa72e69ef892eba7922ecf61808d28c9be15ce684b436225651b187c6e" + }, + { + "path": "research/f7-union-support-audit/census.cpp", + "usage": "input", + "git_blob": "5b290af8c8dd74f0b5a8ad0aec9bf2d55492507d", + "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "usage": "input", + "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + { + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md", + "usage": "input", + "git_blob": "293dd0506025d53e417749b9d77a3b79a0dd8666", + "sha256": "d0435c3637b8fb756b6e05783a47e148e1737ee13faaac634a3432ccffd1228f" + }, + { + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "usage": "input", + "git_blob": "37d1c1ecfb705a55543dddfe87f43467cd4c50a2", + "sha256": "b4722f59811b9920e1f364e68a228ad5ad34cf98f9c490a3655d78dc2e9ae23b" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/README.md", + "usage": "input", + "git_blob": "4fd4a0a98c16ce80f02cc8cbb5217d39356243be", + "sha256": "01ecc4b0c133f9853144c363fa988c89ae967521de326e1c62db0ddc0d7a9bec" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "usage": "input", + "git_blob": "649272d37b29aedb44f5a275189d0f7c05840d7b", + "sha256": "b403d815dad917440e238a7cafe4e15aa296f590e87c85c86653f06cba243055" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/README.md", + "usage": "input", + "git_blob": "90e8452c0dbca6e2623f669335d0a408fc8c00d2", + "sha256": "c3c541a5019aad83b95228de4472c8ab149cec376666b431d4dab57bca72f246" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/search.py", + "usage": "input", + "git_blob": "2bb66b86822fdc248330ffb55bfe955ff4640ea9", + "sha256": "d8bad428035806848f9e0dc6caa3193e1a9abbad6a589dff3ef0e0b66f5f006c" + } + ] +} diff --git a/research/census-prune-source-impact/TASK.json b/research/census-prune-source-impact/TASK.json new file mode 100644 index 0000000000..6d83508b41 --- /dev/null +++ b/research/census-prune-source-impact/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "refined", + "actual_scope": "Whole-tree source-impact inventory of the unsound bit-0/balanced word-census prune at the base commit. Every file with the faulty engine bytes, a cyclic_census definition or call, the #2691 native rule, the old L18/L20 receipts or a 20<=f(7) citation is classified against replacement evidence. A calibration binds the faulty hash to the 01021323 false prune on the complete n=4, L=8 simple domain.", + "scope_change_reason": "The card's calibration, #2542 trace, small exhaustive domain and a six-file call-site inventory are already merged (#3096, #3821, #3215), as are independent corrected replays (#3005, #3333). #3215 states that its inventory is not a whole-repository dependency proof. This package takes that remaining obligation, which is the allowed 'one downstream dependency audit' variation. It repeats the calibration and the n=4, L=8 domain only to bind the faulty engine hash to the defect.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism. A whole-tree dependency boundary shows that no currently relied-upon f(7) exclusion uses the faulty rule, and it names the stale anchors, so no further census is needed to repair it.", + "budget_minutes": 90, + "stop_rule": "Stop after a pinned whole-tree classification at the base commit, a hash-to-defect calibration and rejection controls. No seven-label census, no L22 work, no edits to frozen packages, no supplier or frontier change.", + "outcome": "completed", + "evidence": "verify.py (default): 01021323 budgets (weight excess 0 within budget 5; bit-0 excess 8 against balanced budget 5 and actual budget 9); the faulty PR2542 engine bytes (SHA-256 82e4c407...) agree with an independent oracle on all 22 simple universal n=4, L=8 words without a budget and falsely prune exactly 6 with the balanced budget, while the weight-parity rule prunes 0; 26 pinned inventory files with quoted evidence and role invariants; 7 rejection controls. verify.py --rescan at base cef4b52: 90,399 files scanned, every trigger file (faulty bytes, cyclic_census, native nq&1/BUDGET rule, old L18/L20 receipts, 20<=f(7)) is under one of 21 classified prefixes, with 0 unclassified and 0 stale.", + "result": "The bit-0/balanced pruning rule is disproved. No final bound is disproved. The retired word exclusions are #2542 L18, #2634 partial L20 and #2691 (10,10) L20; all three have merged replacement evidence (#2973, #3005, #3333, #3058 sections 1-2). The set-level packages #2773-#3023 are unaffected by the bit-0 error. #2773, #2870, #2911 and #2933 carry L18 universal=0 anchors from the unsound filter, and #2773-#3023 cite 20<=f(7). Those need reading notes, not revalidation. The replacement engines contain no faulty bytes, no cyclic_census call and no nq&1 grouping.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", + "open_questions": [ + { + "question": "Should frozen packages with historical L18 anchors (#2773 verify.py, #2870, #2911, #2933 receipts) carry a reading note or a successor entry point?", + "why_it_matters": "Their PASS output prints universal_words=0 from the unsound filter, which a reader can take for exclusion evidence.", + "first_step": "A maintainer decides between a central annotation index keyed by INVENTORY.json paths and successor entry points.", + "blocked_by": "Frozen-package policy; this is a maintainer decision." + }, + { + "question": "Can the single-engine L22 exclusions (#3818, #4221) get a second, separately written implementation?", + "why_it_matters": "The f(7)=24 word line at L22 rests on one C engine; #3899 is auditing its union prune only on tiny domains.", + "first_step": "Extend #3005's census past its L<=20 gate on one small L22 split such as (11,7) and compare node-exactly with a capped union-engine run.", + "blocked_by": "#3005's length gate and unmeasured L22 throughput." + }, + { + "question": "Can the rescan detect phrase-level citations of the old exclusions?", + "why_it_matters": "Citations without the receipts, the faulty bytes or the 20<=f(7) form are invisible to the syntactic scan.", + "first_step": "Add patterns such as 'length 18 excluded' and classify every new hit at a fixed base.", + "blocked_by": "Nothing structural; the false-positive rate is unmeasured." + } + ] +} diff --git a/research/census-prune-source-impact/VERIFY.json b/research/census-prune-source-impact/VERIFY.json new file mode 100644 index 0000000000..bb4c88f8de --- /dev/null +++ b/research/census-prune-source-impact/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-capacity-parity-audit/verify.py", + "research/connector-covering-code/README.md", + "research/f7-17point-cover-audit-seedcfa215c2/README.md", + "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "research/f7-17point-fourier-obstruction-seedb5e318fe/verify.py", + "research/f7-18point-avtail-seed010d26fa/README.md", + "research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json", + "research/f7-18point-tight-classes-seed4c1e7b30/README.md", + "research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json", + "research/f7-bit0-false-prune/verify.py", + "research/f7-independent-full-replay/replay.c", + "research/f7-independent-full-replay/verify.py", + "research/f7-l22-deep-shard-census/deep_census.py", + "research/f7-l22-union-census/engine/union_census.c", + "research/f7-set-word-pruning-boundary/verify.py", + "research/f7-union-support-audit/census.cpp", + "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md", + "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "research/universal-f7-singleton-l20-seed06704c39/README.md", + "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "research/universal-f7-singleton-seedb859517b/README.md", + "research/universal-f7-singleton-seedb859517b/engine.py", + "research/universal-f7-singleton-seedb859517b/search.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "01021323 budgets; faulty PR2542 engine bytes against an independent oracle on the complete n=4, L=8 simple domain (6 of 22 universal words falsely pruned, weight-parity rule prunes none); 26 pinned inventory files with quoted evidence and role invariants; 7 rejection controls" + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under -O; the verifier uses explicit checks rather than assert" + } + ] +} diff --git a/research/census-prune-source-impact/verify.py b/research/census-prune-source-impact/verify.py new file mode 100644 index 0000000000..e89eae9e36 --- /dev/null +++ b/research/census-prune-source-impact/verify.py @@ -0,0 +1,375 @@ +#!/usr/bin/env python3 +"""Whole-tree source impact of the unsound bit-0 word-census prune. + +Default mode: + 1. recompute the 01021323 calibration (bit-0 versus weight-parity budgets); + 2. load the faulty PR2542 engine from authenticated bytes and compare it with + an independent oracle on the complete n=4, L=8 simple restored domain; + 3. authenticate every pinned inventory file and its quoted evidence, with + role-specific structural checks; + 4. run rejection controls (tampered role, tampered hash, planted unclassified + consumer, budget and grouping mutants). +--rescan additionally walks the working tree and requires every file that +mentions the faulty engine, its callers, the native rule or the old receipts to +fall under a classified prefix. That walk is bound to the recorded base commit; +later trees may legitimately add consumers. + +Python 3.12 standard library only. Explicit checks, not assert, so -O is safe. +Prepared by JoyboyBrian with substantial assistance from Anthropic Claude. +Apache-2.0. +""" + +import argparse +import copy +import hashlib +import json +import os +import re +import sys +import tempfile +import types +from itertools import combinations +from math import comb +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = "01021323" +MARKER = "PASS_CENSUS_PRUNE_SOURCE_IMPACT" +CODE_SUFFIXES = (".py", ".c", ".cpp", ".cc", ".h") +TEXT_SUFFIXES = (".md", ".json", ".txt") +SCAN_DIRS = ("research", "docs", "certificates", "scripts", "tests") +PROSE_TRIGGERS = { + "l18_receipt": re.compile(r"15,?775,?992"), + "l20_pr2634_partial_receipt": re.compile(r"798,?901,?058"), + "l20_pr2691_receipt": re.compile(r"6,?305,?209,?079"), + "f7_ge_20": re.compile(r"20\s*(<=|≤)\s*f\(7\)|f\(7\)\s*(>=|≥)\s*20\b"), +} +CALL = re.compile(r"(? cap: + return i + return None + + +def calibration(): + states = prefix_states(WORD) + points = states[:-1] + require(states == [0, 1, 3, 2, 6, 4, 12, 8, 0], "prefix states changed") + require(len(set(points)) == 8 and covers(points, 4), "01021323 is not a simple universal word") + w_split = tuple(len(c) for c in classes(points, weight)) + b_split = tuple(len(c) for c in classes(points, bit0)) + require(w_split == (4, 4) and b_split == (6, 2), "class sizes changed") + balanced, actual = budget(4, 4, 4), budget(*b_split, 4) + w_ex, b_ex = within_excess(points, weight), within_excess(points, bit0) + require((balanced, actual, w_ex, b_ex) == (5, 9, 0, 8), "budgets or excesses changed") + old_prune_at = first_violation(WORD, bit0, balanced) + require(old_prune_at is not None, "old rule no longer prunes the calibration word") + require(first_violation(WORD, weight, balanced) is None, "weight-parity rule prunes the calibration word") + require(first_violation(WORD, bit0, actual) is None, "actual-size bit-0 budget prunes the calibration word") + return { + "word": WORD, + "prefix_states": states, + "weight_split": list(w_split), + "bit0_split": list(b_split), + "weight_excess": w_ex, + "bit0_excess": b_ex, + "balanced_budget": balanced, + "bit0_actual_budget": actual, + "old_rule_first_prune_prefix": old_prune_at, + } + + +# ------------------------------------------------------- faulty engine binding + +def load_faulty_engine(inventory): + path = ROOT / inventory["pinned"][0]["path"] + data = path.read_bytes() + require(sha256(data) == inventory["faulty_engine_sha256"], "faulty engine bytes changed") + module = types.ModuleType("pr2542_engine_pinned") + module.__file__ = str(path) + exec(compile(data, str(path), "exec"), module.__dict__) + return module + + +def oracle_simple_universal(n, length): + """Restricted-growth words, every label used an even number >= 2 of times, + restored, with `length` distinct nonclosing states, universal.""" + out = [] + + def rec(prefix, top): + if len(prefix) == length: + word = "".join(map(str, prefix)) + if any(prefix.count(a) % 2 or prefix.count(a) == 0 for a in range(n)): + return + pts = prefix_states(word) + if pts[-1] != 0 or len(set(pts[:-1])) != length: + return + if covers(pts[:-1], n): + out.append(word) + return + for a in range(min(top + 1, n)): + rec(prefix + [a], max(top, a + 1)) + + rec([], 0) + return out + + +def small_domain(engine, functional_for_corrected=weight): + n, length = 4, 8 + truth = oracle_simple_universal(n, length) + balanced = budget(length // 2, length // 2, n) + plain = engine.cyclic_census(n, length, budget=None, simple=True) + pruned = engine.cyclic_census(n, length, budget=balanced, simple=True) + plain_w = sorted("".join(map(str, w)) for w in plain["words"]) + pruned_w = sorted("".join(map(str, w)) for w in pruned["words"]) + require(plain_w == sorted(truth), "faulty engine without budget disagrees with the oracle") + false_prunes = sorted(set(truth) - set(pruned_w)) + require(set(pruned_w) <= set(truth), "faulty engine reports a non-universal word") + corrected_rejects = [w for w in truth if first_violation(w, functional_for_corrected, balanced) is not None] + old_rule_rejects = sorted(w for w in truth if first_violation(w, bit0, balanced) is not None) + return { + "n": n, + "length": length, + "balanced_budget": balanced, + "simple_universal_words": len(truth), + "engine_hits_without_budget": plain["hits"], + "engine_hits_with_balanced_budget": pruned["hits"], + "engine_false_prunes": false_prunes, + "independent_bit0_balanced_rejects": old_rule_rejects, + "weight_parity_balanced_rejects": len(corrected_rejects), + } + + +# ----------------------------------------------------------------- inventory + +def validate_inventory(inventory, root): + faulty = inventory["faulty_engine_sha256"] + roles = {} + for row in inventory["pinned"]: + data = (root / row["path"]).read_bytes() + require(sha256(data) == row["sha256"], "pinned bytes changed: " + row["path"]) + text = data.decode("utf-8") + for pattern in row["evidence"]: + require(re.search(pattern, text), f"evidence {pattern!r} missing in {row['path']}") + role = row["role"] + has_call = bool(CALL.search(text)) + require((row["sha256"] == faulty) == (role == "FAULTY_ENGINE"), "faulty bytes must carry FAULTY_ENGINE: " + row["path"]) + if role == "FAULTY_ENGINE": + require(row["sha256"] == faulty, "faulty-engine row is not the faulty bytes: " + row["path"]) + elif role == "FAULTY_NATIVE_RULE": + require(NATIVE_RULE.search(text) and re.search(r"#define BUDGET 27\b", text), + "native rule row lacks bit-0 grouping with the balanced budget 27") + elif role in CALLER_ROLES: + require(has_call, "caller row does not call cyclic_census: " + row["path"]) + elif role in REPLACEMENT_ROLES: + require(row["sha256"] != faulty and not has_call and "def cyclic_census" not in text, + "replacement row uses the faulty engine: " + row["path"]) + require(not NATIVE_RULE.search(text), "replacement row groups by nq&1: " + row["path"]) + roles[row["path"]] = role + retired = {r["pr"] for r in inventory["pinned"] if r["role"].startswith(("FAULTY", "RETIRED"))} + replacement = {r["pr"] for r in inventory["pinned"] if r["role"] in REPLACEMENT_ROLES} + require(retired == {2542, 2634, 2691, 2773} and not retired & replacement, "retired/replacement split changed") + return sorted(set(roles.values())) + + +def classify(path, coverage): + for entry in coverage: + if path.startswith(entry["prefix"]): + return entry + return None + + +def triggers(rel, data, faulty): + found = [] + if rel.endswith(CODE_SUFFIXES): + if sha256(data) == faulty: + found.append("faulty_engine_bytes") + text = data.decode("utf-8", "ignore") + if CALL.search(text) or "def cyclic_census" in text: + found.append("cyclic_census") + if rel.endswith((".c", ".cpp", ".cc", ".h")) and NATIVE_RULE.search(text) and "BUDGET" in text: + found.append("native_bit0_rule") + if rel.endswith(TEXT_SUFFIXES + CODE_SUFFIXES): + text = data.decode("utf-8", "ignore") + found += [k for k, rx in PROSE_TRIGGERS.items() if rx.search(text)] + return found + + +def rescan(inventory, root, dirs=SCAN_DIRS): + by_class, unclassified, hit_prefixes, files = {}, [], set(), 0 + skip = os.path.relpath(PACKAGE, root) + os.sep + for top in dirs: + base = root / top + if not base.is_dir(): + continue + for dirpath, dirnames, filenames in os.walk(base): + dirnames[:] = sorted(d for d in dirnames if d not in (".git", "__pycache__")) + for name in sorted(filenames): + full = Path(dirpath) / name + rel = full.relative_to(root).as_posix() + if rel.startswith(skip.replace(os.sep, "/")) or not rel.endswith(TEXT_SUFFIXES + CODE_SUFFIXES): + continue + files += 1 + found = triggers(rel, full.read_bytes(), inventory["faulty_engine_sha256"]) + if not found: + continue + entry = classify(rel, inventory["coverage"]) + if entry is None: + unclassified.append((rel, found)) + continue + hit_prefixes.add(entry["prefix"]) + by_class[entry["class"]] = by_class.get(entry["class"], 0) + 1 + stale = sorted(e["prefix"] for e in inventory["coverage"] if e["must_trigger"] and e["prefix"] not in hit_prefixes) + return {"files_scanned": files, "trigger_files_by_class": dict(sorted(by_class.items())), + "unclassified": unclassified, "stale_prefixes": stale} + + +# ------------------------------------------------------------------ controls + +def expect_fail(fn, label): + try: + fn() + except Fail: + return label + raise Fail("control did not fail: " + label) + + +def controls(inventory, engine): + done = [] + bad = copy.deepcopy(inventory) + idx = next(i for i, r in enumerate(bad["pinned"]) if r["path"].endswith("f7-bit0-false-prune/verify.py")) + bad["pinned"][idx]["role"] = "REPLACEMENT_ENGINE" + done.append(expect_fail(lambda: validate_inventory(bad, ROOT), "audit caller relabelled as replacement")) + bad = copy.deepcopy(inventory) + bad["pinned"][3]["role"] = "REPLACEMENT_ENGINE" + done.append(expect_fail(lambda: validate_inventory(bad, ROOT), "native bit-0 rule relabelled as replacement")) + bad = copy.deepcopy(inventory) + bad["pinned"][-1]["sha256"] = "0" * 64 + done.append(expect_fail(lambda: validate_inventory(bad, ROOT), "tampered pinned hash")) + bad = copy.deepcopy(inventory) + bad["pinned"][-1]["evidence"] = [r"f\(7\) >= 20 follows from sections 1-2 alone"] + done.append(expect_fail(lambda: validate_inventory(bad, ROOT), "replacement evidence weakened to f(7)>=20")) + with tempfile.TemporaryDirectory() as tmp: + troot = Path(tmp) + (troot / "research" / "planted").mkdir(parents=True) + (troot / "research" / "planted" / "x.py").write_text("r = cyclic_census(7, 18, budget=9)\n") + (troot / "research" / "planted" / "y.md").write_text("gap 20 <= f(7) <= 24\n") + (troot / "research" / "community-x").mkdir() + (troot / "research" / "community-x" / "p.json").write_text('{"n": "15,775,992"}\n') + result = rescan(inventory, troot) + require(sorted(p for p, _ in result["unclassified"]) == ["research/planted/x.py", "research/planted/y.md"] + and result["trigger_files_by_class"] == {"INTAKE_ARCHIVE": 1}, + "rescan control misclassified planted files") + done.append("planted unclassified consumers flagged") + require(first_violation(WORD, bit0, budget(4, 4, 4)) is not None, "balanced bit-0 mutant") + done.append("balanced bit-0 budget rejects 01021323") + mutant = small_domain(engine, functional_for_corrected=bit0) + require(mutant["weight_parity_balanced_rejects"] > 0, "grouping mutant undetected") + done.append("bit-0 grouping substituted into corrected rule loses universal words") + return done + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--rescan", action="store_true", help="also walk the working tree (base-bound)") + parser.add_argument("--emit", action="store_true", help="print the observed result and exit 0") + args = parser.parse_args() + inventory = json.loads((PACKAGE / "INVENTORY.json").read_text(encoding="utf-8")) + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + try: + engine = load_faulty_engine(inventory) + observed = { + "calibration": calibration(), + "small_domain": small_domain(engine), + "inventory_roles": validate_inventory(inventory, ROOT), + "pinned_rows": len(inventory["pinned"]), + "controls": controls(inventory, engine), + "no_new_kappa": True, + } + if args.rescan: + observed["rescan"] = rescan(inventory, ROOT) + if args.emit: + print(json.dumps(observed, indent=1, sort_keys=True)) + return 0 + for key, value in observed.items(): + require(expected.get(key) == value, f"RESULT.json mismatch for {key}: {json.dumps(value)}") + if args.rescan: + require(not observed["rescan"]["unclassified"] and not observed["rescan"]["stale_prefixes"], + "rescan found unclassified consumers or stale prefixes") + except Fail as exc: + print("FAIL:", exc) + return 1 + sd = observed["small_domain"] + print(f"{MARKER} pinned={observed['pinned_rows']} false_prunes_n4L8={len(sd['engine_false_prunes'])}" + f"/{sd['simple_universal_words']} controls={len(observed['controls'])}" + + (f" rescan_files={observed['rescan']['files_scanned']}" if args.rescan else "") + + " no_new_kappa") + return 0 + + +if __name__ == "__main__": + sys.exit(main())