diff --git a/research/f7-l22-deep-shard-census/README.md b/research/f7-l22-deep-shard-census/README.md new file mode 100644 index 0000000000..073e240af3 --- /dev/null +++ b/research/f7-l22-deep-shard-census/README.md @@ -0,0 +1,136 @@ +# The length-22 seven-label split census, completed + +**Finite census result inside PR943's singleton prefix-walk model. No kappa, +supplier, tariff, certificate or selected-frontier value changes.** + +[#3818](../f7-l22-union-census/README.md) ran the length-22 seven-label word +census with the corrected union-budget engine and left five splits capped: +`(10,9)`, `(10,10)`, `(11,9)`, `(11,10)` and `(11,11)`. This package runs +those five splits to completion with **the same engine, unchanged**, and finds +**zero restored universal words** in every one. It also runs the two 17-point +splits `(11,6)` and `(10,7)` directly, so the length-22 result no longer needs +the imported 17-point exclusion. + +| Split | Cover shards | Nodes (cover sum) | Hits | #3818 capped floor | +|---|---:|---:|---:|---:| +| `(11,11)` | 251 | 55,385,607,437 | 0 | ≥ 6.0000e9 | +| `(11,10)` | 251 | 52,957,641,635 | 0 | ≥ 7.5000e9 | +| `(11,9)` | 251 | 14,058,107,415 | 0 | ≥ 8.1284e9 | +| `(10,10)` | 251 | 44,378,511,529 | 0 | ≥ 1.43517e10 | +| `(10,9)` | 251 | 7,027,617,655 | 0 | ≥ 6.7976e9 | +| `(10,7)` | 251 | 700,909 | 0 | not run (imported) | +| `(11,6)` | 251 | 2,247 | 0 | not run (imported) | + +## What is established + +1. **Seven finite split exclusions.** Each of the seven splits ran on all 251 + shards of the prefix cover below. Every shard's engine exited 0 with + `complete=true`, zero hits and an empty hit file. No node cap was set. + +2. **The length-22 domain is closed.** The merged split-domain package + [#3708](../f7-l22-split-domain/README.md) proves four necessary + conditions that leave eleven splits (`s >= t` by the rotation symmetry + proved there): `(11,11)`, `(11,10)`, `(11,9)`, `(10,10)`, `(11,8)`, + `(10,9)`, `(11,7)`, `(10,8)`, `(9,9)`, `(11,6)`, `(10,7)`. It then imports + the 17-point exclusions of #2773/#2870 to drop the last two. #3731 and + #3818 excluded `(11,7)`, `(10,8)`, `(11,8)` and `(9,9)`. This package + excludes the other seven, including the two 17-point splits, without the + import. `verify.py --check-receipt` checks that the union is all eleven. + +3. **Consequence for f(7).** #2973 established `22 <= f(7) <= 24` in the same + model, with a length-24 witness. Restored words have even length, so with + length 22 excluded, **`f(7) = 24` inside PR943's prefix-walk model**. This + is conditional on the stated dependencies below. + +### The prefix cover + +#3818 split each run into fifteen depth-four restricted-growth prefixes, and +the heavy shards hit its cap. Here the cover is the 203 restricted-growth +prefixes of length six, with the single prefix of six distinct labels, +`012345`, replaced by its 49 restricted-growth extensions of length eight: +251 shards. Every canonical length-22 word has exactly one prefix in the +cover, so the shards partition the unsharded tree. The verifier checks this +directly: every restricted-growth word of length eight over seven labels has +exactly one prefix in the cover. + +Node counts are raw per-shard sums. Nodes above a shard's prefix are counted +once per descendant shard, so a cover sum is compared only with the same +cover's sum. As a consistency check, the `(10,9)` depth-four shards #3818 +completed (3.7976e9 nodes) plus the 3,230,011,225 nodes of its capped shard +`0123`, measured here on depth-six sub-shards, give 7.0276e9. That matches +this cover's total of 7.0276e9 up to the duplicated prefix nodes. + +## Dependencies, stated exactly + +- **The engine.** `research/f7-l22-union-census/engine/union_census.c` is + used byte-for-byte (SHA256 pinned in `SOURCES.json`). Its pruning rules are + the corrected weight-parity budgets of #2973 and the union-support budget of + #3005/#3818. Their proofs are in those packages; brute-force small-domain + cross-checks are in #3818 and the independent tiny-domain audit #3899 (open). + This package adds no pruning rule. +- **The eleven-split domain.** #3708's four conditions and its rotation + symmetry are proved there; `verify.py` takes the eleven rows from its table + and does not re-derive them. The 17-point import of #2773/#2870 is not + used: `(11,6)` and `(10,7)` are enumerated here. +- **One engine implementation.** The five large exclusions rest on this one C + engine. #3005's separately implemented C++ census has not been run at + length 22. + +This is an exhaustive finite enumeration with a written pruning proof. It is +not a formal-kernel proof, and it is not a statement about every +multiplication algorithm or any supplier. + +## Verification + +```sh +# Registered checks (each well under the 600 s per-command margin): +python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --check-receipt +python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --control +python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --replay S,T:A:B +# (the registered replay slices are listed in VERIFY.json) + +# Full local replay of one split (all 251 shards; opt-in, not run by CI): +python3.12 -I -B research/f7-l22-deep-shard-census/verify.py --replay 11,11 --workers 14 # whole cover by default + +# Regenerate RESULT.json (opt-in; about five CPU-hours): +python3.12 -B research/f7-l22-deep-shard-census/deep_census.py --workers 14 \ + --split 11,11 --split 11,10 --split 11,9 --split 10,10 --split 10,9 \ + --split 10,7 --split 11,6 \ + --work OUT_DIR --output RESULT.json +``` + +- `--check-receipt` checks the engine pin, the cover partition, every split's + 251 shard rows, zero hits, completeness, node totals, and that the closed + splits are exactly #3818's capped ones plus the two 17-point splits, and + that together with #3731/#3818 they close the eleven-split domain. +- `--control` compiles the same engine at `(N,L) = (4,8), (4,10), (5,12)`, + where universal words exist, and builds the same kind of mixed-depth cover. + On every accepted split the sharded hit set equals the unsharded hit set + (77 splits, 2,452 universal words). Dropping a hit-bearing shard is detected. + The receipt check also rejects a cover with one entry removed or one + overlapping entry added. +- `--replay` recomputes a slice of cover entries for one split and requires + each shard's node count to equal `RESULT.json` exactly, with zero hits. + +CI replays only the registered slices (about 1.2e9 nodes). Every split was run in full locally; +the exhaustive replay is opt-in because the seven splits total about 1.74e11 +nodes. + +## Credit + +Predecessors: **Ross Richardson** (PR943, the prefix-walk model), **Aaron +Wang** (PR2542/PR2634 word model), **Nicholas Stone** (#2973, the corrected +engine and `22 <= f(7) <= 24`), **navinor** (#2773, #2870, the 17-point +exclusions), and #3005, #3708, #3731 and #3818 (union budget, split domain and +earlier length-22 probes). This package was produced by Nick Petalas. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. + +## Open next questions + +1. **A second implementation at length 22.** The five exclusions rest on one C + engine. Running #3005's separately implemented C++ census on the same + cover would remove that single point of failure. Blocked by: that engine + is gated at `L <= 20` and its throughput at length 22 is unmeasured. +2. **Recompute the domain inside the verifier.** `verify.py` takes #3708's + eleven rows as given. Re-deriving them from the four conditions here would + make the receipt check self-contained. Blocked by: nothing structural. diff --git a/research/f7-l22-deep-shard-census/RESULT.json b/research/f7-l22-deep-shard-census/RESULT.json new file mode 100644 index 0000000000..baf89975f1 --- /dev/null +++ b/research/f7-l22-deep-shard-census/RESULT.json @@ -0,0 +1,1859 @@ +{ + "base_depth": 6, + "cover_size": 251, + "engine": "research/f7-l22-union-census/engine/union_census.c", + "engine_sha256": "d34a322fc6c9fd41bc9dae337d3e84923f9dfb938c1af42de491cf536fe3cabe", + "expanded": { + "012345": 8 + }, + "splits": [ + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 55385607437, + "per_shard_nodes": { + "000000": 2, + "000001": 2, + "000010": 2, + "000011": 2, + "000012": 2, + "000100": 2, + "000101": 2, + "000102": 2, + "000110": 2, + "000111": 2, + "000112": 2, + "000120": 2, + "000121": 2, + "000122": 2, + "000123": 2, + "001000": 2, + "001001": 2, + "001002": 2, + "001010": 2, + "001011": 2, + "001012": 2, + "001020": 2, + "001021": 2, + "001022": 2, + "001023": 2, + "001100": 2, + "001101": 2, + "001102": 2, + "001110": 2, + "001111": 2, + "001112": 2, + "001120": 2, + "001121": 2, + "001122": 2, + "001123": 2, + "001200": 2, + "001201": 2, + "001202": 2, + "001203": 2, + "001210": 2, + "001211": 2, + "001212": 2, + "001213": 2, + "001220": 2, + "001221": 2, + "001222": 2, + "001223": 2, + "001230": 2, + "001231": 2, + "001232": 2, + "001233": 2, + "001234": 2, + "010000": 4, + "010001": 4, + "010002": 4, + "010010": 4, + "010011": 4, + "010012": 4, + "010020": 4, + "010021": 4, + "010022": 4, + "010023": 4, + "010100": 4, + "010101": 4, + "010102": 4, + "010110": 4, + "010111": 4, + "010112": 4, + "010120": 4, + "010121": 4, + "010122": 4, + "010123": 4, + "010200": 6, + "010201": 136022407, + "010202": 6, + "010203": 830250852, + "010210": 136190043, + "010211": 6, + "010212": 6, + "010213": 781324402, + "010220": 5, + "010221": 5, + "010222": 5, + "010223": 5, + "010230": 857970407, + "010231": 800714899, + "010232": 662460581, + "010233": 6, + "010234": 3045447857, + "011000": 3, + "011001": 3, + "011002": 3, + "011010": 3, + "011011": 3, + "011012": 3, + "011020": 3, + "011021": 3, + "011022": 3, + "011023": 3, + "011100": 3, + "011101": 3, + "011102": 3, + "011110": 3, + "011111": 3, + "011112": 3, + "011120": 3, + "011121": 3, + "011122": 3, + "011123": 3, + "011200": 3, + "011201": 3, + "011202": 3, + "011203": 3, + "011210": 3, + "011211": 3, + "011212": 3, + "011213": 3, + "011220": 3, + "011221": 3, + "011222": 3, + "011223": 3, + "011230": 3, + "011231": 3, + "011232": 3, + "011233": 3, + "011234": 3, + "012000": 5, + "012001": 5, + "012002": 5, + "012003": 5, + "012010": 114411239, + "012011": 6, + "012012": 6, + "012013": 840952358, + "012020": 6, + "012021": 6, + "012022": 6, + "012023": 744831954, + "012030": 768779528, + "012031": 899689960, + "012032": 842693690, + "012033": 6, + "012034": 3292577877, + "012100": 6, + "012101": 136022407, + "012102": 6, + "012103": 797897719, + "012110": 5, + "012111": 5, + "012112": 5, + "012113": 5, + "012120": 5, + "012121": 5, + "012122": 5, + "012123": 5, + "012130": 862763488, + "012131": 712672862, + "012132": 626143897, + "012133": 6, + "012134": 2940899805, + "012200": 4, + "012201": 4, + "012202": 4, + "012203": 4, + "012210": 4, + "012211": 4, + "012212": 4, + "012213": 4, + "012220": 4, + "012221": 4, + "012222": 4, + "012223": 4, + "012230": 4, + "012231": 4, + "012232": 4, + "012233": 4, + "012234": 4, + "012300": 6, + "012301": 846446231, + "012302": 850803093, + "012303": 650859026, + "012304": 3331891222, + "012310": 874855011, + "012311": 6, + "012312": 665305842, + "012313": 517401280, + "012314": 3249773431, + "012320": 841987391, + "012321": 649680039, + "012322": 6, + "012323": 6, + "012324": 2909098770, + "012330": 5, + "012331": 5, + "012332": 5, + "012333": 5, + "012334": 5, + "012340": 3291769197, + "012341": 3149367984, + "012342": 2965949766, + "012343": 2478839049, + "012344": 6, + "01234500": 8, + "01234501": 214246779, + "01234502": 227744175, + "01234503": 217695676, + "01234504": 204941132, + "01234505": 158955779, + "01234506": 260177642, + "01234510": 218435126, + "01234511": 8, + "01234512": 210459487, + "01234513": 212487451, + "01234514": 199050719, + "01234515": 150653617, + "01234516": 263181197, + "01234520": 233977225, + "01234521": 213389709, + "01234522": 8, + "01234523": 183590818, + "01234524": 183413609, + "01234525": 138331387, + "01234526": 259806108, + "01234530": 225390999, + "01234531": 217447475, + "01234532": 187687162, + "01234533": 8, + "01234534": 146850800, + "01234535": 112951611, + "01234536": 248186219, + "01234540": 205048758, + "01234541": 196725277, + "01234542": 183948726, + "01234543": 147357313, + "01234544": 8, + "01234545": 8, + "01234546": 227510836, + "01234550": 7, + "01234551": 7, + "01234552": 7, + "01234553": 7, + "01234554": 7, + "01234555": 7, + "01234556": 7, + "01234560": 261744374, + "01234561": 257013700, + "01234562": 252546401, + "01234563": 241453651, + "01234564": 225585165, + "01234565": 192875083, + "01234566": 8 + }, + "shards": 251, + "split": [ + 11, + 11 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 52957641635, + "per_shard_nodes": { + "000000": 2, + "000001": 2, + "000010": 2, + "000011": 2, + "000012": 2, + "000100": 2, + "000101": 2, + "000102": 2, + "000110": 2, + "000111": 2, + "000112": 2, + "000120": 2, + "000121": 2, + "000122": 2, + "000123": 2, + "001000": 2, + "001001": 2, + "001002": 2, + "001010": 2, + "001011": 2, + "001012": 2, + "001020": 2, + "001021": 2, + "001022": 2, + "001023": 2, + "001100": 2, + "001101": 2, + "001102": 2, + "001110": 2, + "001111": 2, + "001112": 2, + "001120": 2, + "001121": 2, + "001122": 2, + "001123": 2, + "001200": 2, + "001201": 2, + "001202": 2, + "001203": 2, + "001210": 2, + "001211": 2, + "001212": 2, + "001213": 2, + "001220": 2, + "001221": 2, + "001222": 2, + "001223": 2, + "001230": 2, + "001231": 2, + "001232": 2, + "001233": 2, + "001234": 2, + "010000": 4, + "010001": 4, + "010002": 4, + "010010": 4, + "010011": 4, + "010012": 4, + "010020": 4, + "010021": 4, + "010022": 4, + "010023": 4, + "010100": 4, + "010101": 4, + "010102": 4, + "010110": 4, + "010111": 4, + "010112": 4, + "010120": 4, + "010121": 4, + "010122": 4, + "010123": 4, + "010200": 6, + "010201": 100238816, + "010202": 6, + "010203": 581461970, + "010210": 99175189, + "010211": 6, + "010212": 6, + "010213": 553005382, + "010220": 6, + "010221": 6, + "010222": 6, + "010223": 450870321, + "010230": 639813171, + "010231": 612895691, + "010232": 521829620, + "010233": 6, + "010234": 2357627192, + "011000": 4, + "011001": 4, + "011002": 4, + "011010": 4, + "011011": 4, + "011012": 4, + "011020": 4, + "011021": 4, + "011022": 4, + "011023": 4, + "011100": 4, + "011101": 4, + "011102": 4, + "011110": 4, + "011111": 4, + "011112": 4, + "011120": 4, + "011121": 4, + "011122": 4, + "011123": 4, + "011200": 6, + "011201": 99626371, + "011202": 6, + "011203": 501070976, + "011210": 99789386, + "011211": 6, + "011212": 6, + "011213": 518979126, + "011220": 5, + "011221": 5, + "011222": 5, + "011223": 5, + "011230": 514828566, + "011231": 535110348, + "011232": 372489928, + "011233": 6, + "011234": 1798041698, + "012000": 6, + "012001": 83974563, + "012002": 6, + "012003": 552697573, + "012010": 95639528, + "012011": 6, + "012012": 6, + "012013": 608359013, + "012020": 6, + "012021": 6, + "012022": 6, + "012023": 486651051, + "012030": 641121807, + "012031": 717592093, + "012032": 647559087, + "012033": 6, + "012034": 2628015815, + "012100": 6, + "012101": 100238816, + "012102": 6, + "012103": 560666078, + "012110": 99789386, + "012111": 6, + "012112": 6, + "012113": 518979126, + "012120": 6, + "012121": 6, + "012122": 6, + "012123": 452156740, + "012130": 645356080, + "012131": 585076595, + "012132": 482630270, + "012133": 6, + "012134": 2232564296, + "012200": 4, + "012201": 4, + "012202": 4, + "012203": 4, + "012210": 4, + "012211": 4, + "012212": 4, + "012213": 4, + "012220": 4, + "012221": 4, + "012222": 4, + "012223": 4, + "012230": 4, + "012231": 4, + "012232": 4, + "012233": 4, + "012234": 4, + "012300": 6, + "012301": 661745242, + "012302": 659170747, + "012303": 547131831, + "012304": 2697316727, + "012310": 658306191, + "012311": 6, + "012312": 547143429, + "012313": 488470882, + "012314": 2582841557, + "012320": 601506876, + "012321": 511491021, + "012322": 6, + "012323": 6, + "012324": 2131827578, + "012330": 490022137, + "012331": 396004925, + "012332": 6, + "012333": 6, + "012334": 1740559048, + "012340": 2681308447, + "012341": 2601509510, + "012342": 2371686729, + "012343": 2147218187, + "012344": 6, + "01234500": 8, + "01234501": 159936064, + "01234502": 169729290, + "01234503": 165189153, + "01234504": 152972475, + "01234505": 128092603, + "01234506": 196570615, + "01234510": 162223295, + "01234511": 8, + "01234512": 156598601, + "01234513": 162268465, + "01234514": 150154881, + "01234515": 124862505, + "01234516": 199214103, + "01234520": 171458129, + "01234521": 157173636, + "01234522": 8, + "01234523": 131760529, + "01234524": 132560329, + "01234525": 112112886, + "01234526": 189232833, + "01234530": 162767276, + "01234531": 159383026, + "01234532": 129072269, + "01234533": 8, + "01234534": 112442639, + "01234535": 103780353, + "01234536": 178420240, + "01234540": 137123514, + "01234541": 133828250, + "01234542": 120889839, + "01234543": 107372413, + "01234544": 8, + "01234545": 8, + "01234546": 152412511, + "01234550": 117493826, + "01234551": 112581508, + "01234552": 103037345, + "01234553": 85689190, + "01234554": 8, + "01234555": 8, + "01234556": 131513285, + "01234560": 195113108, + "01234561": 194189318, + "01234562": 184900188, + "01234563": 179928397, + "01234564": 166684876, + "01234565": 155724500, + "01234566": 8 + }, + "shards": 251, + "split": [ + 11, + 10 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 14058107415, + "per_shard_nodes": { + "000000": 2, + "000001": 2, + "000010": 2, + "000011": 2, + "000012": 2, + "000100": 2, + "000101": 2, + "000102": 2, + "000110": 2, + "000111": 2, + "000112": 2, + "000120": 2, + "000121": 2, + "000122": 2, + "000123": 2, + "001000": 2, + "001001": 2, + "001002": 2, + "001010": 2, + "001011": 2, + "001012": 2, + "001020": 2, + "001021": 2, + "001022": 2, + "001023": 2, + "001100": 2, + "001101": 2, + "001102": 2, + "001110": 2, + "001111": 2, + "001112": 2, + "001120": 2, + "001121": 2, + "001122": 2, + "001123": 2, + "001200": 2, + "001201": 2, + "001202": 2, + "001203": 2, + "001210": 2, + "001211": 2, + "001212": 2, + "001213": 2, + "001220": 2, + "001221": 2, + "001222": 2, + "001223": 2, + "001230": 2, + "001231": 2, + "001232": 2, + "001233": 2, + "001234": 2, + "010000": 4, + "010001": 4, + "010002": 4, + "010010": 4, + "010011": 4, + "010012": 4, + "010020": 4, + "010021": 4, + "010022": 4, + "010023": 4, + "010100": 4, + "010101": 4, + "010102": 4, + "010110": 4, + "010111": 4, + "010112": 4, + "010120": 4, + "010121": 4, + "010122": 4, + "010123": 4, + "010200": 6, + "010201": 15623211, + "010202": 6, + "010203": 93589833, + "010210": 15271491, + "010211": 6, + "010212": 6, + "010213": 89020650, + "010220": 6, + "010221": 6, + "010222": 6, + "010223": 203064816, + "010230": 120502781, + "010231": 117043611, + "010232": 104614815, + "010233": 6, + "010234": 484000531, + "011000": 4, + "011001": 4, + "011002": 4, + "011010": 4, + "011011": 4, + "011012": 4, + "011020": 4, + "011021": 4, + "011022": 4, + "011023": 4, + "011100": 4, + "011101": 4, + "011102": 4, + "011110": 4, + "011111": 4, + "011112": 4, + "011120": 4, + "011121": 4, + "011122": 4, + "011123": 4, + "011200": 6, + "011201": 42958285, + "011202": 6, + "011203": 239036737, + "011210": 43470505, + "011211": 6, + "011212": 6, + "011213": 247625021, + "011220": 6, + "011221": 6, + "011222": 6, + "011223": 206818714, + "011230": 273369927, + "011231": 281271554, + "011232": 198347963, + "011233": 6, + "011234": 981220276, + "012000": 6, + "012001": 41821228, + "012002": 6, + "012003": 285286024, + "012010": 16562617, + "012011": 6, + "012012": 6, + "012013": 100046075, + "012020": 6, + "012021": 6, + "012022": 6, + "012023": 71780078, + "012030": 134210637, + "012031": 151644210, + "012032": 132526386, + "012033": 6, + "012034": 578742048, + "012100": 6, + "012101": 15623211, + "012102": 6, + "012103": 90662935, + "012110": 43470505, + "012111": 6, + "012112": 6, + "012113": 247625021, + "012120": 6, + "012121": 6, + "012122": 6, + "012123": 202061271, + "012130": 125343462, + "012131": 110936930, + "012132": 86855958, + "012133": 6, + "012134": 436396425, + "012200": 4, + "012201": 4, + "012202": 4, + "012203": 4, + "012210": 4, + "012211": 4, + "012212": 4, + "012213": 4, + "012220": 4, + "012221": 4, + "012222": 4, + "012223": 4, + "012230": 4, + "012231": 4, + "012232": 4, + "012233": 4, + "012234": 4, + "012300": 6, + "012301": 132705502, + "012302": 138334677, + "012303": 116813864, + "012304": 608752046, + "012310": 127922009, + "012311": 6, + "012312": 106019123, + "012313": 103284826, + "012314": 544540661, + "012320": 112404831, + "012321": 95148003, + "012322": 6, + "012323": 6, + "012324": 401778982, + "012330": 249028605, + "012331": 210258436, + "012332": 6, + "012333": 6, + "012334": 915843949, + "012340": 608354904, + "012341": 589042299, + "012342": 521731320, + "012343": 498172684, + "012344": 6, + "01234500": 8, + "01234501": 31865583, + "01234502": 36534138, + "01234503": 35264794, + "01234504": 31564073, + "01234505": 27126637, + "01234506": 40488026, + "01234510": 32370088, + "01234511": 8, + "01234512": 31111419, + "01234513": 34948655, + "01234514": 31379075, + "01234515": 26830285, + "01234516": 42321044, + "01234520": 36246515, + "01234521": 30304726, + "01234522": 8, + "01234523": 25343075, + "01234524": 26384422, + "01234525": 23660122, + "01234526": 39244651, + "01234530": 31869761, + "01234531": 31279857, + "01234532": 23895379, + "01234533": 8, + "01234534": 20966039, + "01234535": 22249308, + "01234536": 33936594, + "01234540": 24025987, + "01234541": 23616958, + "01234542": 21347224, + "01234543": 19526252, + "01234544": 8, + "01234545": 8, + "01234546": 26195825, + "01234550": 57184045, + "01234551": 55152945, + "01234552": 49306257, + "01234553": 44032177, + "01234554": 8, + "01234555": 8, + "01234556": 63471340, + "01234560": 39144268, + "01234561": 39244885, + "01234562": 37624723, + "01234563": 36635594, + "01234564": 32708240, + "01234565": 33123328, + "01234566": 8 + }, + "shards": 251, + "split": [ + 11, + 9 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 44378511529, + "per_shard_nodes": { + "000000": 4, + "000001": 4, + "000010": 4, + "000011": 4, + "000012": 4, + "000100": 6, + "000101": 6, + "000102": 46978979, + "000110": 5, + "000111": 5, + "000112": 5, + "000120": 52230534, + "000121": 38781219, + "000122": 6, + "000123": 254781822, + "001000": 6, + "001001": 6, + "001002": 46978979, + "001010": 6, + "001011": 6, + "001012": 46978979, + "001020": 42361183, + "001021": 42361183, + "001022": 6, + "001023": 269334537, + "001100": 4, + "001101": 4, + "001102": 4, + "001110": 4, + "001111": 4, + "001112": 4, + "001120": 4, + "001121": 4, + "001122": 4, + "001123": 4, + "001200": 6, + "001201": 47383986, + "001202": 40825816, + "001203": 317635010, + "001210": 42226243, + "001211": 6, + "001212": 6, + "001213": 228310623, + "001220": 39259707, + "001221": 6, + "001222": 6, + "001223": 225284264, + "001230": 320668656, + "001231": 275357401, + "001232": 239161291, + "001233": 6, + "001234": 1071848102, + "010000": 6, + "010001": 6, + "010002": 46978979, + "010010": 6, + "010011": 6, + "010012": 46978979, + "010020": 42361183, + "010021": 42361183, + "010022": 6, + "010023": 269334537, + "010100": 6, + "010101": 6, + "010102": 46978979, + "010110": 6, + "010111": 6, + "010112": 46978979, + "010120": 42226243, + "010121": 42226243, + "010122": 6, + "010123": 256747883, + "010200": 42361183, + "010201": 44346115, + "010202": 40825816, + "010203": 304229262, + "010210": 43447703, + "010211": 42226243, + "010212": 39028057, + "010213": 289136389, + "010220": 39259707, + "010221": 37489610, + "010222": 46978979, + "010223": 210549374, + "010230": 363267710, + "010231": 350416610, + "010232": 288346956, + "010233": 227444433, + "010234": 1471443154, + "011000": 5, + "011001": 5, + "011002": 5, + "011010": 6, + "011011": 6, + "011012": 46978979, + "011020": 39259707, + "011021": 52533640, + "011022": 6, + "011023": 248225424, + "011100": 6, + "011101": 6, + "011102": 46978979, + "011110": 5, + "011111": 5, + "011112": 5, + "011120": 52230534, + "011121": 38781219, + "011122": 6, + "011123": 254781822, + "011200": 39259707, + "011201": 42735695, + "011202": 37489610, + "011203": 238718423, + "011210": 43080185, + "011211": 38781219, + "011212": 38781219, + "011213": 247387694, + "011220": 5, + "011221": 5, + "011222": 5, + "011223": 5, + "011230": 267598704, + "011231": 276599313, + "011232": 161835565, + "011233": 171767154, + "011234": 943371963, + "012000": 52230534, + "012001": 33621650, + "012002": 42563135, + "012003": 287631704, + "012010": 40210792, + "012011": 47383986, + "012012": 45502329, + "012013": 330946370, + "012020": 40825816, + "012021": 41051889, + "012022": 42361183, + "012023": 253875302, + "012030": 358979281, + "012031": 446678472, + "012032": 397683911, + "012033": 262748433, + "012034": 1757992276, + "012100": 40825816, + "012101": 44346115, + "012102": 41051889, + "012103": 294544508, + "012110": 43080185, + "012111": 38781219, + "012112": 38781219, + "012113": 247387694, + "012120": 46068307, + "012121": 38781219, + "012122": 38781219, + "012123": 210153254, + "012130": 378820363, + "012131": 299982009, + "012132": 243677745, + "012133": 206464863, + "012134": 1309409127, + "012200": 6, + "012201": 6, + "012202": 42361183, + "012203": 230476323, + "012210": 6, + "012211": 6, + "012212": 38781219, + "012213": 225579740, + "012220": 52230534, + "012221": 38781219, + "012222": 6, + "012223": 254781822, + "012230": 266325551, + "012231": 222005917, + "012232": 271703378, + "012233": 6, + "012234": 969573485, + "012300": 305221417, + "012301": 379125961, + "012302": 419125577, + "012303": 312372235, + "012304": 1865560795, + "012310": 379076053, + "012311": 302489887, + "012312": 297051801, + "012313": 246919637, + "012314": 1700116434, + "012320": 368330348, + "012321": 274256107, + "012322": 271703378, + "012323": 219784089, + "012324": 1310993198, + "012330": 259313675, + "012331": 178800595, + "012332": 183139309, + "012333": 254781822, + "012334": 935113993, + "012340": 1843715682, + "012341": 1725172200, + "012342": 1547205656, + "012343": 1316879922, + "012344": 962034556, + "01234500": 64373547, + "01234501": 90597157, + "01234502": 112513364, + "01234503": 106072576, + "01234504": 95567188, + "01234505": 72256946, + "01234506": 127338484, + "01234510": 94319261, + "01234511": 66166334, + "01234512": 93551935, + "01234513": 102824522, + "01234514": 94676529, + "01234515": 69272997, + "01234516": 133046410, + "01234520": 114482489, + "01234521": 92731842, + "01234522": 66850791, + "01234523": 73420161, + "01234524": 83453209, + "01234525": 63424690, + "01234526": 125740509, + "01234530": 102498071, + "01234531": 97404186, + "01234532": 70466503, + "01234533": 64848330, + "01234534": 60192714, + "01234535": 53768965, + "01234536": 109613219, + "01234540": 81676112, + "01234541": 78368402, + "01234542": 72696714, + "01234543": 57962199, + "01234544": 60489318, + "01234545": 46430361, + "01234546": 89798634, + "01234550": 58442675, + "01234551": 53952406, + "01234552": 50226261, + "01234553": 36737274, + "01234554": 38062845, + "01234555": 57314907, + "01234556": 64956724, + "01234560": 124179883, + "01234561": 122004439, + "01234562": 117713957, + "01234563": 111080178, + "01234564": 101536768, + "01234565": 90966013, + "01234566": 68437919 + }, + "shards": 251, + "split": [ + 10, + 10 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 7027617655, + "per_shard_nodes": { + "000000": 4, + "000001": 4, + "000010": 4, + "000011": 4, + "000012": 4, + "000100": 6, + "000101": 6, + "000102": 11030905, + "000110": 6, + "000111": 6, + "000112": 12953687, + "000120": 13750107, + "000121": 10957342, + "000122": 6, + "000123": 70924030, + "001000": 6, + "001001": 6, + "001002": 11030905, + "001010": 6, + "001011": 6, + "001012": 11030905, + "001020": 3947046, + "001021": 3947046, + "001022": 6, + "001023": 25435191, + "001100": 4, + "001101": 4, + "001102": 4, + "001110": 4, + "001111": 4, + "001112": 4, + "001120": 4, + "001121": 4, + "001122": 4, + "001123": 4, + "001200": 6, + "001201": 4970400, + "001202": 4437424, + "001203": 33249696, + "001210": 3927597, + "001211": 6, + "001212": 6, + "001213": 20340021, + "001220": 10972550, + "001221": 6, + "001222": 6, + "001223": 57873645, + "001230": 33863078, + "001231": 29074304, + "001232": 26718278, + "001233": 6, + "001234": 117369897, + "010000": 6, + "010001": 6, + "010002": 11030905, + "010010": 6, + "010011": 6, + "010012": 11030905, + "010020": 3947046, + "010021": 3947046, + "010022": 6, + "010023": 25435191, + "010100": 6, + "010101": 6, + "010102": 11030905, + "010110": 6, + "010111": 6, + "010112": 11030905, + "010120": 3927597, + "010121": 3927597, + "010122": 6, + "010123": 24942875, + "010200": 3947046, + "010201": 4324321, + "010202": 4437424, + "010203": 30703088, + "010210": 4291762, + "010211": 3927597, + "010212": 4396842, + "010213": 30328802, + "010220": 10972550, + "010221": 10802782, + "010222": 11030905, + "010223": 59033077, + "010230": 38518818, + "010231": 38167866, + "010232": 36399251, + "010233": 25942165, + "010234": 173943788, + "011000": 6, + "011001": 6, + "011002": 12953687, + "011010": 6, + "011011": 6, + "011012": 11030905, + "011020": 10972550, + "011021": 13747751, + "011022": 6, + "011023": 69942376, + "011100": 6, + "011101": 6, + "011102": 11030905, + "011110": 6, + "011111": 6, + "011112": 12953687, + "011120": 13750107, + "011121": 10957342, + "011122": 6, + "011123": 70924030, + "011200": 10972550, + "011201": 10672975, + "011202": 10802782, + "011203": 74976371, + "011210": 10727378, + "011211": 10957342, + "011212": 10957342, + "011213": 76062750, + "011220": 12806409, + "011221": 12953687, + "011222": 12953687, + "011223": 50648855, + "011230": 88995906, + "011231": 89995625, + "011232": 56080717, + "011233": 54071376, + "011234": 320254076, + "012000": 13750107, + "012001": 9865558, + "012002": 13155957, + "012003": 93076356, + "012010": 4646207, + "012011": 4970400, + "012012": 4922345, + "012013": 36421369, + "012020": 4437424, + "012021": 3916878, + "012022": 3947046, + "012023": 23478551, + "012030": 45688721, + "012031": 55427913, + "012032": 48317273, + "012033": 33886568, + "012034": 223484942, + "012100": 4437424, + "012101": 4324321, + "012102": 3916878, + "012103": 30445149, + "012110": 10727378, + "012111": 10957342, + "012112": 10957342, + "012113": 76062750, + "012120": 10904655, + "012121": 10957342, + "012122": 10957342, + "012123": 58946354, + "012130": 43395353, + "012131": 36123735, + "012132": 27859339, + "012133": 26941064, + "012134": 154212251, + "012200": 6, + "012201": 6, + "012202": 3947046, + "012203": 20423248, + "012210": 6, + "012211": 6, + "012212": 10957342, + "012213": 57822778, + "012220": 13750107, + "012221": 10957342, + "012222": 6, + "012223": 70924030, + "012230": 26185534, + "012231": 23590610, + "012232": 30516020, + "012233": 6, + "012234": 100635771, + "012300": 38382161, + "012301": 41636136, + "012302": 52122610, + "012303": 40448861, + "012304": 246334944, + "012310": 41233619, + "012311": 37599357, + "012312": 38629483, + "012313": 36568968, + "012314": 229977308, + "012320": 42165080, + "012321": 33259716, + "012322": 30516020, + "012323": 29024711, + "012324": 153778766, + "012330": 83747872, + "012331": 66994969, + "012332": 58533722, + "012333": 70924030, + "012334": 311280435, + "012340": 241649105, + "012341": 230948341, + "012342": 202567617, + "012343": 192357001, + "012344": 128923236, + "01234500": 7714718, + "01234501": 8972772, + "01234502": 12877941, + "01234503": 12620378, + "01234504": 11573196, + "01234505": 9117455, + "01234506": 15435789, + "01234510": 9374296, + "01234511": 7799962, + "01234512": 9835292, + "01234513": 12317349, + "01234514": 11514919, + "01234515": 9057667, + "01234516": 16146089, + "01234520": 13093497, + "01234521": 9752651, + "01234522": 7667008, + "01234523": 7534137, + "01234524": 9764162, + "01234525": 8198020, + "01234526": 15076167, + "01234530": 12256310, + "01234531": 11727524, + "01234532": 7194067, + "01234533": 7372359, + "01234534": 7944150, + "01234535": 8163228, + "01234536": 13686025, + "01234540": 8758689, + "01234541": 8523885, + "01234542": 7939155, + "01234543": 7145851, + "01234544": 6339559, + "01234545": 6111955, + "01234546": 10115469, + "01234550": 17793699, + "01234551": 16942501, + "01234552": 15604409, + "01234553": 13708880, + "01234554": 11709727, + "01234555": 14595082, + "01234556": 20571827, + "01234560": 14880975, + "01234561": 14530736, + "01234562": 13847626, + "01234563": 13696011, + "01234564": 12565641, + "01234565": 12811442, + "01234566": 8427288 + }, + "shards": 251, + "split": [ + 10, + 9 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 700909, + "per_shard_nodes": { + "000000": 4, + "000001": 4, + "000010": 4, + "000011": 4, + "000012": 4, + "000100": 6, + "000101": 6, + "000102": 947, + "000110": 6, + "000111": 6, + "000112": 9206, + "000120": 1955, + "000121": 1646, + "000122": 6, + "000123": 11357, + "001000": 6, + "001001": 6, + "001002": 947, + "001010": 6, + "001011": 6, + "001012": 947, + "001020": 54, + "001021": 54, + "001022": 6, + "001023": 589, + "001100": 4, + "001101": 4, + "001102": 4, + "001110": 4, + "001111": 4, + "001112": 4, + "001120": 4, + "001121": 4, + "001122": 4, + "001123": 4, + "001200": 6, + "001201": 54, + "001202": 72, + "001203": 1465, + "001210": 54, + "001211": 6, + "001212": 6, + "001213": 837, + "001220": 1646, + "001221": 6, + "001222": 6, + "001223": 8265, + "001230": 1361, + "001231": 1237, + "001232": 1263, + "001233": 6, + "001234": 5951, + "010000": 6, + "010001": 6, + "010002": 947, + "010010": 6, + "010011": 6, + "010012": 947, + "010020": 54, + "010021": 54, + "010022": 6, + "010023": 589, + "010100": 6, + "010101": 6, + "010102": 947, + "010110": 6, + "010111": 6, + "010112": 947, + "010120": 54, + "010121": 54, + "010122": 6, + "010123": 589, + "010200": 54, + "010201": 6, + "010202": 72, + "010203": 243, + "010210": 6, + "010211": 54, + "010212": 72, + "010213": 243, + "010220": 1646, + "010221": 1646, + "010222": 947, + "010223": 9005, + "010230": 178, + "010231": 178, + "010232": 1801, + "010233": 1147, + "010234": 5590, + "011000": 6, + "011001": 6, + "011002": 9206, + "011010": 6, + "011011": 6, + "011012": 947, + "011020": 1646, + "011021": 1955, + "011022": 6, + "011023": 11357, + "011100": 6, + "011101": 6, + "011102": 947, + "011110": 6, + "011111": 6, + "011112": 9206, + "011120": 1955, + "011121": 1646, + "011122": 6, + "011123": 11357, + "011200": 1646, + "011201": 6, + "011202": 1646, + "011203": 11001, + "011210": 6, + "011211": 1646, + "011212": 1646, + "011213": 11001, + "011220": 9206, + "011221": 9206, + "011222": 9206, + "011223": 50505, + "011230": 12916, + "011231": 12916, + "011232": 13061, + "011233": 13000, + "011234": 61410, + "012000": 1955, + "012001": 6, + "012002": 2654, + "012003": 15872, + "012010": 6, + "012011": 54, + "012012": 54, + "012013": 226, + "012020": 72, + "012021": 54, + "012022": 54, + "012023": 291, + "012030": 396, + "012031": 1954, + "012032": 1941, + "012033": 2377, + "012034": 11472, + "012100": 72, + "012101": 6, + "012102": 54, + "012103": 243, + "012110": 6, + "012111": 1646, + "012112": 1646, + "012113": 11001, + "012120": 947, + "012121": 1646, + "012122": 1646, + "012123": 9005, + "012130": 1510, + "012131": 430, + "012132": 461, + "012133": 1877, + "012134": 7159, + "012200": 6, + "012201": 6, + "012202": 54, + "012203": 837, + "012210": 6, + "012211": 6, + "012212": 1646, + "012213": 8265, + "012220": 1955, + "012221": 1646, + "012222": 6, + "012223": 11357, + "012230": 1157, + "012231": 1259, + "012232": 1427, + "012233": 6, + "012234": 5661, + "012300": 2147, + "012301": 6, + "012302": 1870, + "012303": 396, + "012304": 9677, + "012310": 6, + "012311": 2187, + "012312": 379, + "012313": 631, + "012314": 9666, + "012320": 1656, + "012321": 461, + "012322": 1427, + "012323": 1659, + "012324": 7623, + "012330": 13739, + "012331": 16091, + "012332": 15008, + "012333": 11357, + "012334": 61945, + "012340": 9835, + "012341": 8673, + "012342": 8090, + "012343": 12268, + "012344": 10292, + "01234500": 414, + "01234501": 8, + "01234502": 264, + "01234503": 191, + "01234504": 257, + "01234505": 79, + "01234506": 463, + "01234510": 8, + "01234511": 397, + "01234512": 36, + "01234513": 187, + "01234514": 185, + "01234515": 79, + "01234516": 408, + "01234520": 281, + "01234521": 36, + "01234522": 431, + "01234523": 8, + "01234524": 253, + "01234525": 79, + "01234526": 459, + "01234530": 208, + "01234531": 187, + "01234532": 8, + "01234533": 369, + "01234534": 79, + "01234535": 130, + "01234536": 433, + "01234540": 336, + "01234541": 214, + "01234542": 308, + "01234543": 98, + "01234544": 316, + "01234545": 387, + "01234546": 485, + "01234550": 2347, + "01234551": 2029, + "01234552": 1930, + "01234553": 3199, + "01234554": 2866, + "01234555": 1953, + "01234556": 3770, + "01234560": 736, + "01234561": 551, + "01234562": 613, + "01234563": 609, + "01234564": 383, + "01234565": 1328, + "01234566": 833 + }, + "shards": 251, + "split": [ + 10, + 7 + ] + }, + { + "complete": true, + "hit_words": [], + "hits": 0, + "nodes": 2247, + "per_shard_nodes": { + "000000": 2, + "000001": 2, + "000010": 2, + "000011": 2, + "000012": 2, + "000100": 2, + "000101": 2, + "000102": 2, + "000110": 2, + "000111": 2, + "000112": 2, + "000120": 2, + "000121": 2, + "000122": 2, + "000123": 2, + "001000": 2, + "001001": 2, + "001002": 2, + "001010": 2, + "001011": 2, + "001012": 2, + "001020": 2, + "001021": 2, + "001022": 2, + "001023": 2, + "001100": 2, + "001101": 2, + "001102": 2, + "001110": 2, + "001111": 2, + "001112": 2, + "001120": 2, + "001121": 2, + "001122": 2, + "001123": 2, + "001200": 2, + "001201": 2, + "001202": 2, + "001203": 2, + "001210": 2, + "001211": 2, + "001212": 2, + "001213": 2, + "001220": 2, + "001221": 2, + "001222": 2, + "001223": 2, + "001230": 2, + "001231": 2, + "001232": 2, + "001233": 2, + "001234": 2, + "010000": 4, + "010001": 4, + "010002": 4, + "010010": 4, + "010011": 4, + "010012": 4, + "010020": 4, + "010021": 4, + "010022": 4, + "010023": 4, + "010100": 4, + "010101": 4, + "010102": 4, + "010110": 4, + "010111": 4, + "010112": 4, + "010120": 4, + "010121": 4, + "010122": 4, + "010123": 4, + "010200": 5, + "010201": 5, + "010202": 5, + "010203": 5, + "010210": 5, + "010211": 5, + "010212": 5, + "010213": 5, + "010220": 6, + "010221": 6, + "010222": 6, + "010223": 24, + "010230": 6, + "010231": 6, + "010232": 6, + "010233": 6, + "010234": 16, + "011000": 4, + "011001": 4, + "011002": 4, + "011010": 4, + "011011": 4, + "011012": 4, + "011020": 4, + "011021": 4, + "011022": 4, + "011023": 4, + "011100": 4, + "011101": 4, + "011102": 4, + "011110": 4, + "011111": 4, + "011112": 4, + "011120": 4, + "011121": 4, + "011122": 4, + "011123": 4, + "011200": 6, + "011201": 6, + "011202": 6, + "011203": 24, + "011210": 6, + "011211": 6, + "011212": 6, + "011213": 24, + "011220": 6, + "011221": 6, + "011222": 6, + "011223": 271, + "011230": 24, + "011231": 24, + "011232": 35, + "011233": 6, + "011234": 180, + "012000": 6, + "012001": 6, + "012002": 6, + "012003": 24, + "012010": 5, + "012011": 5, + "012012": 5, + "012013": 5, + "012020": 5, + "012021": 5, + "012022": 5, + "012023": 5, + "012030": 6, + "012031": 6, + "012032": 6, + "012033": 6, + "012034": 16, + "012100": 5, + "012101": 5, + "012102": 5, + "012103": 5, + "012110": 6, + "012111": 6, + "012112": 6, + "012113": 24, + "012120": 6, + "012121": 6, + "012122": 6, + "012123": 24, + "012130": 6, + "012131": 6, + "012132": 6, + "012133": 6, + "012134": 16, + "012200": 4, + "012201": 4, + "012202": 4, + "012203": 4, + "012210": 4, + "012211": 4, + "012212": 4, + "012213": 4, + "012220": 4, + "012221": 4, + "012222": 4, + "012223": 4, + "012230": 4, + "012231": 4, + "012232": 4, + "012233": 4, + "012234": 4, + "012300": 6, + "012301": 6, + "012302": 6, + "012303": 6, + "012304": 16, + "012310": 6, + "012311": 6, + "012312": 6, + "012313": 6, + "012314": 16, + "012320": 6, + "012321": 6, + "012322": 6, + "012323": 6, + "012324": 16, + "012330": 24, + "012331": 35, + "012332": 6, + "012333": 6, + "012334": 163, + "012340": 16, + "012341": 16, + "012342": 16, + "012343": 22, + "012344": 6, + "01234500": 8, + "01234501": 8, + "01234502": 8, + "01234503": 8, + "01234504": 8, + "01234505": 8, + "01234506": 10, + "01234510": 8, + "01234511": 8, + "01234512": 8, + "01234513": 8, + "01234514": 8, + "01234515": 8, + "01234516": 10, + "01234520": 8, + "01234521": 8, + "01234522": 8, + "01234523": 8, + "01234524": 8, + "01234525": 8, + "01234526": 10, + "01234530": 8, + "01234531": 8, + "01234532": 8, + "01234533": 8, + "01234534": 8, + "01234535": 8, + "01234536": 10, + "01234540": 8, + "01234541": 8, + "01234542": 8, + "01234543": 8, + "01234544": 8, + "01234545": 8, + "01234546": 10, + "01234550": 13, + "01234551": 13, + "01234552": 13, + "01234553": 16, + "01234554": 8, + "01234555": 8, + "01234556": 25, + "01234560": 10, + "01234561": 10, + "01234562": 10, + "01234563": 10, + "01234564": 10, + "01234565": 11, + "01234566": 8 + }, + "shards": 251, + "split": [ + 11, + 6 + ] + } + ] +} diff --git a/research/f7-l22-deep-shard-census/SOURCES.json b/research/f7-l22-deep-shard-census/SOURCES.json new file mode 100644 index 0000000000..2b613280d6 --- /dev/null +++ b/research/f7-l22-deep-shard-census/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/f7-l22-union-census/README.md", + "usage": "input", + "git_blob": "7fdb9c2a4cc84fdee577bad15263fbfd0a9f6687", + "sha256": "d5b490a7c55a74f7be571655530018db49689cd7207a28b9e3ea9c9b2c8b779c" + }, + { + "path": "research/f7-l22-union-census/RESULT.json", + "usage": "input", + "git_blob": "e845a493dbedb7556658a1f05e7f3d5b8652ecac", + "sha256": "292277ff25d6c63f2443b65aa2f6955d35beb116b0984a5457a1a8fa82633533" + }, + { + "path": "research/f7-l22-union-census/engine/union_census.c", + "usage": "input", + "git_blob": "b2742d3f711b468b287acb3fb65e8d27938e448f", + "sha256": "d34a322fc6c9fd41bc9dae337d3e84923f9dfb938c1af42de491cf536fe3cabe" + } + ] +} diff --git a/research/f7-l22-deep-shard-census/TASK.json b/research/f7-l22-deep-shard-census/TASK.json new file mode 100644 index 0000000000..525adbd4ee --- /dev/null +++ b/research/f7-l22-deep-shard-census/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "refined", + "actual_scope": "Finish the length-22 seven-label split census that research/f7-l22-union-census (#3818) left capped. The five capped splits (10,9), (10,10), (11,9), (11,10), (11,11), and the two 17-point splits (11,6), (10,7) that #3708 removed only by importing #2773/#2870, are run with the unchanged merged union-budget engine on a 251-entry prefix-free cover (the 203 depth-six restricted-growth prefixes, with 012345 replaced by its 49 depth-eight extensions), with no node cap. A split is a finite exclusion only if all 251 shards exit complete with zero hits. A small-domain partition control compares sharded and unsharded hit sets where universal words exist.", + "scope_change_reason": "The card asks which census exclusions are sound and which bounded repair is justified. #3818 already ported a proved, mutant-tested prune into the corrected engine and left an explicit resource-limited open question (OQ1): five length-22 splits capped. The named decision is f(7) in {22, 24} inside PR943's prefix-walk model (#2973). This package changes no pruning rule; it only removes the cap by finer sharding and records the receipts.", + "bottleneck_link": "Side result in the word-census line. It settles the length-22 question that #2973, #3708, #3731 and #3818 left open, inside the stated finite model. It changes no supplier, tariff, kappa or selected record.", + "budget_minutes": 60, + "stop_rule": "Stop after each target split has been run on all 251 cover shards or the session budget is exhausted. Any hit word is reported verbatim and the exclusion withdrawn. A split with any incomplete shard is not an exclusion.", + "outcome": "completed", + "evidence": "RESULT.json: all seven target splits complete on all 251 cover shards with zero hits ((11,11) 55,385,607,437 nodes; (11,10) 52,957,641,635; (10,10) 44,378,511,529; (11,9) 14,058,107,415; (10,9) 7,027,617,655; (10,7) 700,909; (11,6) 2,247). With #3731/#3818's four exclusions they close all eleven rows of #3708's length-22 table, so no restored universal length-22 seven-label word exists in PR943's prefix-walk model, and with #2973's bounds f(7) = 24 in that model. verify.py checks the engine pin, the cover partition, the receipt and the domain closure, runs a sharded-versus-unsharded control on small domains with real universal words, and replays registered cover slices with exact per-shard node equality.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a separately implemented census (for example #3005's C++ engine) reproduce the seven length-22 split exclusions?", + "why_it_matters": "The f(7) = 24 conclusion in the prefix-walk model rests on one C engine and its written pruning proofs.", + "first_step": "Lift #3005's L <= 20 gate to 22, run (10,9) on the same 251-entry cover, and compare zero-hit completion shard by shard.", + "blocked_by": "The #3005 engine's throughput at length 22 is unmeasured; the largest splits need about 5e10 nodes each." + }, + { + "question": "Can verify.py re-derive #3708's eleven-row length-22 domain from the four necessary conditions instead of taking the table as given?", + "why_it_matters": "It would make the domain-closure check self-contained.", + "first_step": "Port #3708's arithmetic checks (time bound, odd budget, even budget, pair identity) into verify.py and compare the row set.", + "blocked_by": "Nothing structural." + } + ] +} diff --git a/research/f7-l22-deep-shard-census/VERIFY.json b/research/f7-l22-deep-shard-census/VERIFY.json new file mode 100644 index 0000000000..37d8167a19 --- /dev/null +++ b/research/f7-l22-deep-shard-census/VERIFY.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-l22-union-census/README.md", + "research/f7-l22-union-census/RESULT.json", + "research/f7-l22-union-census/engine/union_census.c" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--check-receipt", + "--control" + ], + "timeout_seconds": 150, + "checks": "Engine bytes equal the SOURCES.json pin; the 251-entry cover is prefix-free and complete over all restricted-growth words of length eight; every recorded split has 251 complete zero-hit shard rows whose node sum equals its total; the closed splits are exactly #3818's capped splits plus (11,6) and (10,7); with #3731/#3818's exclusions they close all eleven rows of #3708's length-22 table. Partition control: the same engine compiled at (N,L)=(4,8),(4,10),(5,12) with the same kind of mixed-depth cover; on every accepted split the sharded hit set equals the unsharded hit set (77 splits, 2,452 universal words), and a dropped hit-bearing shard is detected." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "10,9:231:251", + "--workers", + "4" + ], + "timeout_seconds": 150, + "checks": "Fresh length-22 census of cover entries [231,251) of split (10,9): every shard complete with zero hits and per-shard node counts equal to RESULT.json (247,861,718 nodes)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "11,9:244:251", + "--workers", + "4" + ], + "timeout_seconds": 150, + "checks": "Fresh length-22 census of cover entries [244,251) of split (11,9): every shard complete with zero hits and per-shard node counts equal to RESULT.json (218,481,046 nodes)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "11,11:249:251", + "--workers", + "4" + ], + "timeout_seconds": 150, + "checks": "Fresh length-22 census of cover entries [249,251) of split (11,11): every shard complete with zero hits and per-shard node counts equal to RESULT.json (192,875,091 nodes)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "11,10:249:251", + "--workers", + "4" + ], + "timeout_seconds": 150, + "checks": "Fresh length-22 census of cover entries [249,251) of split (11,10): every shard complete with zero hits and per-shard node counts equal to RESULT.json (155,724,508 nodes)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "10,10:249:251", + "--workers", + "4" + ], + "timeout_seconds": 150, + "checks": "Fresh length-22 census of cover entries [249,251) of split (10,10): every shard complete with zero hits and per-shard node counts equal to RESULT.json (159,403,932 nodes)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--replay", + "10,7:0:251", + "--replay", + "11,6:0:251", + "--workers", + "4" + ], + "timeout_seconds": 60, + "checks": "Fresh length-22 census of cover entries [0,251) of split (10,7): every shard complete with zero hits and per-shard node counts equal to RESULT.json (700,909 nodes). Fresh length-22 census of cover entries [0,251) of split (11,6): every shard complete with zero hits and per-shard node counts equal to RESULT.json (2,247 nodes)." + } + ], + "notes": "C11 compiler with unsigned __int128 required (clang or GCC). No Python dependencies. CI replays the registered cover slices only (about 1.2e9 of 1.74e11 nodes; a first CI run showed a 2e9-node slice exceeding 150 s on the hosted runner); every split was run in full locally, and '--replay S,T' with the default range replays a whole split (opt-in). Local timings on CPython 3.12 with 4 workers (Apple silicon, shared machine): (10,9) full split 121 s, (11,11) slice 46 s, control about 40 s, receipt check under 1 s. Timing fields are excluded from all equality checks." +} diff --git a/research/f7-l22-deep-shard-census/deep_census.py b/research/f7-l22-deep-shard-census/deep_census.py new file mode 100644 index 0000000000..ad98072738 --- /dev/null +++ b/research/f7-l22-deep-shard-census/deep_census.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Run length-22 seven-label split censuses over a prefix-free shard cover. + +The engine is the merged union-budget engine of research/f7-l22-union-census, +used unchanged. The cover is every restricted-growth prefix of length six, +except that 012345 (the only one with six distinct labels, and by far the +heaviest subtree) is replaced by its restricted-growth extensions of length +eight. Every canonical length-22 word has exactly one prefix in the cover, so +running the engine once per cover prefix covers exactly the tree of one +unsharded run. Shard node counts are raw per-shard counts: nodes above a +shard's prefix are counted once per descendant shard, so the raw sum is +compared only with sums over the same cover. + +Engine outputs are kept in --work. A shard whose complete engine output is +already there is reused, so an interrupted run resumes without recomputation. +""" +import argparse +import concurrent.futures +import hashlib +import json +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +ENGINE = ROOT / "research/f7-l22-union-census/engine/union_census.c" +LABELS = 7 +LENGTH = 22 +DEPTH = 6 +EXPANDED = {"012345": 8} + + +def extensions(prefix, depth, labels=LABELS): + """Restricted-growth extensions of prefix to the given depth, in order.""" + if len(prefix) == depth: + return [prefix] + used = max((int(c) for c in prefix), default=-1) + 1 + out = [] + for label in range(min(used + 1, labels)): + out += extensions(prefix + str(label), depth, labels) + return out + + +def prefixes(depth=DEPTH, labels=LABELS): + """All restricted-growth prefixes of the given depth, in order.""" + return extensions("", depth, labels) + + +def cover(): + """The prefix-free shard cover used by RESULT.json.""" + out = [] + for key in prefixes(): + out += extensions(key, EXPANDED[key]) if key in EXPANDED else [key] + return out + + +def engine_sha256(): + return hashlib.sha256(ENGINE.read_bytes()).hexdigest() + + +def build(directory): + binary = Path(directory) / "union_census_l22" + cmd = ["cc", "-O3", "-Wall", "-Wextra", "-Werror", "-std=c11", + f"-DN={LABELS}", f"-DL={LENGTH}", str(ENGINE), "-o", str(binary)] + subprocess.run(cmd, check=True) + return binary + + +def read_shard(split, shard, directory): + """Parse one engine output; None if absent or incomplete.""" + hits = Path(directory) / f"hits_{split[0]}_{split[1]}_{shard}.txt" + data = Path(directory) / f"result_{split[0]}_{split[1]}_{shard}.json" + if not (hits.exists() and data.exists()) or data.stat().st_size == 0: + return None + payload = json.loads(data.read_text()) + total = payload["total"][0] + if (payload["split"] != list(split) or payload["requested_shards"] != 1 + or payload["shards"][0]["prefix"] != shard): + raise RuntimeError(f"{data} does not belong to shard {shard}") + return {"prefix": shard, "complete": payload["complete"] is True, + "nodes": total["nodes"], "hits": total["hits"], + "candidate_restored_leaves": total["candidate_restored_leaves"], + "hit_words": hits.read_text().split()} + + +def run_shard(binary, split, shard, directory): + row = read_shard(split, shard, directory) + if row is not None and row["complete"]: + return row + hits = Path(directory) / f"hits_{split[0]}_{split[1]}_{shard}.txt" + data = Path(directory) / f"result_{split[0]}_{split[1]}_{shard}.json" + for path in (hits, data): + if path.exists(): + path.unlink() + proc = subprocess.run([str(binary), f"{split[0]},{split[1]}", "--hits", + str(hits), "--json", str(data), shard], + capture_output=True, text=True) + row = read_shard(split, shard, directory) + if row is None: + raise RuntimeError(f"shard {shard} wrote no output: {proc.stderr[-500:]}") + row["complete"] = row["complete"] and proc.returncode == 0 + return row + + +def run_split(binary, split, workers, directory, shards): + # Heaviest subtrees first: more distinct labels in the prefix run longer. + order = sorted(shards, key=lambda k: -len(set(k))) + with concurrent.futures.ThreadPoolExecutor(max_workers=workers) as pool: + rows = dict(zip(order, pool.map( + lambda s: run_shard(binary, split, s, directory), order))) + return [rows[k] for k in shards] + + +def summarize(split, rows): + return {"split": list(split), "shards": len(rows), + "complete": all(r["complete"] for r in rows), + "nodes": sum(r["nodes"] for r in rows), + "hits": sum(r["hits"] for r in rows), + "hit_words": sorted(w for r in rows for w in r["hit_words"]), + "per_shard_nodes": {r["prefix"]: r["nodes"] for r in rows}} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--split", action="append", required=True, + help="S,T; may repeat") + parser.add_argument("--workers", type=int, default=os.cpu_count() or 4) + parser.add_argument("--work", type=Path, + help="directory for engine outputs (enables resume)") + parser.add_argument("--output", type=Path) + args = parser.parse_args() + keys = cover() + out = {"engine": str(ENGINE.relative_to(ROOT)), + "engine_sha256": engine_sha256(), "base_depth": DEPTH, + "expanded": EXPANDED, "cover_size": len(keys), "splits": []} + with tempfile.TemporaryDirectory(prefix="l22deep-") as tmp: + work = args.work or Path(tmp) + work.mkdir(parents=True, exist_ok=True) + binary = build(tmp) + for text in args.split: + split = tuple(int(x) for x in text.split(",")) + summary = summarize(split, run_split(binary, split, args.workers, + work, keys)) + out["splits"].append(summary) + print(json.dumps({k: summary[k] for k in + ("split", "shards", "complete", "nodes", "hits")}), + flush=True) + text = json.dumps(out, indent=1, sort_keys=True) + "\n" + if args.output: + args.output.write_text(text) + ok = all(s["complete"] and s["hits"] == 0 for s in out["splits"]) + return 0 if ok else 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/f7-l22-deep-shard-census/verify.py b/research/f7-l22-deep-shard-census/verify.py new file mode 100644 index 0000000000..8f3b0e68ff --- /dev/null +++ b/research/f7-l22-deep-shard-census/verify.py @@ -0,0 +1,234 @@ +#!/usr/bin/env python3 +"""Verify the prefix-cover sharded length-22 seven-label split census. + +Modes: + --check-receipt RESULT.json structure, engine pin, cover partition, + totals, and the split-domain closure arithmetic. + --control Partition control: on small compiled domains with real + universal words, mixed-depth cover sharding reproduces the + unsharded engine's hit set exactly on every split. + --replay S,T[:A:B] (repeatable) + Fresh census of cover entries [A,B) of split (S,T), default + the whole cover; per-shard node counts, zero hits and + completion must equal RESULT.json. +""" +import argparse +import concurrent.futures +import hashlib +import itertools +import json +import subprocess +import sys +import tempfile +import time +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +sys.path.insert(0, str(PACKAGE)) +import deep_census # noqa: E402 + +PREDECESSOR = ROOT / "research/f7-l22-union-census/RESULT.json" +# The eleven splits (s >= t) admitted at length 22 by the four necessary +# conditions of research/f7-l22-split-domain, before its 17-point import. +DOMAIN = [(11, 11), (11, 10), (11, 9), (10, 10), (11, 8), (10, 9), (11, 7), + (10, 8), (9, 9), (11, 6), (10, 7)] +SEVENTEEN_POINT = {(11, 6), (10, 7)} + + +def fail(message): + raise SystemExit(f"FAIL: {message}") + + +def pinned_engine_sha256(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["path"] == str(deep_census.ENGINE.relative_to(ROOT)): + return row["sha256"] + fail("engine is not pinned in SOURCES.json") + + +def check_cover(keys, labels): + """Every restricted-growth word of the cover's maximum depth has exactly + one prefix in the cover (prefix-free and complete).""" + depth = max(len(k) for k in keys) + if len(set(keys)) != len(keys): + fail("duplicate cover prefix") + for word in deep_census.extensions("", depth, labels): + if sum(word.startswith(k) for k in keys) != 1: + fail(f"cover is not a partition at {word}") + + +def mixed_cover(labels): + """Depth-six prefixes with the most-distinct-label prefix expanded to + depth eight: the same construction as deep_census.cover().""" + base = deep_census.prefixes(depth=6, labels=labels) + heavy = max(base, key=lambda k: (len(set(k)), k)) + out = [] + for key in base: + out += deep_census.extensions(key, 8, labels) if key == heavy else [key] + return out + + +def check_receipt(): + result = json.loads((PACKAGE / "RESULT.json").read_text()) + engine_hash = deep_census.engine_sha256() + if engine_hash != pinned_engine_sha256(): + fail("engine bytes differ from the SOURCES.json pin") + if result["engine_sha256"] != engine_hash: + fail("RESULT.json engine hash differs from the engine") + keys = deep_census.cover() + check_cover(keys, labels=7) + for mutant in (keys[:-1], keys + ["0123456"]): + try: + check_cover(mutant, labels=7) + except SystemExit: + continue + fail("a mutated cover passed the partition check") + if len(keys) != 251: + fail("cover is not the 202 depth-six prefixes plus 49 extensions of 012345") + if result["cover_size"] != 251 or result["expanded"] != {"012345": 8}: + fail("receipt cover metadata") + closed = {} + for split in result["splits"]: + s, t = split["split"] + if list(split["per_shard_nodes"]) != keys: + fail(f"{s},{t}: shard keys differ from the restricted-growth list") + if split["shards"] != 251 or not split["complete"]: + fail(f"{s},{t}: incomplete") + if split["hits"] != 0 or split["hit_words"]: + fail(f"{s},{t}: hits recorded") + if sum(split["per_shard_nodes"].values()) != split["nodes"]: + fail(f"{s},{t}: node total") + closed[(s, t)] = split["nodes"] + predecessor = json.loads(PREDECESSOR.read_text()) + prior_complete = {tuple(p["split"]) for p in predecessor["probes"] + if p["complete"] and p["hits"] == 0} + prior_open = {tuple(p["split"]) for p in predecessor["probes"] + if not p["complete"]} + if prior_open | SEVENTEEN_POINT != set(closed) - prior_complete: + fail(f"closed splits {sorted(closed)} do not match the predecessor's " + f"capped splits {sorted(prior_open)}") + remaining = [d for d in DOMAIN if d not in closed and d not in prior_complete] + for (s, t), nodes in sorted(closed.items()): + print(f"split ({s},{t}): 251 shards complete, hits 0, nodes {nodes:,}") + print(f"length-22 domain splits still open: {remaining}") + if remaining: + fail("domain not closed") + print("PASS_F7_L22_DEEP_SHARD_RECEIPT closed_domain=11_of_11") + + +def control(): + """Compile small (N,L) engines and compare unsharded and sharded hit sets.""" + total_hits = 0 + rows = 0 + mutations = 0 + with tempfile.TemporaryDirectory(prefix="l22deep-control-") as tmp: + for n, length in ((4, 8), (4, 10), (5, 12)): + binary = Path(tmp) / f"engine_{n}_{length}" + subprocess.run(["cc", "-O3", "-Wall", "-Wextra", "-Werror", + "-std=c11", f"-DN={n}", f"-DL={length}", + str(deep_census.ENGINE), "-o", str(binary)], + check=True) + keys = mixed_cover(n) + check_cover(keys, labels=n) + for s, t in itertools.product(range(1, length // 2 + 1), repeat=2): + whole = _run(binary, (s, t), [], tmp, f"w{n}{length}") + with concurrent.futures.ThreadPoolExecutor(8) as pool: + parts = list(pool.map( + lambda k: _run(binary, (s, t), [k], tmp, f"p{n}{length}"), + keys)) + if whole is None: + if any(p is not None for p in parts): + fail(f"N={n} L={length} ({s},{t}) shard-only output") + continue + if not (whole[0] and all(p[0] for p in parts)): + fail(f"N={n} L={length} ({s},{t}) incomplete") + words = sorted(w for p in parts for w in p[1]) + if sorted(whole[1]) != words: + fail(f"N={n} L={length} ({s},{t}) sharded hit set differs") + # Mutation: omitting any one hit-bearing prefix must be detected. + for k, p in zip(keys, parts): + if p[1]: + dropped = sorted(w for q in parts if q is not p for w in q[1]) + if dropped == sorted(whole[1]): + fail("dropped-prefix mutation not detected") + mutations += 1 + break + total_hits += len(words) + rows += 1 + if total_hits == 0: + fail("control has no positive universal words") + print(f"control: {rows} small splits, {total_hits} universal words, " + f"sharded hit sets equal unsharded; {mutations} dropped-prefix " + "mutations detected") + if mutations == 0: + fail("no mutation control ran") + print("PASS_F7_L22_DEEP_SHARD_CONTROL") + + +_counter = itertools.count() + + +def _run(binary, split, shards, tmp, tag): + index = next(_counter) + hits = Path(tmp) / f"{tag}_{index}.hits" + data = Path(tmp) / f"{tag}_{index}.json" + proc = subprocess.run([str(binary), f"{split[0]},{split[1]}", "--hits", + str(hits), "--json", str(data), *shards], + capture_output=True, text=True) + if proc.returncode == 1 and not data.exists(): + return None + payload = json.loads(data.read_text()) + return (payload["complete"] is True and proc.returncode == 0, + hits.read_text().split()) + + +def replay(text, workers): + split_text, _, bounds = text.partition(":") + first, last = (int(x) for x in bounds.split(":")) if bounds else (0, 251) + s, t = (int(x) for x in split_text.split(",")) + result = json.loads((PACKAGE / "RESULT.json").read_text()) + record = next(r for r in result["splits"] if r["split"] == [s, t]) + keys = deep_census.cover()[first:last] + if not keys: + fail("empty prefix range") + if deep_census.engine_sha256() != pinned_engine_sha256(): + fail("engine bytes differ from the SOURCES.json pin") + with tempfile.TemporaryDirectory(prefix="l22deep-replay-") as tmp: + binary = deep_census.build(tmp) + start = time.monotonic() + rows = deep_census.run_split(binary, (s, t), workers, tmp, keys) + elapsed = time.monotonic() - start + for row in rows: + if not row["complete"] or row["hits"] or row["hit_words"]: + fail(f"({s},{t}) shard {row['prefix']} not a complete zero-hit run") + if row["nodes"] != record["per_shard_nodes"][row["prefix"]]: + fail(f"({s},{t}) shard {row['prefix']} nodes {row['nodes']} != " + f"{record['per_shard_nodes'][row['prefix']]}") + nodes = sum(r["nodes"] for r in rows) + print(f"({s},{t}) prefixes [{first},{first + len(keys)}): {len(keys)} " + f"shards complete, hits 0, nodes {nodes:,} equal RESULT.json " + f"({elapsed:.1f} s, not compared)") + print("PASS_F7_L22_DEEP_SHARD_REPLAY") + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--check-receipt", action="store_true") + parser.add_argument("--control", action="store_true") + parser.add_argument("--replay", action="append", default=[]) + parser.add_argument("--workers", type=int, default=4) + args = parser.parse_args() + if args.check_receipt: + check_receipt() + if args.control: + control() + for text in args.replay: + replay(text, args.workers) + if not (args.check_receipt or args.control or args.replay): + parser.error("choose a mode") + + +if __name__ == "__main__": + main()