From 0f06b7e03d09865799f567ce2cbbc8863851da8c Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:20:15 -0700 Subject: [PATCH 1/3] Bind the faulty PR2542 engine bytes to the 01021323 false prune Scaffold research/census-prune-source-impact, recompute the bit-0 versus weight-parity budgets of 01021323, and compare the authenticated faulty engine with an independent oracle on the complete n=4, L=8 simple domain (6 of 22 universal words falsely pruned; weight-parity rule prunes none). --- .../census-prune-source-impact/INVENTORY.json | 387 ++++++++++++++++++ research/census-prune-source-impact/README.md | 35 ++ .../census-prune-source-impact/RESULT.json | 92 +++++ .../census-prune-source-impact/SOURCES.json | 174 ++++++++ research/census-prune-source-impact/TASK.json | 66 +++ .../census-prune-source-impact/VERIFY.json | 45 ++ research/census-prune-source-impact/verify.py | 375 +++++++++++++++++ 7 files changed, 1174 insertions(+) create mode 100644 research/census-prune-source-impact/INVENTORY.json create mode 100644 research/census-prune-source-impact/README.md create mode 100644 research/census-prune-source-impact/RESULT.json create mode 100644 research/census-prune-source-impact/SOURCES.json create mode 100644 research/census-prune-source-impact/TASK.json create mode 100644 research/census-prune-source-impact/VERIFY.json create mode 100644 research/census-prune-source-impact/verify.py 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..b21da2923a --- /dev/null +++ b/research/census-prune-source-impact/README.md @@ -0,0 +1,35 @@ +# census-prune-source-impact + +**Draft; no new bound claimed.** + +## Scope and evidence + +Original card: `census-pruning-audit`. Complete [TASK.json](TASK.json), including any scope +change and its connection to the bottleneck. Explain the result and limitations here. +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance, so later priority +updates do not invalidate this package. Explicit --source files are live inputs +and must match their pins. Full Git history is needed to resolve provenance. + +## Reproduce + +After completing the verifier and marking VERIFY.json ready, from repo root: + +```sh +python3 scripts/research_package.py --package research/census-prune-source-impact --check-only +python3.12 scripts/research_package.py --package research/census-prune-source-impact +``` + +Declare all external inputs and pinned dependencies in VERIFY.json. The generic +hook is bounded; native/Lean or long replays need an explicit dedicated workflow. + +## Open next questions + +Complete the structured `open_questions` list in TASK.json and explain it here: +the question, why it matters, a feasible first step and any blocker. If no next +question is justified, say so rather than inventing one. + +## Credit + +Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. 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..4bff499686 --- /dev/null +++ b/research/census-prune-source-impact/TASK.json @@ -0,0 +1,66 @@ +{ + "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": "unchanged", + "actual_scope": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "scope_change_reason": null, + "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "budget_minutes": 90, + "stop_rule": "TODO", + "outcome": "in-progress", + "evidence": "TODO", + "author": "JoyboyBrian", + "ai_assistance": "TODO: disclose tools used", + "open_questions": [ + { + "question": "TODO", + "why_it_matters": "TODO", + "first_step": "TODO", + "blocked_by": "TODO" + } + ] +} diff --git a/research/census-prune-source-impact/VERIFY.json b/research/census-prune-source-impact/VERIFY.json new file mode 100644 index 0000000000..d034c18f4f --- /dev/null +++ b/research/census-prune-source-impact/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "draft", + "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": "TODO: identity, positive fixture and failure controls" + } + ] +} 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()) From 319e59f12a90e2626e95fc83afdb3475eb053738 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:20:41 -0700 Subject: [PATCH 2/3] Register the source-impact verifier with -O control --- research/census-prune-source-impact/VERIFY.json | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/research/census-prune-source-impact/VERIFY.json b/research/census-prune-source-impact/VERIFY.json index d034c18f4f..bb4c88f8de 100644 --- a/research/census-prune-source-impact/VERIFY.json +++ b/research/census-prune-source-impact/VERIFY.json @@ -1,6 +1,6 @@ { "schema_version": 1, - "status": "draft", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [ @@ -39,7 +39,17 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "TODO: identity, positive fixture and failure controls" + "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" } ] } From e15c50039b2ed5ef581c1311bf501a5976be4e1a Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:23:27 -0700 Subject: [PATCH 3/3] Document the whole-tree classification, revalidation list and open questions README states the disproved rule versus untouched final bounds, the 21-prefix classification of every trigger file at base cef4b52, which exclusions need replacement evidence (three, all supplied), and which need reading notes only. TASK.json records the refined scope, stop rule and structured next questions. --- research/census-prune-source-impact/README.md | 177 ++++++++++++++++-- research/census-prune-source-impact/TASK.json | 37 ++-- 2 files changed, 184 insertions(+), 30 deletions(-) diff --git a/research/census-prune-source-impact/README.md b/research/census-prune-source-impact/README.md index b21da2923a..e036e5381d 100644 --- a/research/census-prune-source-impact/README.md +++ b/research/census-prune-source-impact/README.md @@ -1,35 +1,176 @@ -# census-prune-source-impact +# Whole-tree source impact of the bit-0 word-census prune -**Draft; no new bound claimed.** +**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.** -## Scope and evidence +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. -Original card: `census-pruning-audit`. Complete [TASK.json](TASK.json), including any scope -change and its connection to the bottleneck. Explain the result and limitations here. -Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). -The selected record and catalogue are historical provenance, so later priority -updates do not invalidate this package. Explicit --source files are live inputs -and must match their pins. Full Git history is needed to resolve provenance. +**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 -After completing the verifier and marking VERIFY.json ready, from repo root: +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 scripts/research_package.py --package research/census-prune-source-impact +python3.12 -B scripts/research_package.py --package research/census-prune-source-impact ``` -Declare all external inputs and pinned dependencies in VERIFY.json. The generic -hook is bounded; native/Lean or long replays need an explicit dedicated workflow. +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 -Complete the structured `open_questions` list in TASK.json and explain it here: -the question, why it matters, a feasible first step and any blocker. If no next -question is justified, say so rather than inventing one. +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 -Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. -New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. +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/TASK.json b/research/census-prune-source-impact/TASK.json index 4bff499686..6d83508b41 100644 --- a/research/census-prune-source-impact/TASK.json +++ b/research/census-prune-source-impact/TASK.json @@ -45,22 +45,35 @@ "census pruning" ] }, - "scope_status": "unchanged", - "actual_scope": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", - "scope_change_reason": null, - "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "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": "TODO", - "outcome": "in-progress", - "evidence": "TODO", + "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": "TODO: disclose tools used", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", "open_questions": [ { - "question": "TODO", - "why_it_matters": "TODO", - "first_step": "TODO", - "blocked_by": "TODO" + "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." } ] }