From bfc93a8ba6a1a097736181e33ef74cb5690b4308 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 20:06:35 +0100 Subject: [PATCH 1/2] research: measure the corrected L22 census budget; exclude splits (11,7), (10,8), (11,8) Extends the #2973 corrected word-census engine to length 22 by changing only its compile-time gate (three header/gate lines; all counters stay within their exact types). Validates the extension against the pinned predecessor: its math check, its brute-force small-domain cross-check in all four budget modes, and node-exact reproduction of all six recorded L20/L18 receipts (590371593 / 244301902 / 14450133 / 67643567 / 35241 / 951416 nodes). Runs capped censuses at the nine open length-22 splits of the PR #3708 split domain with both proved necessary budgets. Three splits complete with complete=true and zero hits - finite exclusions of (11,7) at 8,784,744 nodes, (10,8) at 597,933,297 and (11,8) at 1,349,702,650. The six loose-budget splits abort at the 2e9-node cap and are recorded as tree-size lower bounds only. With the imported #2773/#2870 exclusions, the length-22 domain narrows from nine splits to six. No hits anywhere; f(7) in {22,24} is untouched; no kappa, supplier or frontier change. Supplies the node-budget measurement named as the blocker of the #3708 handoff (open question 1). Fresh CI replays compare against the committed RESULT.json receipt; node equality is deterministic, timing excluded. --- research/f7-l22-census-probe/README.md | 125 ++++++++ research/f7-l22-census-probe/RESULT.json | 264 ++++++++++++++++ research/f7-l22-census-probe/SOURCES.json | 108 +++++++ research/f7-l22-census-probe/TASK.json | 72 +++++ research/f7-l22-census-probe/VERIFY.json | 48 +++ .../engine/extended_census.c | 219 ++++++++++++++ research/f7-l22-census-probe/verify.py | 284 ++++++++++++++++++ 7 files changed, 1120 insertions(+) create mode 100644 research/f7-l22-census-probe/README.md create mode 100644 research/f7-l22-census-probe/RESULT.json create mode 100644 research/f7-l22-census-probe/SOURCES.json create mode 100644 research/f7-l22-census-probe/TASK.json create mode 100644 research/f7-l22-census-probe/VERIFY.json create mode 100644 research/f7-l22-census-probe/engine/extended_census.c create mode 100644 research/f7-l22-census-probe/verify.py diff --git a/research/f7-l22-census-probe/README.md b/research/f7-l22-census-probe/README.md new file mode 100644 index 0000000000..5fb4becd29 --- /dev/null +++ b/research/f7-l22-census-probe/README.md @@ -0,0 +1,125 @@ +# 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). +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 +python3 -I -B research/f7-l22-census-probe/verify.py # full: validation + probes +python3 -I -B research/f7-l22-census-probe/verify.py --skip-probe # validation stages only +python3 -I -B research/f7-l22-census-probe/verify.py --probe-cap 500000000 # smaller probes +``` + +`verify.py` writes `RESULT.json` in this package and prints +`PASS_F7_L22_CENSUS_PROBE`. 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. + +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..a74a543c57 --- /dev/null +++ b/research/f7-l22-census-probe/VERIFY.json @@ -0,0 +1,48 @@ +{ + "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": 600, + "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", + "--skip-replay" + ], + "timeout_seconds": 600, + "checks": "Fresh capped length-22 probes at the nine open splits, compared against the committed RESULT.json session receipt: each recorded-complete split must complete again with the identical node count and zero hits; each recorded-aborted split must abort at the cap with zero hits; the fresh cap must not exceed the recorded cap. A probe counts as a finite split exclusion only when its process exits 0 with complete=true and zero hits; capped runs are lower bounds on the tree size and never exclusions." + } + ], + "notes": "C11 compiler with unsigned __int128 required (clang or GCC). No Python dependencies. Default probe cap 2,000,000,000 nodes per split, probes in parallel threads; --probe-cap lowers it (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(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. + """ + 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") + + 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 OPEN_SPLITS} + rows = [futures[split].result() for split in OPEN_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", + "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 main(): + parser = argparse.ArgumentParser() + 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) + parser.add_argument("--skip-probe", action="store_true", + help="run only integrity, math and validation stages") + parser.add_argument("--skip-replay", action="store_true", + help="probe stage only; skips the slow receipt replay") + args = parser.parse_args() + + result = {"schema": 1, "package": "f7-l22-census-probe"} + with tempfile.TemporaryDirectory(prefix="l22probestage-") as tmp: + work = Path(tmp) + result["integrity"] = stage_integrity() + if not args.skip_replay: + 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: + result["probe"] = stage_probe(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: + 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() From e75698688de7300df4f44d86d31738302ea355b8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 20:35:58 +0100 Subject: [PATCH 2/2] fix(research): scope registered L22 replay to the three exclusions The single registered probe command re-ran all nine length-22 splits, including the six capped 2e9-node probes, and was killed at the 600 s per-command cap. Each completed split exclusion now gets its own registered command with a bounded timeout, and the six capped lower-bound probes move to the explicit opt-in --probe-all-splits mode. RESULT.json receipt values and the claim scope are unchanged. --- research/f7-l22-census-probe/README.md | 40 ++++++++--- research/f7-l22-census-probe/VERIFY.json | 35 +++++++-- research/f7-l22-census-probe/verify.py | 92 ++++++++++++++++++++---- 3 files changed, 137 insertions(+), 30 deletions(-) diff --git a/research/f7-l22-census-probe/README.md b/research/f7-l22-census-probe/README.md index 5fb4becd29..3820303ebb 100644 --- a/research/f7-l22-census-probe/README.md +++ b/research/f7-l22-census-probe/README.md @@ -27,7 +27,11 @@ budget; #2973's stop rule was explicitly no L22 census."* 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). + 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 @@ -51,17 +55,28 @@ the real evidence: identical node-exact receipts at every recorded case. From the repository root, with Python 3.12 and a C11 compiler: ```sh -python3 -I -B research/f7-l22-census-probe/verify.py # full: validation + probes -python3 -I -B research/f7-l22-census-probe/verify.py --skip-probe # validation stages only -python3 -I -B research/f7-l22-census-probe/verify.py --probe-cap 500000000 # smaller probes +# 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 `RESULT.json` in this package and prints -`PASS_F7_L22_CENSUS_PROBE`. 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. +`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 @@ -88,6 +103,11 @@ 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), diff --git a/research/f7-l22-census-probe/VERIFY.json b/research/f7-l22-census-probe/VERIFY.json index a74a543c57..31af5cc9bd 100644 --- a/research/f7-l22-census-probe/VERIFY.json +++ b/research/f7-l22-census-probe/VERIFY.json @@ -29,7 +29,7 @@ "{package}/verify.py", "--skip-probe" ], - "timeout_seconds": 600, + "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." }, { @@ -38,11 +38,36 @@ "-I", "-B", "{package}/verify.py", - "--skip-replay" + "--probe-split", + "11,7" ], - "timeout_seconds": 600, - "checks": "Fresh capped length-22 probes at the nine open splits, compared against the committed RESULT.json session receipt: each recorded-complete split must complete again with the identical node count and zero hits; each recorded-aborted split must abort at the cap with zero hits; the fresh cap must not exceed the recorded cap. A probe counts as a finite split exclusion only when its process exits 0 with complete=true and zero hits; capped runs are lower bounds on the tree size and never exclusions." + "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. Default probe cap 2,000,000,000 nodes per split, probes in parallel threads; --probe-cap lowers it (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." + "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/verify.py b/research/f7-l22-census-probe/verify.py index a11e2c71c6..5e3356b584 100644 --- a/research/f7-l22-census-probe/verify.py +++ b/research/f7-l22-census-probe/verify.py @@ -10,11 +10,24 @@ brute-force cross-check (all budget modes) via its check_corrected_c.py; (c) the extended engine, compiled at L=20 and L=18, reproduces all six recorded receipts of the predecessor package node-exactly. -3. Probe: capped census runs at length 22 for the nine open splits of the - L22 split domain. A split whose run finishes with exit 0 and - complete=true and zero hits is a finite exclusion of that split. A run - that hits its cap aborts (exit 2, complete=false) and records only a - LOWER BOUND on that split's tree size. Timing fields are not compared. +3. Probe: census runs at length 22 for the nine open splits of the L22 + split domain. A split whose run finishes with exit 0, complete=true and + zero hits is a finite exclusion of that split. A run that hits its cap + aborts (exit 2, complete=false) and records only a LOWER BOUND on that + split's tree size. Timing fields are not compared. + +Replay scope: + +* The registered checks cover stages 1-2 and a fresh node-exact replay of + the three completed exclusions (11,7), (10,8) and (11,8), one command + per split (`--probe-split S,T`). These three exclusions are the + package's finite claims and are CI-certified. +* `--probe-all-splits` is the opt-in full measurement: it additionally + replays the six capped lower-bound probes against the committed + RESULT.json receipt. That is about 1.4e10 nodes and is not run by CI; + the six capped probes stay locally measured and reproducible. +* The committed RESULT.json session receipt is never rewritten; every run + writes LAST-RUN.json instead. Stage 3 measures the resource budget named as the blocker of the L22 census in research/f7-l22-split-domain (PR #3708) and #2973. No complete @@ -41,6 +54,10 @@ OPEN_SPLITS = [(11, 11), (11, 10), (11, 9), (10, 10), (11, 8), (10, 9), (11, 7), (10, 8), (9, 9)] +# The three splits whose census finished with complete=true and zero hits. +# Registered CI commands replay exactly these, one split per command. +EXCLUSION_SPLITS = [(11, 7), (10, 8), (11, 8)] + RECORDED_CASES = [ ("7", "20", "n7_l20_10_10"), ("7", "20", "n7_l20_10_9"), @@ -181,7 +198,7 @@ def probe_one(split, cap, work): } -def stage_probe(cap, workers): +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 @@ -192,6 +209,10 @@ def stage_probe(cap, workers): 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(), @@ -203,6 +224,9 @@ def stage_probe(cap, workers): 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: @@ -210,8 +234,8 @@ def stage_probe(cap, workers): 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 OPEN_SPLITS} - rows = [futures[split].result() for split in OPEN_SPLITS] + for split in splits} + rows = [futures[split].result() for split in splits] finally: shutil.rmtree(work, ignore_errors=True) for row in rows: @@ -235,37 +259,75 @@ def stage_probe(cap, workers): 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() + 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) - parser.add_argument("--skip-probe", action="store_true", - help="run only integrity, math and validation stages") - parser.add_argument("--skip-replay", action="store_true", - help="probe stage only; skips the slow receipt replay") + 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 args.skip_replay: + 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: - result["probe"] = stage_probe(args.probe_cap, args.workers) + 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"])