diff --git a/research/f7-l22-census-probe/README.md b/research/f7-l22-census-probe/README.md new file mode 100644 index 0000000000..3820303ebb --- /dev/null +++ b/research/f7-l22-census-probe/README.md @@ -0,0 +1,145 @@ +# Bounded length-22 probe of the corrected word census (resource budget, no f(7) claim) + +This package measures the resource budget for the one remaining controlled +step of the #2973 word-census correction: a corrected length-22 census at +seven labels. It is the named next step of the +[f7-l22-split-domain](https://github.com/CrocSwap/integer-mult-bounds/pull/3708) +handoff, whose recorded blocker is *"no node-count estimate or resource +budget; #2973's stop rule was explicitly no L22 census."* + +**What is established here, at its actual strength:** + +1. **Engine extension, validated.** The corrected census engine of + `research/f7-weight-parity-census-correction` (#2973, Nicholas Stone) is + pinned at blob hash with source `sha256 265ead91…`. A copy extended by + **exactly three header/gate lines** (`L <= 20` to `L <= 22`; nothing else) + is included as `engine/extended_census.c`. The extension is validated by + (a) the predecessor package's own `math/check_math.py`, (b) the + predecessor's brute-force cross-check `validation/check_corrected_c.py` + run against the extended engine (all small splits, all four budget + modes, cap and fail-closed input controls), and (c) **node-exact + reproduction of all six recorded L20/L18 receipts** of the pinned + package with the extended binary. +2. **Capped length-22 probes with three completed exclusions.** All nine + open splits of the #3708 domain — `(11,11), (11,10), (11,9), (10,10), + (11,8), (10,9), (11,7), (10,8), (9,9)` — are probed with both proved + necessary budgets enabled. Three splits completed with `complete=true` + and zero hits — **`(11,7)`, `(10,8)` and `(11,8)` are finite + exclusions**; the six others hit the 2e9-node cap and abort, recording + only **lower bounds** on their tree sizes. Per-split results, including + node counts and seconds, are in [RESULT.json](RESULT.json). **CI scope:** + the registered commands re-run the validation stages and replay each of + the three completed exclusions node-exactly, one command per split; the + six capped probes are locally measured and are reproduced only by the + opt-in `--probe-all-splits` command (about 1.4e10 nodes), not by CI. +3. **No f(7) claim.** The six loose-budget splits remain open, so nothing + here decides whether `f(7) = 22` or `24`. No supplier, tariff, kappa, + certificate, frozen input or selected-frontier change is made or + implied. `scripts/research_baseline.py` still reports + `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` with the pinned selected record. + +## Why the L<=22 gate change is sound + +The predecessor restricts compile-time `L` to `[2,20]`, described as keeping +"masks and all full-search counters within their exact types". At `N = 7, +L = 22`: coverage masks still use 7 of the 128 bits of `mask_t`; the largest +new counter values are `C(11,2)+C(11,2) = 110` (even budget bound), `11*11-64 += 57` (odd budget), per-label multiplicity `<= L-2(N-1) = 10`, and +`rem_even/rem_odd` table entries `< 22`. Every state variable is an exact +small integer or a fixed-width bitset at `L = 22`, so the gate is +conservative rather than necessary at 22. The behavioral controls above are +the real evidence: identical node-exact receipts at every recorded case. + +## How to reproduce + +From the repository root, with Python 3.12 and a C11 compiler: + +```sh +# Registered CI scope: validation stages, then one fresh node-exact replay +# per completed exclusion (the registered commands run these separately). +python3 -I -B research/f7-l22-census-probe/verify.py --skip-probe +python3 -I -B research/f7-l22-census-probe/verify.py --probe-split 11,7 +python3 -I -B research/f7-l22-census-probe/verify.py --probe-split 10,8 +python3 -I -B research/f7-l22-census-probe/verify.py --probe-split 11,8 + +# Default (no flags): validation stages plus all three exclusion replays. +python3 -I -B research/f7-l22-census-probe/verify.py + +# Opt-in, not run by CI: the full nine-split comparison against the +# committed RESULT.json receipt, including the six capped lower-bound +# probes (about 1.4e10 nodes; minutes on a many-core host). +python3 -I -B research/f7-l22-census-probe/verify.py --probe-all-splits +``` + +`verify.py` writes `LAST-RUN.json` in this package and prints +`PASS_F7_L22_CENSUS_PROBE`; the committed `RESULT.json` session receipt is +never rewritten. Probe cap default is 2,000,000,000 nodes per split; probes +run in parallel threads. All other generated files use temporary +directories. Aborted/capped probes are recorded with `complete=false` and +are never exclusions; the engine returns exit 2 for them. + +## Results summary + +Measured on this host (Apple arm64, CPython 3.12.15, Apple clang, 18 cores, +probes in parallel, cap 2,000,000,000 nodes per split). Node counts are +exact engine outputs; seconds are host timings and are not part of any +claim. + +| Split | Nodes | Outcome | Meaning | +|---|---:|---|---| +| `(11,7)` | 8,784,744 | complete, exit 0, 0 hits | **finite split exclusion** | +| `(10,8)` | 597,933,297 | complete, exit 0, 0 hits | **finite split exclusion** | +| `(11,8)` | 1,349,702,650 | complete, exit 0, 0 hits | **finite split exclusion** | +| `(9,9)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | +| `(10,9)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | +| `(10,10)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | +| `(11,9)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | +| `(11,10)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | +| `(11,11)` | 2,000,000,000 (cap) | aborted | tree has more than 2e9 nodes; open | + +For scale, the predecessor's recorded length-20 exclusions totalled about +9.2e8 nodes across all five splits; the three completed length-22 splits +alone reach 1.96e9 nodes, and each of the six open splits exceeds 2e9 +before its cap. A complete census needs the six open splits finished, so +the probe numbers are the concrete resource datum the handoff asked for. + +Certification scope, stated exactly: the three finite exclusions and the +validation stages above are re-run by the registered CI commands; the six +capped lower-bound probes are not part of CI replay and remain locally +measured, reproducible with the opt-in command in "How to reproduce". + +Combined with the imported 17-point set-level exclusions of #2773/#2870 +(splits `(10,7)`, `(11,6)`), any restored universal length-22 word must now +have its distinct-state split in `{(9,9), (10,9), (10,10), (11,9), +(11,10), (11,11)}`. The domain is six splits, not nine. No universal word +was found and no claim is made about `f(7)`: it remains 22 or 24. + +All six recorded predecessor receipts were reproduced node-exactly with +the extended binary (`receipt_replay` in RESULT.json); the brute-force +cross-check and the predecessor math check pass. `scripts/research_baseline.py` +reports `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` unchanged. + +## Credit + +Predecessor and sole mathematical source: **Nicholas Stone** +(#2973 corrected census engine, budgets, split theory) on the word model of +Aaron Wang (PR2542/PR2634) and Ross Richardson (PR943), with the length-22 +split domain derived by Nick Petalas (PR #3708). This package was produced +by Nick Petalas with AI assistance. Apache-2.0. + +## Open next questions + +1. **Is a complete nine-split L22 census affordable?** RESULT.json gives + per-split tree-size lower bounds from the capped probes. A feasibility + decision needs those numbers plus the loose-budget splits' completion + behavior at higher caps; it is a resource decision, not a new mechanism. +2. **Does a restored universal length-22 word exist?** This package + excludes the splits `(11,7)`, `(10,8)` and `(11,8)`; the domain is the + six splits `{(9,9), (10,9), (10,10), (11,9), (11,10), (11,11)}`. The + smallest trees there already exceed 2e9 nodes at each aborted split, so + the next probe level (8-16e9 nodes, or a cheaper prune) is a resource + decision, not this package's claim. +3. **Can the pair identity (`sum_x A_x B_x >= need`, MATH.md section 3) + become a third monotone engine prune?** It is proved necessary at + leaves but its partial quantity is not shown monotone; a non-monotone + prune would be unsound. See TASK.json open questions. diff --git a/research/f7-l22-census-probe/RESULT.json b/research/f7-l22-census-probe/RESULT.json new file mode 100644 index 0000000000..25307f9420 --- /dev/null +++ b/research/f7-l22-census-probe/RESULT.json @@ -0,0 +1,264 @@ +{ + "brute_crosscheck": { + "check_corrected_c_exit": 0 + }, + "integrity": { + "changed_lines": [ + 15, + 35, + 36 + ], + "extended_engine_sha256": "659bcdd10c6eb892e0a52438979c8f91e793a4dbf27e167c1ecabf4ee91c59e6", + "predecessor_engine_sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + "math_check": { + "check_math_exit": 0 + }, + "package": "f7-l22-census-probe", + "probe": { + "aborted_splits": [ + [ + 11, + 11 + ], + [ + 11, + 10 + ], + [ + 11, + 9 + ], + [ + 10, + 10 + ], + [ + 10, + 9 + ], + [ + 9, + 9 + ] + ], + "any_hits": false, + "cap_per_split": 2000000000, + "complete_zero_hit_splits": [ + [ + 11, + 8 + ], + [ + 11, + 7 + ], + [ + 10, + 8 + ] + ], + "probes": [ + { + "aborted": true, + "candidate_restored_leaves": 3, + "complete": false, + "even_budget": 47, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 57, + "process_exit": 2, + "seconds": 144.103896, + "split": [ + 11, + 11 + ] + }, + { + "aborted": true, + "candidate_restored_leaves": 0, + "complete": false, + "even_budget": 37, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 46, + "process_exit": 2, + "seconds": 154.840223, + "split": [ + 11, + 10 + ] + }, + { + "aborted": true, + "candidate_restored_leaves": 0, + "complete": false, + "even_budget": 28, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 35, + "process_exit": 2, + "seconds": 163.386531, + "split": [ + 11, + 9 + ] + }, + { + "aborted": true, + "candidate_restored_leaves": 0, + "complete": false, + "even_budget": 27, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 36, + "process_exit": 2, + "seconds": 163.711186, + "split": [ + 10, + 10 + ] + }, + { + "aborted": false, + "candidate_restored_leaves": 0, + "complete": true, + "even_budget": 20, + "finite_split_exclusion": true, + "hit_words": [], + "hits": 0, + "nodes": 1349702650, + "odd_budget": 24, + "process_exit": 0, + "seconds": 118.799134, + "split": [ + 11, + 8 + ] + }, + { + "aborted": true, + "candidate_restored_leaves": 0, + "complete": false, + "even_budget": 18, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 26, + "process_exit": 2, + "seconds": 170.384781, + "split": [ + 10, + 9 + ] + }, + { + "aborted": false, + "candidate_restored_leaves": 0, + "complete": true, + "even_budget": 13, + "finite_split_exclusion": true, + "hit_words": [], + "hits": 0, + "nodes": 8784744, + "odd_budget": 13, + "process_exit": 0, + "seconds": 0.832114, + "split": [ + 11, + 7 + ] + }, + { + "aborted": false, + "candidate_restored_leaves": 0, + "complete": true, + "even_budget": 10, + "finite_split_exclusion": true, + "hit_words": [], + "hits": 0, + "nodes": 597933297, + "odd_budget": 16, + "process_exit": 0, + "seconds": 52.247122, + "split": [ + 10, + 8 + ] + }, + { + "aborted": true, + "candidate_restored_leaves": 0, + "complete": false, + "even_budget": 9, + "finite_split_exclusion": false, + "hit_words": [], + "hits": 0, + "nodes": 2000000000, + "odd_budget": 17, + "process_exit": 2, + "seconds": 171.71321, + "split": [ + 9, + 9 + ] + } + ] + }, + "receipt_replay": { + "replayed_cases": [ + { + "candidate_restored_leaves": 0, + "case": "n7_l20_10_10", + "hits": 0, + "node_exact_match": true, + "nodes": 590371593 + }, + { + "candidate_restored_leaves": 0, + "case": "n7_l20_10_9", + "hits": 0, + "node_exact_match": true, + "nodes": 244301902 + }, + { + "candidate_restored_leaves": 0, + "case": "n7_l20_10_8", + "hits": 0, + "node_exact_match": true, + "nodes": 14450133 + }, + { + "candidate_restored_leaves": 0, + "case": "n7_l20_9_9", + "hits": 0, + "node_exact_match": true, + "nodes": 67643567 + }, + { + "candidate_restored_leaves": 0, + "case": "n7_l20_10_7", + "hits": 0, + "node_exact_match": true, + "nodes": 35241 + }, + { + "candidate_restored_leaves": 0, + "case": "n7_l18_9_9", + "hits": 0, + "node_exact_match": true, + "nodes": 951416 + } + ] + }, + "schema": 1 +} diff --git a/research/f7-l22-census-probe/SOURCES.json b/research/f7-l22-census-probe/SOURCES.json new file mode 100644 index 0000000000..a6f10cc400 --- /dev/null +++ b/research/f7-l22-census-probe/SOURCES.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/f7-weight-parity-census-correction/SOURCES.json", + "usage": "input", + "git_blob": "debaab5575799e8e6dcbd6a9e5921829b3b90dd1", + "sha256": "8d1aba232c278737def586f8d9b1794ec0619d266623da7196a624aeec7ff96d" + }, + { + "path": "research/f7-weight-parity-census-correction/TASK.json", + "usage": "input", + "git_blob": "0a7d2158d6c9ebbd18c75f15a50d4c66821152c9", + "sha256": "60d9a4cb105a17f3e0d30f2854ea9aa28746cb6d8afa70bc31f5da88f313af09" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "input", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "usage": "input", + "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/README.md", + "usage": "input", + "git_blob": "5c9267158d8990507849cfb8f35d4dd2b1d1c407", + "sha256": "c46e0f1b9d578918564da06ffc50e74a134c8d37a834a41d18cb50b3163ab334" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/SUMMARIES.json", + "usage": "input", + "git_blob": "b82513ed4f33cba22d1c9fca95cc1928ac9090b2", + "sha256": "e58bcef2ee6e03c889061c001623a6159dd3cfffd0a35acb6f3ab630002261c2" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_10.json", + "usage": "input", + "git_blob": "da8d29896e33640f90b8077f9a6fb9a44136f5e6", + "sha256": "e26c999c21b21a078241b2f7a350ab17c5efe7c0b78b836e97e243f9d1d21642" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_9.json", + "usage": "input", + "git_blob": "50b87a3852899f5474f086bcad6e56176829f5da", + "sha256": "0749686418137f7b8da76f1193f29f856b1add2340751902a5fb75456a6d7f5c" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_8.json", + "usage": "input", + "git_blob": "0df6438957932a3e27fda1f7d26c4445e203c844", + "sha256": "2b804534866b0b542e505ead8c5b46d35c139220582331a11231f52a03ef5ca7" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_9_9.json", + "usage": "input", + "git_blob": "3ccced64ea2b434ddd3d0e6ca7124de1a298176f", + "sha256": "fb6b00fded1a3ed94540361c315aae5c9d769d26d989aeddb28c3a1e99773cdd" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_7.json", + "usage": "input", + "git_blob": "48439aacedb107bf03fa9defa7acb8236c1ed531", + "sha256": "d1176caf822b1251e438caded4e32ae84b8eab3938ddc6caf9cf4511f2bd8962" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/results/n7_l18_9_9.json", + "usage": "input", + "git_blob": "3458233a09a687fb96b414187aeb0381cdd10d43", + "sha256": "9ea887e0e0df4a994498ea997db6d98de979d0ff5ff92ac174f0a43cd7a3e03c" + }, + { + "path": "research/f7-weight-parity-census-correction/math/check_math.py", + "usage": "input", + "git_blob": "2ac1478a2115a82ad50bb7a56f4d33177ff2bea1", + "sha256": "a6b011f4c06017200bf855c122c510c23d08f4b74b269f27a0e0f92aae99d220" + }, + { + "path": "research/f7-weight-parity-census-correction/validation/check_corrected_c.py", + "usage": "input", + "git_blob": "7ca76aeff908a0e2070d96bfe841cc4ce94464b0", + "sha256": "b6f1159a98fb2d9d6053d3e7c73cd10f9ca15f5b9c3f6e956e171922b0927684" + }, + { + "path": "research/f7-weight-parity-census-correction/validation/brute_validation.py", + "usage": "input", + "git_blob": "4c11e64695229bd35d3a7b4f458dbf2059d3db59", + "sha256": "3a2dedc73d1674b13f6017cb04913e870936abcbd9c9c3ec57bd7c8280b6dcff" + } + ] +} diff --git a/research/f7-l22-census-probe/TASK.json b/research/f7-l22-census-probe/TASK.json new file mode 100644 index 0000000000..404a5d90ce --- /dev/null +++ b/research/f7-l22-census-probe/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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", + "scope_change_reason": "The prune-correction audit (#2973) is merged and its small-domain counterexample is already independently corroborated by #3005, #3096 and PR #3699. PR #3708 then derived the exact length-22 split domain and named as its blocker 'no node-count estimate or resource budget' for the corrected engine at length 22. This package refines the card to that named obligation: validate the corrected engine against its pinned sources and recorded receipts, then measure the L22 resource budget with capped probes, completing any split whose enumeration finishes under the cap. The active decision it can change is whether a complete corrected L22 census (and hence deciding f(7) = 22) is feasible and at what cost; no larger census is launched beyond the capped probes in this session.", + "actual_scope": "Single-gate extension (L<=20 to L<=22) of the pinned corrected census engine of #2973, validated node-exactly against all six of its recorded receipts and its brute-force small-domain cross-check, then capped L22 probes at the nine open splits of the PR #3708 domain. Complete zero-hit probes are finite split exclusions; aborted probes are measured tree-size lower bounds only.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census. This package supplies the resource-budget measurement that the census-pruning-audit card and the PR #3708 handoff name as the blocker for deciding f(7) = 22 within PR943's prefix-walk model.", + "budget_minutes": 60, + "stop_rule": "Stop after the nine capped probes finish (each completing or hitting the cap), or when the session budget is exhausted, whichever is first. A capped probe never becomes an exclusion; a complete zero-hit probe is recorded as a finite split exclusion; any hit word is reported verbatim and immediately.", + "outcome": "completed", + "evidence": "RESULT.json: integrity diff (3 gate lines only), predecessor math check exit 0, brute cross-check exit 0 over all small splits and budget modes, node-exact replay of all six recorded receipts, and nine capped L22 probes. Finite split exclusions completed at (11,7), (10,8), (11,8) with zero hits; the six remaining splits aborted at the 2e9-node cap and are recorded as tree-size lower bounds only. No hits; no f(7) claim.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a restored universal length-22 seven-label word exist (f(7) = 22 versus 24)?", + "why_it_matters": "#2973 bounds 22 <= f(7) <= 24; deciding length 22 is the next word-level frontier step inside PR943's model.", + "first_step": "Run the extended engine at the tightest splits first; this package's RESULT.json records the measured node budgets per split.", + "blocked_by": "A complete nine-split census needs a resource decision beyond one session; the measured budgets in RESULT.json are the input to that decision." + }, + { + "question": "Can the pair identity (sum_x A_x B_x >= need) be added as a third monotone prune in the engine to cut the (11,11) tree?", + "why_it_matters": "It is proved necessary in MATH.md section 3 but not implemented; it prunes branches the two budgets alone leave.", + "first_step": "Prove the partial quantity sum_x A_x B_x is dominated by its final necessary value under monotone growth, or find the monotone variant, before touching the engine.", + "blocked_by": "Monotonicity of the partial bound is not established; a non-monotone prune is unsound." + } + ] +} diff --git a/research/f7-l22-census-probe/VERIFY.json b/research/f7-l22-census-probe/VERIFY.json new file mode 100644 index 0000000000..31af5cc9bd --- /dev/null +++ b/research/f7-l22-census-probe/VERIFY.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-weight-parity-census-correction/SOURCES.json", + "research/f7-weight-parity-census-correction/TASK.json", + "research/f7-weight-parity-census-correction/MATH.md", + "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "research/f7-weight-parity-census-correction/engine/README.md", + "research/f7-weight-parity-census-correction/engine/SUMMARIES.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_10.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_9.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_8.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l20_9_9.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l20_10_7.json", + "research/f7-weight-parity-census-correction/engine/results/n7_l18_9_9.json", + "research/f7-weight-parity-census-correction/math/check_math.py", + "research/f7-weight-parity-census-correction/validation/check_corrected_c.py", + "research/f7-weight-parity-census-correction/validation/brute_validation.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--skip-probe" + ], + "timeout_seconds": 420, + "checks": "Engine-integrity diff against the pinned corrected_census.c (only the documented L<=22 gate lines may differ), the predecessor package's own math check, the predecessor's brute-force cross-check of the extended engine over all small splits and all four budget modes with cap and fail-closed controls, and node-exact replay of all six recorded L20/L18 receipts of the pinned package with the extended binary." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--probe-split", + "11,7" + ], + "timeout_seconds": 60, + "checks": "Fresh length-22 census replay of the completed exclusion split (11,7) against the committed RESULT.json receipt: must exit 0 with complete=true, zero hits, and the identical node count (8,784,744 nodes). A capped abort or any node drift fails." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--probe-split", + "10,8" + ], + "timeout_seconds": 240, + "checks": "Fresh length-22 census replay of the completed exclusion split (10,8) against the committed RESULT.json receipt: must exit 0 with complete=true, zero hits, and the identical node count (597,933,297 nodes). A capped abort or any node drift fails." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--probe-split", + "11,8" + ], + "timeout_seconds": 480, + "checks": "Fresh length-22 census replay of the completed exclusion split (11,8) against the committed RESULT.json receipt: must exit 0 with complete=true, zero hits, and the identical node count (1,349,702,650 nodes). A capped abort or any node drift fails." + } + ], + "notes": "C11 compiler with unsigned __int128 required (clang or GCC). No Python dependencies. The three completed split exclusions (11,7), (10,8) and (11,8) are replayable by the registered commands; each runs one split under its own timeout. The six capped lower-bound probes (2e9-node cap each, the remaining splits) are NOT re-run by CI: reproduce them with the documented opt-in command `{python} -I -B {package}/verify.py --probe-all-splits` (about 1.4e10 nodes; long). `--probe-cap` lowers the cap for the opt-in measurement (must stay at or below the recorded cap). RESULT.json is the committed receipt and is never rewritten; each run writes LAST-RUN.json. Timing fields are excluded from all equality checks." +} diff --git a/research/f7-l22-census-probe/engine/extended_census.c b/research/f7-l22-census-probe/engine/extended_census.c new file mode 100644 index 0000000000..f7e6f1b929 --- /dev/null +++ b/research/f7-l22-census-probe/engine/extended_census.c @@ -0,0 +1,219 @@ +/* Corrected finite canonical restored-word census. + * Derived from Nicholas Stone's audit-f7/f7_census.c and session2/agent-a/ + * f7_census_revisit.c; preserves their restricted-growth word scope. + * New implementation/review with substantial OpenAI Codex assistance. + * + * E and O ALWAYS mean Hamming-weight parity, never coordinate bit 0. + * New DISTINCT states add pair representations; visits add none. + * Even excess is (C(|E|,2)-|supp EE|)+(C(|O|,2)-|supp OO|). + * Odd excess is |E||O|-|supp EO|. These are monotone, so their necessary + * final bounds are sound at intermediate prefixes. Default enables both. + * + * candidate_restored_leaves counts only leaves surviving enabled budgets. + * all_restored_leaves is exact only with --no-budgets and complete=true. + * A capped run returns 2, complete=false; bad input or output I/O returns 1. + * N in [1,7], positive even L<=22. Extended from the corrected census engine; + */ +#ifndef _POSIX_C_SOURCE +#define _POSIX_C_SOURCE 200809L +#endif +#include +#include +#include +#include +#include +#include +#include +#include + +#ifndef N +#define N 7 +#endif +#ifndef L +#define L 20 +#endif +#if N < 1 || N > 7 || L < 2 || L > 22 || L % 2 +#error "Requires 1 <= N <= 7 and positive even 2 <= L <= 22" +#endif + +typedef unsigned __int128 mask_t; +typedef struct { char key[L+1]; int length; uint64_t cap; } Shard; +typedef struct { + uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes; + int aborted; + double seconds; +} Result; +static int S,T, even_on=1,odd_on=1,even_budget,odd_budget; +static int word[L], counts[N], E[L+1],O[L+1],es=1,os=0; +static int q,used,odd_counts,even_excess,odd_excess; +static mask_t seen=1, ee,oo,eo; +static Result run; +static Shard *current; +static FILE *hitout; +static int io_error; +static int rem_even[L],rem_odd[L]; +static inline int pop(mask_t x) { + return __builtin_popcountll((uint64_t)x)+__builtin_popcountll((uint64_t)(x>>64)); +} +static inline int parity(int x) { return __builtin_popcount((unsigned)x)&1; } +static inline mask_t bit(int x) { return (mask_t)1 << x; } +static void rec(int i) { + if (run.aborted || io_error) return; + if (current->cap && run.nodes >= current->cap) { run.aborted=1; return; } + run.nodes++; + if (i==L) { + if (q || used!=N || odd_counts || es!=S || os!=T) return; + run.candidate_leaves++; + if (pop(ee|oo|eo|1)==(1<L-i) return; + int limit=used=L-2*(N-1)) continue; + if (ilength && j!=current->key[i]-'0') continue; + int nq=q^(1<S || nt>T || ns+rem_even[i]even_budget) { run.even_prunes++; continue; } + if (odd_on && odd_excess+dc_odd>odd_budget) { run.odd_prunes++; continue; } + } + mask_t old_seen=seen,old_ee=ee,old_oo=oo,old_eo=eo; + int old_q=q,old_used=used,old_odd=odd_counts; + word[i]=j; + counts[j]++; + odd_counts+=(counts[j]&1)?1:-1; + q=nq; + if (j==old_used) used++; + if (fresh) { + seen|=bit(nq); + if (p) { O[os++]=nq; oo|=add_same; } + else { E[es++]=nq; ee|=add_same; } + eo|=add_cross; + even_excess+=dc_even; odd_excess+=dc_odd; + } + rec(i+1); + if (fresh) { + if (p) os--; else es--; + even_excess-=dc_even; odd_excess-=dc_odd; + } + seen=old_seen; ee=old_ee; oo=old_oo; eo=old_eo; + counts[j]--; q=old_q; used=old_used; odd_counts=old_odd; + } +} +static int parse_uint(const char *s,uint64_t *out) { + if (!*s || *s<'0' || *s>'9') return 0; + errno=0; char *end; unsigned long long n=strtoull(s,&end,10); + if (errno || *end) return 0; + *out=(uint64_t)n; return 1; +} +static int parse_split(const char *s) { + const char *comma=strchr(s,','); + if (!comma || comma==s || strchr(comma+1,',') || comma-s>3) return 0; + char left[4]; memcpy(left,s,(size_t)(comma-s)); left[comma-s]=0; + uint64_t a,b; + if (!parse_uint(left,&a)||!parse_uint(comma+1,&b)||a<1||b<1||a>L/2||b>L/2||a>(1u<<(N-1))||b>(1u<<(N-1))) return 0; + S=(int)a; T=(int)b; return 1; +} +static int parse_shard(const char *s,Shard *dst,uint64_t cap) { + const char *colon=strchr(s,':'); + size_t len=colon?(size_t)(colon-s):strlen(s); + if (len==1 && s[0]=='-') len=0; + if (len>L || (colon && !parse_uint(colon+1,&cap))) return 0; + int introduced=0; + for (size_t k=0;k=N || label>introduced) return 0; + if (label==introduced) introduced++; + dst->key[k]=s[k]; + } + dst->key[len]=0; dst->length=(int)len; dst->cap=cap; + return 1; +} +static void write_result(FILE *f,const char *prefix,Result *r,int comma) { + fprintf(f," {\"prefix\":\"%s\",\"nodes\":%" PRIu64 ",\"candidate_restored_leaves\":%" PRIu64 ",\"all_restored_leaves\":",prefix,r->nodes,r->candidate_leaves); + if (!even_on&&!odd_on&&!r->aborted) fprintf(f,"%" PRIu64,r->candidate_leaves); else fputs("null",f); + fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":""); +} +int main(int argc,char **argv) { + Shard shards[128]; Result results[128]; int nshards=0; + const char *hits_path=NULL,*json_path=NULL; uint64_t cap=0; + if (argc<2||!parse_split(argv[1])) { fprintf(stderr,"usage: %s s,t --hits PATH [--json PATH] [--cap N] [--no-budgets|--no-even-budget|--no-odd-budget] [PREFIX[:CAP]...]\n",argv[0]); return 1; } + for (int a=2;a=argc) { fprintf(stderr,"missing option argument\n"); return 1; } + if (!strcmp(arg,"--hits")) { if(hits_path) return 1; hits_path=argv[a]; } + else if (!strcmp(arg,"--json")) { if(json_path) return 1; json_path=argv[a]; } + else if (!parse_uint(argv[a],&cap)) { fprintf(stderr,"invalid cap\n"); return 1; } + continue; + } + if (nshards==128 || !parse_shard(arg,&shards[nshards],0)) { fprintf(stderr,"invalid shard: %s\n",arg); return 1; } + nshards++; + } + if (!hits_path || (json_path&&!strcmp(hits_path,json_path))) { fprintf(stderr,"distinct explicit --hits PATH required\n"); return 1; } + if (!nshards) { memset(&shards[0],0,sizeof shards[0]); nshards=1; } + for(int a=0;alength?current->key:"-",run.nodes,run.candidate_leaves,run.hits,(!run.aborted&&!io_error)?"true":"false",run.seconds); fflush(stdout); + if (run.aborted||io_error) break; + } + printf("TOTAL N=%d L=%d split=%d,%d nodes=%" PRIu64 " candidate_restored_leaves=%" PRIu64 " hits=%" PRIu64 " complete=%s seconds=%.3f\n",N,L,S,T,total.nodes,total.candidate_leaves,total.hits,(!total.aborted&&!io_error)?"true":"false",total.seconds); + if(jsonout) { + fprintf(jsonout,"{\n \"schema\":1,\"n\":%d,\"length\":%d,\"split\":[%d,%d],\"groups\":\"hamming_weight_parity\",\"even_budget\":%d,\"odd_budget\":%d,\"even_budget_enabled\":%s,\"odd_budget_enabled\":%s,\n \"complete\":%s,\"aborted\":%s,\"requested_shards\":%d,\"completed_or_partial_shards\":%d,\n \"shards\":[\n",N,L,S,T,even_budget,odd_budget,even_on?"true":"false",odd_on?"true":"false",(!total.aborted&&!io_error)?"true":"false",total.aborted?"true":"false",nshards,done); + for(int a=0;a 22" in changed[1][2] and "L <= 22" in changed[2][2], + "lines 35-36 must change only the L<=20 gate to L<=22") + return {"predecessor_engine_sha256": sha256(pred_source), + "extended_engine_sha256": sha256(ext_source), + "changed_lines": sorted(allowed)} + + +def stage_math_check(): + proc = subprocess.run( + [sys.executable, "-B", str(PREDECESSOR / "math" / "check_math.py")], + capture_output=True, text=True) + require(proc.returncode == 0, f"predecessor math check failed:\n{proc.stdout[-2000:]}") + return {"check_math_exit": 0} + + +def stage_brute_crosscheck(work): + proc = subprocess.run( + [sys.executable, "-B", + str(PREDECESSOR / "validation" / "check_corrected_c.py"), + "--engine-source", str(HERE / "engine" / "extended_census.c"), + "--output-dir", str(work / "brute")], + capture_output=True, text=True) + require(proc.returncode == 0, + f"extended-engine brute cross-check failed:\n{proc.stdout[-2000:]}\n{proc.stderr[-2000:]}") + return {"check_corrected_c_exit": 0} + + +def stage_replay_receipts(work): + source = HERE / "engine" / "extended_census.c" + per_case = [] + for n, l, case in RECORDED_CASES: + recorded = json.loads( + (PREDECESSOR / "engine" / "results" / f"{case}.json").read_text()) + rec = recorded["shards"][0] + binary = work / f"census_n{n}_l{l}_ext" + compile_engine(source, n, l, binary) + proc, data, words = run_case(binary, (recorded["split"][0], recorded["split"][1]), + work / f"replay_{case}") + require(proc.returncode == 0 and data["complete"] is True, + f"{case}: replay did not complete (exit {proc.returncode})") + total = data["total"][0] + fields = {} + for key in ("nodes", "candidate_restored_leaves", "hits", + "even_budget", "odd_budget"): + if key in ("even_budget", "odd_budget"): + fields[key] = (data[key], recorded[key]) + else: + fields[key] = (total[key], rec[key]) + for key, (got, want) in fields.items(): + require(got == want, + f"{case}: {key} replayed {got} != recorded {want}") + require(total["hits"] == len(words), f"{case}: hit-file mismatch") + per_case.append({"case": case, "nodes": total["nodes"], + "candidate_restored_leaves": + total["candidate_restored_leaves"], + "hits": total["hits"], "node_exact_match": True}) + return {"replayed_cases": per_case} + + +def probe_one(split, cap, work): + s, t = split + binary = work / f"census_n7_l22" + directory = work / f"probe_{s}_{t}" + directory.mkdir(parents=True, exist_ok=True) + proc, data, words = run_case(binary, split, directory, cap=cap) + total = data["total"][0] + return { + "split": [s, t], + "even_budget": data["even_budget"], + "odd_budget": data["odd_budget"], + "complete": data["complete"], + "aborted": data["aborted"], + "process_exit": proc.returncode, + "nodes": total["nodes"], + "candidate_restored_leaves": total["candidate_restored_leaves"], + "hits": total["hits"], + "hit_words": words, + "seconds": total["seconds"], + "finite_split_exclusion": bool(proc.returncode == 0 + and data["complete"] is True + and total["hits"] == 0), + } + + +def stage_probe(splits, cap, workers): + """Fresh capped probes, compared against the committed RESULT.json. + + The committed receipt is session evidence and is never rewritten. A + fresh run must agree with it: a split recorded complete must complete + again with the identical node count and zero hits (node counts are + cap-independent for completed runs); a split recorded aborted at the + recorded cap must abort again at the fresh cap with zero hits. The + fresh cap must not exceed the recorded cap. Determinism of the + traversal order is what makes exact node equality possible; timing + fields are excluded everywhere. + + The registered CI commands pass one exclusion split each. The six + capped lower-bound splits are replayed only by the explicit opt-in + `--probe-all-splits`, never by a registered command. + """ + committed_path = HERE / "RESULT.json" + require(committed_path.exists(), + "RESULT.json (committed session receipt) is missing; it is the " + "comparison target and must not be deleted") + committed = json.loads(committed_path.read_text()) + recorded_cap = committed["probe"]["cap_per_split"] + require(cap <= recorded_cap, + f"fresh cap {cap} exceeds recorded cap {recorded_cap}") + recorded = {tuple(r["split"]): r for r in committed["probe"]["probes"]} + require(set(recorded) == set(OPEN_SPLITS), "committed splits changed") + for split in splits: + require(tuple(split) in recorded, + f"split {split} is not in the committed RESULT.json receipt") + + work = Path(tempfile.mkdtemp(prefix="l22probe-")) + try: + binary = work / "census_n7_l22" + compile_engine(HERE / "engine" / "extended_census.c", 7, 22, binary) + with concurrent.futures.ThreadPoolExecutor(max_workers=workers) as pool: + futures = {split: pool.submit(probe_one, split, cap, work) + for split in splits} + rows = [futures[split].result() for split in splits] + finally: + shutil.rmtree(work, ignore_errors=True) + for row in rows: + rec = recorded[tuple(row["split"])] + require(row["hits"] == 0 and rec["hits"] == 0, + f"split {row['split']}: unexpected hit") + if rec["finite_split_exclusion"]: + require(row["finite_split_exclusion"], + f"split {row['split']}: recorded complete but fresh run " + f"did not complete (nodes {row['nodes']})") + require(row["nodes"] == rec["nodes"], + f"split {row['split']}: node drift {row['nodes']} vs " + f"recorded {rec['nodes']}") + else: + require(row["nodes"] == cap, + f"split {row['split']}: aborted run stopped at " + f"{row['nodes']} != cap {cap}") + require(row["nodes"] <= rec["nodes"], + f"split {row['split']}: fresh nodes exceed recorded") + complete = [r for r in rows if r["finite_split_exclusion"]] + aborted = [r for r in rows if not r["finite_split_exclusion"]] + return {"cap_per_split": cap, "recorded_cap": recorded_cap, + "compared_against": "committed RESULT.json", + "splits": rows, + "complete_zero_hit_splits": [r["split"] for r in complete], + "aborted_splits": [r["split"] for r in aborted], + "any_hits": any(r["hits"] for r in rows)} + + +def parse_probe_split(parser, item): + parts = item.split(",") + if len(parts) != 2 or not all(p.strip().isdigit() for p in parts): + parser.error(f"--probe-split expects S,T as integers; got {item!r}") + split = (int(parts[0]), int(parts[1])) + if split not in OPEN_SPLITS: + parser.error(f"--probe-split {item}: not one of the nine open " + "length-22 splits") + return split + + +def main(): + parser = argparse.ArgumentParser( + description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("--probe-cap", type=int, default=2_000_000_000, + help="node cap per length-22 probe (0 = unlimited); " + "must not exceed the recorded cap in RESULT.json") + parser.add_argument("--workers", type=int, default=9) + mode = parser.add_mutually_exclusive_group() + mode.add_argument("--skip-probe", action="store_true", + help="run only integrity, math and validation stages") + mode.add_argument("--probe-all-splits", action="store_true", + help="opt-in full nine-split replay of the committed " + "RESULT.json receipt, including the six capped " + "lower-bound probes (about 1.4e10 nodes; not run " + "by CI)") + mode.add_argument("--probe-split", action="append", metavar="S,T", + help="replay only the named split(s); repeatable; the " + "registered CI commands replay one completed " + "exclusion per invocation") + args = parser.parse_args() + + splits = None + if args.probe_split: + splits = [] + for item in args.probe_split: + split = parse_probe_split(parser, item) + if split not in splits: + splits.append(split) + probe_only = bool(splits) or args.probe_all_splits + + result = {"schema": 1, "package": "f7-l22-census-probe"} + with tempfile.TemporaryDirectory(prefix="l22probestage-") as tmp: + work = Path(tmp) + result["integrity"] = stage_integrity() + if not probe_only: + result["math_check"] = stage_math_check() + result["brute_crosscheck"] = stage_brute_crosscheck(work) + result["receipt_replay"] = stage_replay_receipts(work) + if not args.skip_probe: + probe_splits = (OPEN_SPLITS if args.probe_all_splits + else (splits or EXCLUSION_SPLITS)) + result["probe"] = stage_probe(probe_splits, args.probe_cap, + args.workers) + + report = HERE / "LAST-RUN.json" + report.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + if "probe" in result: + for row in result["probe"]["splits"]: + print(f" probe {row['split']}: complete={row['complete']} " + f"nodes={row['nodes']:,} hits={row['hits']} " + f"finite_split_exclusion={row['finite_split_exclusion']}") + p = result["probe"] + print("complete zero-hit splits:", p["complete_zero_hit_splits"]) + print("aborted splits:", p["aborted_splits"]) + print("any hits:", p["any_hits"]) + if "receipt_replay" in result: + for row in result["receipt_replay"]["replayed_cases"]: + print(f" replay {row['case']}: nodes={row['nodes']:,} " + f"node_exact_match={row['node_exact_match']}") + print("PASS_F7_L22_CENSUS_PROBE") + if "probe" in result and result["probe"]["any_hits"]: + print("NOTE: a probe reported hits; inspect hit_words in the fresh " + "run before relying on any exclusion claim.") + + +if __name__ == "__main__": + main()