diff --git a/research/f7-set-word-pruning-boundary/README.md b/research/f7-set-word-pruning-boundary/README.md new file mode 100644 index 0000000000..2cab2ebb47 --- /dev/null +++ b/research/f7-set-word-pruning-boundary/README.md @@ -0,0 +1,232 @@ +# Separate set-cover pruning from word-census exclusions + +**Scoped source audit and finite certificate; no new f(7) bound or kappa.** + +The retained PR2542 `joint_covers` has two interface traps. Its split sizes +refer to **coordinate bit 0**, despite a docstring saying weight parity. +Its optional degree-two filter is exact as a set predicate, but the stated +justification that every minimum-length universal word is Hamiltonian is false: +the minimum-length three-label word `010122` has a degree-one prefix vertex. + +The actual-size set enumerator agrees with a separate unpruned subset oracle +in all 200 split/filter domains over dimensions 1–4. This checks, on the +actual function, the scope that Nicholas Stone's +[PR2973 parity correction](../f7-weight-parity-census-correction/README.md) +states in its MATH.md section 4: +the old **word** exclusions need replacement evidence, while this set-level +enumerator is not refuted merely for using bit 0. Four pinned set-search +call sites leave the optional degree filter disabled. No additional false +seven-label exclusion is inferred from the new degree counterexample. + +This is an independent audit of an adjacent contract. PR2973 already gives +`01021323`, corrected budgets and source-impact prose; James Reed's +[PR3096 audit](../f7-bit0-false-prune/README.md) already checks small words; +[Nick Petalas's PR3005](../f7-union-support-audit/README.md) already supplies a +separate complete seven-label word implementation. None is rerun at full +seven-label scale here. The contribution is the actual set-interface check, +the degree-filter counterexample, and the precise separation of dependencies. + +## The counterexamples and their scope + +### Minimum length does not justify minimum degree two + +In the singleton prefix-walk model, `010122` traces + +``` +0, 1, 3, 2, 0, 4, 0. +``` + +Each of three labels occurs twice, so it restores. Its distinct prefix set +`P={0,1,2,3,4}` covers all eight masks: `{0,1,2,3}` covers the lower two +coordinates, and its XORs with `4` give `{4,5,6,7}`. Every restored word +using all three labels has length at least six, because every label must +occur a positive even number of times. Thus this length-six word is minimal. +Vertex `4` has only neighbor `0` in the induced cube graph. The actual call +`joint_covers(3, [(3,2)])` returns 18 covers including `P`; enabling +`require_min_degree=True` returns none. + +This refutes the general minimum-length justification in the retained +`joint_covers` docstring. It does **not** refute the predicate itself, or its +use after proving a simple cycle of length at least four is required. If a +closed word has `|P|=L>=4`, all its nonclosing prefix states are distinct, +and every vertex has two distinct cycle neighbors. The hypothesis `|P|=L` +cannot be replaced by minimum word length. The two-vertex closed walk is +also excluded from that simple-cycle implication. + +`010122` is the predecessor's reflected-Gray construction at three labels; +the construction and minimum-length observation are not claimed as new. +The finding is its use against this particular retained interface claim. + +### Weight parity is not the actual `joint_covers` partition + +Reconstructing PR2973's `01021323` gives + +``` +0, 1, 3, 2, 6, 4, 12, 8, 0. +``` + +Its eight distinct states cover all 16 masks. Weight parity gives sizes +`(4,4)` and within-side collision excess zero; bit 0 gives `(6,2)` and +excess eight. The balanced budget is five, whereas the actual-size bit-0 +budget is nine. Calling the pinned old `cyclic_census` on this forced word +returns one hit with no budget or budget nine, and zero with budget five. +This directly corroborates the known false prune, without a seven-label +counterexample. The actual `joint_covers(4,[(6,2)])` contains its prefix +set; `joint_covers(4,[(4,4)])` does not. The latter call describes a different +set domain, rather than a failed enumeration of the former domain. + +A linear coordinate change cannot silently repair the word interface, as +PR2973's MATH.md section 4 also notes; here is an explicit witness. Define +`T(x)` by replacing bit 0 by the weight parity of `x` and retaining +all other bits. It is an invertible linear map, so it preserves XOR coverage +and takes the original weight split to an actual bit-0 split. But it maps +`e_i` to `e_i+e_0` for `i>0`, changing the singleton-step alphabet. +For the eight-state witness it gives +`T(P)={0,1,2,3,5,6,9,12}`, whose vertex `12` is isolated in the *original* +cube graph. The source filter accordingly rejects it. A transported word +must use the transported adjacency relation; testing the original relation +after this map is unjustified. + +## Why the actual-size set pruning survives this objection + +Fix a nonzero linear functional, here `ell(x)=x&1`, and actual final sizes +`s,t` in its two classes. Put `Q=2^(n-1)`. If the set covers the whole group, +the union of its two within-class pair supports has size `Q-1`. Hence the +sum of the separate collision excesses satisfies + +``` +coll <= C(s,2) + C(t,2) - (Q-1). +``` + +This is the budget used by `joint_covers`. When a new distinct point is +added to one class, its XORs with the existing points in that class are +distinct. The number already in the old support is exactly the increment +in collision excess. Thus `coll` is monotone, and exceeding the final +actual-size budget cannot discard a covering completion. + +At current sizes `e,o`, at most `s*t-e*o` new cross pairs and +`C(s,2)+C(t,2)-C(e,2)-C(o,2)` new within-class pairs remain. Each pair can +cover at most one previously missing mask, which justifies the two remaining +capacity prunes. The state saves and restores the affected support, collision +count and both coverage unions at each branch. + +Every zero-containing set with the stated actual sizes has one increasing +ordering of its nonzero points. At each step exactly the branch for that +point's bit-0 class can choose it. Conversely each finished branch is one +such set. Exact union coverage is checked at leaves. This gives the written +completeness argument for valid integer inputs `n>=1`, `1<=s<=Q`, `0<=t<=Q`, +with an uncapped run and no degree filter. With the filter, completeness is +for covers additionally satisfying the degree predicate, not for arbitrary +minimal words. A reached node cap raises `OverflowError`, which this audit +requires to remain a failure rather than a zero-hit result. + +The argument does not substitute `s=t=L/2`. Time parity bounds the sizes of +the **weight** classes of a closed singleton word, not its bit-0 classes. +That substitution is the separate error in the old word engine. + +## Executed finite check and dependency boundary + +The direct oracle visits every subset containing zero and computes all +pairwise XORs without a collision or capacity prune. For each actual bit-0 +split it compares the complete returned set collection, including duplicates +and partition labels, with `joint_covers`, with the degree filter both off +and on. It also checks that the separate `set_level_splits` selector retains +every observed covering split. Empty splits and zero-hit domains are included. + +| Dimension | All zero-containing sets | Covers | Covers with minimum degree two | +|---:|---:|---:|---:| +| 1 | 2 | 1 | 0 | +| 2 | 8 | 4 | 1 | +| 3 | 128 | 64 | 20 | +| 4 | 32,768 | 23,552 | 5,074 | + +The total is **32,906 sets and 200 exact domain comparisons**. Every domain +has a count and canonical returned-set SHA256 in [RESULT.json](RESULT.json). +During this enumeration the subject's `cyclic_census` is replaced in memory +by a function that raises immediately, making accidental use a failure. +The PR2542 engine, PR2634 copy and PR2773 vendor copy are byte-identical, +SHA256 `82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4`. +One execution therefore audits those shared bytes, rather than claiming +three independent implementations. + +The source-bound call-site inventory covers six named Python files, plus +PR2691's native rule. It is not a whole-repository dependency proof. + +| Predecessor evidence | Consequence of the audited premise | +|---|---| +| PR2542 `search.py` and `verify.py`, L18, `budget=9`, `simple=True` | Two word calls apply the invalid bit-0/balanced budget. Their old zero-hit receipts cannot justify exclusion; use separate corrected exclusion evidence. | +| PR2634 `verify.py`, full and sharded L18 replay | Two calls repeat the same invalid premise. Reproducing the historical counters does not repair it. | +| PR2634 `census20.py`, L20, `budget=27`, `simple=True` | Its partial simple-cycle traversal is not a complete exclusion of the claimed word class. | +| PR2691 `f7_census.c`, `BUDGET=27`, grouping by `nq&1` | Its 15-shard completion inherits the same unsound rule; the old 6,305,209,079-node receipt remains historical filter evidence. No new native replay is performed here. | +| PR2773 `verify.py`, sharded L18 replay | One more call repeats the invalid historical word evidence. That invocation is separate from the set-level computations below. | +| Four PR2542 set-search calls in `search.py`, `verify.py`, `test_engine.py` | All use the default degree flag `False`; their n=5 size-10 controls use the set-level split selector. Neither the bit-0 choice nor the new degree counterexample refutes these calls. The full n=5 controls were not rerun. | +| PR2773 `cover17.py` and `search17.py` | Both import only standard-library modules and use their own set routines. Fresh calculations reproduce empty rows for `(9,8)/(8,9)` and, conditional on the separately recorded excess floors, `(10,7)/(7,10)`. They leave two rows for each `(11,6)/(6,11)` orientation. This reproduces the retained arithmetic without the word engine; the large Sidon floor censuses were not rerun or newly validated. | + +PR2973 and PR3005 provide **replacement** word-exclusion evidence in their +own packages. They do not make the old prune valid. Their complete n=7 +receipts and resulting `22<=f(7)<=24` claim are not revalidated by this +small-domain check. Later Fourier/set-level results must retain their own +hypotheses; this audit neither revokes nor independently certifies them. +No selected-result file or frozen predecessor is changed. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -I -B research/f7-set-word-pruning-boundary/verify.py +python3 -I -B research/f7-set-word-pruning-boundary/test_verify.py -v +python3 scripts/research_package.py --package research/f7-set-word-pruning-boundary --check-only +python3 scripts/research_package.py --package research/f7-set-word-pruning-boundary +``` + +Expected marker: +`PASS_F7_SET_WORD_BOUNDARY sets=32906 comparisons=200 degree_counterexample=010122 no_new_kappa`. +The tests exercise the actual counterexamples, a balanced-size budget mutant, +node-cap failure, changed source bytes, wrong partition labels, duplicate +results, a newly enabled degree-filter caller, and missing/changed receipt +fields. The verifier uses explicit checks under `-O`; `--emit` prints a +fresh receipt and does not overwrite files. Loaded source is authenticated +and compiled from bytes, without importing a predecessor bytecode cache. + +[SOURCES.json](SOURCES.json) pins the base and all live inputs. +[TASK.json](TASK.json) records the refined revision-6 `census-pruning-audit` +scope, predecessor heads, overlap and remaining obligations. The base is +`463113d675af7410ac91d53a4fed51ec6494eb9a`. The claim is in +[discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19001818). +This is author-checked executable +and written evidence with a separately implemented oracle; no independent +human review, proof-assistant verification, hosted CI success, full supplier +replay or theorem admission is claimed. + +## Open next questions + +1. **Should a maintained successor expose separate set-cover and simple-cycle + APIs?** The new counterexample shows why a minimum-length description is + insufficient. First define a `simple cycle, |P|=L>=4` contract, preserve + the actual bit-0 split meaning, and carry these witnesses into its tests. + This is an interface decision; frozen predecessor files must stay pinned. +2. **Which historical entry points should point to replacement evidence?** + The six Python calls and one native rule above identify a bounded target + for an annotation or successor entry point. First decide whether a caller + intends historical counter reproduction or a mathematical exclusion. + Independent scientific review of the corrected n=7 receipts remains a + separate obligation; this package does not reopen the completed independent + implementation task or launch a length-22 search. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Ross Richardson supplied the PR943 singleton prefix-walk model. Aaron Wang +supplied PR2542/PR2634's word and set engines, reflected-Gray construction, +and PR2773's set-level audit. Nicholas Stone supplied PR2691's C traversal +and PR2973's parity correction and `01021323` counterexample. Nick Petalas +supplied PR3005's independent union-support word census, and James Reed +(@jwr404) supplied PR3096's earlier tiny false-prune audit. Douglas Colkitt +supplied the retained project and contribution framework. This package adds +the particular degree-contract counterexample, set-interface oracle and +dependency audit; it claims no priority over those constructions or the +corrected f(7) bound. OpenAI Codex assisted substantially with derivation, +implementation, checking and writing. No independent human review is +claimed. Apache-2.0. diff --git a/research/f7-set-word-pruning-boundary/RESULT.json b/research/f7-set-word-pruning-boundary/RESULT.json new file mode 100644 index 0000000000..7e4f4e3518 --- /dev/null +++ b/research/f7-set-word-pruning-boundary/RESULT.json @@ -0,0 +1,2131 @@ +{ + "all_sets": 32906, + "controls": { + "balanced_size_mutant_rejected": true, + "cap_raises": true, + "degree_filter_counterexample_detected": true, + "linear_map_adjacency_loss_detected": true, + "partition_misinterpretation_rejected": true + }, + "exact_domain_comparisons": 200, + "kind": "scoped_source_audit_and_finite_certificate", + "schema_version": 1, + "small_domain": [ + { + "all_sets": 2, + "cases": [ + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "f515fa775d99acd6f31a0b7f0a698ebf3bb5052eb031c28e49b7b81b7ad53b6a", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + } + ], + "covers": 1, + "degree_two_covers": 0, + "n": 1 + }, + { + "all_sets": 8, + "cases": [ + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "8aa979662480431ff672da659c1a38c1760d2eff12f903b442ec270aee4196b1", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 2, + "minimum_degree_two": false, + "sets_sha256": "d2e48164181367aef6a64ff681f96d02165444d4e54922f76121238e5c5ab7e0", + "split": [ + 2, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 1 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "24d62856bfcf1370a5afefd9c5686c620ab4194469cd4b98405aa627030b7d70", + "split": [ + 2, + 2 + ] + }, + { + "covers": 1, + "minimum_degree_two": true, + "sets_sha256": "24d62856bfcf1370a5afefd9c5686c620ab4194469cd4b98405aa627030b7d70", + "split": [ + 2, + 2 + ] + } + ], + "covers": 4, + "degree_two_covers": 1, + "n": 2 + }, + { + "all_sets": 128, + "cases": [ + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 3 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "32e48d94be6693fe95faced68898a8de09bce657ba81188ca81978fad421f8e0", + "split": [ + 1, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 2 + ] + }, + { + "covers": 12, + "minimum_degree_two": false, + "sets_sha256": "b3353a36ff8ae7bf47d369ef79915bbc403223163078fcbc05666adf5f717c7d", + "split": [ + 2, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 3 + ] + }, + { + "covers": 3, + "minimum_degree_two": false, + "sets_sha256": "7aa763246cabfde3dac002fd0fb48fa0013a4417f6026c7c537f52b701c0a7d1", + "split": [ + 2, + 4 + ] + }, + { + "covers": 2, + "minimum_degree_two": true, + "sets_sha256": "eaba8fadf152bfbfce3d435d4c192cb991448620cc94a457b16fb8449c64e1a2", + "split": [ + 2, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 1 + ] + }, + { + "covers": 18, + "minimum_degree_two": false, + "sets_sha256": "d4d3e4d5502b1b8f2579ace15be48f7dea2a90fc01dd019f69725040932a9996", + "split": [ + 3, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 2 + ] + }, + { + "covers": 12, + "minimum_degree_two": false, + "sets_sha256": "dcb79c36939e06efe5bbbb10bdd719e551f4a22e674c451e2f1e350a612b4868", + "split": [ + 3, + 3 + ] + }, + { + "covers": 6, + "minimum_degree_two": true, + "sets_sha256": "fd25a6ddedca193f16f8059db0caa41f9b077f731ef198d0fdc719b985dec838", + "split": [ + 3, + 3 + ] + }, + { + "covers": 3, + "minimum_degree_two": false, + "sets_sha256": "92e40e3bd169861b5924295abcf14572092146bd6a789cd5d0c0b7e7e509f311", + "split": [ + 3, + 4 + ] + }, + { + "covers": 3, + "minimum_degree_two": true, + "sets_sha256": "92e40e3bd169861b5924295abcf14572092146bd6a789cd5d0c0b7e7e509f311", + "split": [ + 3, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 0 + ] + }, + { + "covers": 4, + "minimum_degree_two": false, + "sets_sha256": "2d08fcf441e096cd2578e12398d9fcc1ad383afc8078bbba7a1170a87e201a4f", + "split": [ + 4, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 1 + ] + }, + { + "covers": 6, + "minimum_degree_two": false, + "sets_sha256": "529053b459bbd198a3ef72c4c8804500096eb8794a4969158ee282cb2c3d092e", + "split": [ + 4, + 2 + ] + }, + { + "covers": 4, + "minimum_degree_two": true, + "sets_sha256": "e19e6cf15a6d0cfc719b5af914b22c01a4b1cc4e20ff200f28c723036fdcc1f0", + "split": [ + 4, + 2 + ] + }, + { + "covers": 4, + "minimum_degree_two": false, + "sets_sha256": "83ce3d5dcd6a048572d3cbf31b8469c645380bbf8963de7e711bca97e6b08706", + "split": [ + 4, + 3 + ] + }, + { + "covers": 4, + "minimum_degree_two": true, + "sets_sha256": "83ce3d5dcd6a048572d3cbf31b8469c645380bbf8963de7e711bca97e6b08706", + "split": [ + 4, + 3 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "5474ed11ed33173f19112c31bf7a8f49eb7a51cf44b278283bc07a180123fd03", + "split": [ + 4, + 4 + ] + }, + { + "covers": 1, + "minimum_degree_two": true, + "sets_sha256": "5474ed11ed33173f19112c31bf7a8f49eb7a51cf44b278283bc07a180123fd03", + "split": [ + 4, + 4 + ] + } + ], + "covers": 64, + "degree_two_covers": 20, + "n": 3 + }, + { + "all_sets": 32768, + "cases": [ + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 5 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 5 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 6 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 6 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 7 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 7 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "fc59f7be4dbabea9cdb50040b4641f099ce4af48e1003b4e239b90f70b035423", + "split": [ + 1, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 1, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 3 + ] + }, + { + "covers": 56, + "minimum_degree_two": false, + "sets_sha256": "9ea3e17da1f96a17bc670f0a1f56beda7678857bf238e74f4a1de50b8b6cb54f", + "split": [ + 2, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 2, + 4 + ] + }, + { + "covers": 224, + "minimum_degree_two": false, + "sets_sha256": "d3cbcb0c2b21d9be662a995411ed100dc8a569f516e23ea36167b760b0cebc74", + "split": [ + 2, + 5 + ] + }, + { + "covers": 6, + "minimum_degree_two": true, + "sets_sha256": "bd11b06c533329d4cb4da929fc90d43e5d38fd09c2719f248e355df45243909f", + "split": [ + 2, + 5 + ] + }, + { + "covers": 168, + "minimum_degree_two": false, + "sets_sha256": "d0bc1ade92139a664277be25dc90db4f64eaed0ed34c48080126d65857b769fd", + "split": [ + 2, + 6 + ] + }, + { + "covers": 18, + "minimum_degree_two": true, + "sets_sha256": "1a524ef41d1f4c0b495561f8afb986e4d2130f7399c90130ca510746f805b9ad", + "split": [ + 2, + 6 + ] + }, + { + "covers": 56, + "minimum_degree_two": false, + "sets_sha256": "002bbc87067dfef2c4450e38c7097b42b32ffdf5a38d7fbd958aad56c21b758a", + "split": [ + 2, + 7 + ] + }, + { + "covers": 18, + "minimum_degree_two": true, + "sets_sha256": "398d1300b898069295b5a694ce819c11fb852b7c285e08f06a4712c792d74079", + "split": [ + 2, + 7 + ] + }, + { + "covers": 7, + "minimum_degree_two": false, + "sets_sha256": "8f1d37850e8d0ee563c875a6078f4d6562f8034e53f61408b54851bc96fc2697", + "split": [ + 2, + 8 + ] + }, + { + "covers": 3, + "minimum_degree_two": true, + "sets_sha256": "7845561b0efba8fff1c3db7f4be3761c17d294c300caf1d960d97540ba6fc915", + "split": [ + 2, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 3 + ] + }, + { + "covers": 504, + "minimum_degree_two": false, + "sets_sha256": "19635a3daeee09c04d0ac4969407913d98e8bf756ab04938bfb04b1e650d2ab2", + "split": [ + 3, + 4 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 3, + 4 + ] + }, + { + "covers": 1008, + "minimum_degree_two": false, + "sets_sha256": "13ef98253840650fefae0694e3e829e219b21ffc7f40089b18e0a538674f2a30", + "split": [ + 3, + 5 + ] + }, + { + "covers": 54, + "minimum_degree_two": true, + "sets_sha256": "c11733cbd4abbf1dea35ae1011fb4585e3ee3a9bae2b89a6cae70a02a5ba674e", + "split": [ + 3, + 5 + ] + }, + { + "covers": 588, + "minimum_degree_two": false, + "sets_sha256": "018555c2e6be9c9d06b690143c86a721a6c8daa33c02a3b4c7af42649cc6bce7", + "split": [ + 3, + 6 + ] + }, + { + "covers": 81, + "minimum_degree_two": true, + "sets_sha256": "ab872b5eb2a2f5b5a1d32dbf7ec9ca60fc8abd5fe4a16a3b457c4baeb01e0046", + "split": [ + 3, + 6 + ] + }, + { + "covers": 168, + "minimum_degree_two": false, + "sets_sha256": "07b0c246d878cab75923a36042e5d9609611765ecf06e170136507ea69584fb6", + "split": [ + 3, + 7 + ] + }, + { + "covers": 54, + "minimum_degree_two": true, + "sets_sha256": "82e36069050e5dba36003b9ae7d180dc434ec86d7fdea6399376b6312e0216e9", + "split": [ + 3, + 7 + ] + }, + { + "covers": 21, + "minimum_degree_two": false, + "sets_sha256": "c1f51a7a5947f0f27fe7124d901f2213d55883afd0bac959ac85958bb1e736b1", + "split": [ + 3, + 8 + ] + }, + { + "covers": 9, + "minimum_degree_two": true, + "sets_sha256": "60c286b918888a37a7994976a30e105f8498b3ae54e8a344367cff27067501b8", + "split": [ + 3, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 1 + ] + }, + { + "covers": 112, + "minimum_degree_two": false, + "sets_sha256": "b0ab6c794dfc2f9633ef5cee912bb9134c62c80d6da1e89415eb4b6ee000ffb7", + "split": [ + 4, + 2 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 2 + ] + }, + { + "covers": 672, + "minimum_degree_two": false, + "sets_sha256": "01d2749dd64ccc0d61f779d7d04a138865bb28535ff3a9913d5dc05fad1830b1", + "split": [ + 4, + 3 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 4, + 3 + ] + }, + { + "covers": 1680, + "minimum_degree_two": false, + "sets_sha256": "f9aa98a1b6234d0e83ee98e2ac2586c0524563edbf836342dcabd8c5860fc823", + "split": [ + 4, + 4 + ] + }, + { + "covers": 48, + "minimum_degree_two": true, + "sets_sha256": "6c9207f8427f44474e6da859044471eac6071dc1f5f8092428d2c771fa40549e", + "split": [ + 4, + 4 + ] + }, + { + "covers": 1960, + "minimum_degree_two": false, + "sets_sha256": "07a033965d7a83ea31f5fb7ee17021492218a754fc5feb3ac8ba3e6d6d6775e9", + "split": [ + 4, + 5 + ] + }, + { + "covers": 204, + "minimum_degree_two": true, + "sets_sha256": "4cb8e6ddd8f31a3abce90d0d041400aeffa86cd6cdba730ede20e2075fe51f17", + "split": [ + 4, + 5 + ] + }, + { + "covers": 980, + "minimum_degree_two": false, + "sets_sha256": "b508c1550474a9bb7c331c61bf13e99c36a8cb571f5de9e47757f411c280cac5", + "split": [ + 4, + 6 + ] + }, + { + "covers": 232, + "minimum_degree_two": true, + "sets_sha256": "ac0b1121c6056a3cbf4d6f7155566f102aaf6ea7ce9cd7949c7faef2fc5f81e1", + "split": [ + 4, + 6 + ] + }, + { + "covers": 280, + "minimum_degree_two": false, + "sets_sha256": "5b352bdd3d8dac16bc789a29b1130db42dd32e71b2e973d68412d744da957312", + "split": [ + 4, + 7 + ] + }, + { + "covers": 128, + "minimum_degree_two": true, + "sets_sha256": "6e68581648f1b8d290544ceaa2a4be8a1e754ba88ee752d921df947bf0a42bc8", + "split": [ + 4, + 7 + ] + }, + { + "covers": 35, + "minimum_degree_two": false, + "sets_sha256": "a768d2331fa3a740e38c2ce404face27a9c4c7d286a74699b169910c58ac6c55", + "split": [ + 4, + 8 + ] + }, + { + "covers": 22, + "minimum_degree_two": true, + "sets_sha256": "991dcc789e79b054f524b09b61c171c1df23ef29561b969f62cafbe8e8d870f5", + "split": [ + 4, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 5, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 5, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 5, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 5, + 1 + ] + }, + { + "covers": 560, + "minimum_degree_two": false, + "sets_sha256": "69484f59b078b72ffc495cd9acf3eb668531f07b144aed9f26345669f0ab37bf", + "split": [ + 5, + 2 + ] + }, + { + "covers": 15, + "minimum_degree_two": true, + "sets_sha256": "ca57558e961620625456d506ca2fba88308dbbed40ceddb268c3e6e7d92d614b", + "split": [ + 5, + 2 + ] + }, + { + "covers": 1680, + "minimum_degree_two": false, + "sets_sha256": "4b677db1f76fc159435a68a8c212e567be426f3dc3754eea5375d590b3ad0588", + "split": [ + 5, + 3 + ] + }, + { + "covers": 90, + "minimum_degree_two": true, + "sets_sha256": "7a11d61a032de17dc3ba736c1d9bd588d7138c55723c1f96209c7a6d7267f20c", + "split": [ + 5, + 3 + ] + }, + { + "covers": 2450, + "minimum_degree_two": false, + "sets_sha256": "734906c9c20fd2a35329192bd14738651847d8cab6e462ef8437ff9a16f20a86", + "split": [ + 5, + 4 + ] + }, + { + "covers": 255, + "minimum_degree_two": true, + "sets_sha256": "fa517f25bbb04c933978ea25d5f0bc8d990e044caa76e20cd1184d449c7b79d0", + "split": [ + 5, + 4 + ] + }, + { + "covers": 1960, + "minimum_degree_two": false, + "sets_sha256": "6c3579f2e0e9dc03211e5a1fb8c805e45c36d26c4066ce2c3b1a276f21e5fa48", + "split": [ + 5, + 5 + ] + }, + { + "covers": 465, + "minimum_degree_two": true, + "sets_sha256": "03f799103e23d4d993c957898a7e3903ce5e00a18aca5b6dca699e33a7911ed9", + "split": [ + 5, + 5 + ] + }, + { + "covers": 980, + "minimum_degree_two": false, + "sets_sha256": "110e4d5eb12064e91583b23ac150f5d86f5553e600d2605617e8eb905ee8d86e", + "split": [ + 5, + 6 + ] + }, + { + "covers": 420, + "minimum_degree_two": true, + "sets_sha256": "067e5b94993b25a04647e0836745d8258e6feb2b530564a321a2c272d640206b", + "split": [ + 5, + 6 + ] + }, + { + "covers": 280, + "minimum_degree_two": false, + "sets_sha256": "f26f84b7fa55beb8af1614a0c28fb3f3886ada890e1d1eebe04a54fee107f130", + "split": [ + 5, + 7 + ] + }, + { + "covers": 195, + "minimum_degree_two": true, + "sets_sha256": "157ef7bf87b50d65ba7db188f9d49262d14ae1393738383a599810f1b503ed98", + "split": [ + 5, + 7 + ] + }, + { + "covers": 35, + "minimum_degree_two": false, + "sets_sha256": "a9eac7ccf7ce7f006edda6bbf0eca22f4c0aa760e77ac663a12dd68e4c2f7c04", + "split": [ + 5, + 8 + ] + }, + { + "covers": 30, + "minimum_degree_two": true, + "sets_sha256": "0360b9566a66147814c24f394758b1759831fd05db5044f5c05e5f5263b3dc34", + "split": [ + 5, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 6, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 6, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 6, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 6, + 1 + ] + }, + { + "covers": 504, + "minimum_degree_two": false, + "sets_sha256": "4c9750b17321339f736c184675227ddcd1ebaa741e531a79c3749380d20abfad", + "split": [ + 6, + 2 + ] + }, + { + "covers": 54, + "minimum_degree_two": true, + "sets_sha256": "bacd8cfb1c8ee3119b22a9dfc0c01c7f19998feb85929435ea98194e46f06ec7", + "split": [ + 6, + 2 + ] + }, + { + "covers": 1176, + "minimum_degree_two": false, + "sets_sha256": "bd119266c3b71986b4f415b738c7071334eca49b70ce49f9fa40abe51db5dae9", + "split": [ + 6, + 3 + ] + }, + { + "covers": 162, + "minimum_degree_two": true, + "sets_sha256": "93df15db9bd6a7617f2d3c9adc111b24e6bd46e31f686abd9e064125280340e0", + "split": [ + 6, + 3 + ] + }, + { + "covers": 1470, + "minimum_degree_two": false, + "sets_sha256": "3bc32babf30c5b30b77e9822b9e83fe86e5edf9978cfc636dfc3e822fd41538d", + "split": [ + 6, + 4 + ] + }, + { + "covers": 348, + "minimum_degree_two": true, + "sets_sha256": "9502b7f792630301adbeb253a9d4af44afa78b161d67755bf89a6cfac225d4a5", + "split": [ + 6, + 4 + ] + }, + { + "covers": 1176, + "minimum_degree_two": false, + "sets_sha256": "d938e27d6c35ca85eefafb549227c98a99beb6d8741303b0348b97e43200e1a7", + "split": [ + 6, + 5 + ] + }, + { + "covers": 504, + "minimum_degree_two": true, + "sets_sha256": "6f8aa41405ccf7531a341468ef0f573c6314d91e4bfca6f4b0cbe74700637301", + "split": [ + 6, + 5 + ] + }, + { + "covers": 588, + "minimum_degree_two": false, + "sets_sha256": "19f3b3c06e7dd1fbe209715099179196529f679e9b8d505105dc617ec91d6f46", + "split": [ + 6, + 6 + ] + }, + { + "covers": 399, + "minimum_degree_two": true, + "sets_sha256": "ff0061eb4efbd52c28c4f645c0938f56809d66f9b7d524013e5e9bc1136cc4c1", + "split": [ + 6, + 6 + ] + }, + { + "covers": 168, + "minimum_degree_two": false, + "sets_sha256": "642a47f735a52adbcaa82719c1b56a97bd0e8965bf61a8568851d518fa5d39d0", + "split": [ + 6, + 7 + ] + }, + { + "covers": 150, + "minimum_degree_two": true, + "sets_sha256": "b652cfa74a0601e5d6470a0a4c866f6702d214cfcb3fb266d8a5ef6523d41809", + "split": [ + 6, + 7 + ] + }, + { + "covers": 21, + "minimum_degree_two": false, + "sets_sha256": "5fec460c053d629cd9721ca2933dbfa743e0368ce103b16a126173e84e7298b3", + "split": [ + 6, + 8 + ] + }, + { + "covers": 21, + "minimum_degree_two": true, + "sets_sha256": "5fec460c053d629cd9721ca2933dbfa743e0368ce103b16a126173e84e7298b3", + "split": [ + 6, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 7, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 7, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 7, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 7, + 1 + ] + }, + { + "covers": 196, + "minimum_degree_two": false, + "sets_sha256": "39651b75174a9d65acc9e85c7d47140e10944412d6bfe42ad8e3bb69c7afcd0a", + "split": [ + 7, + 2 + ] + }, + { + "covers": 63, + "minimum_degree_two": true, + "sets_sha256": "540b730de7dc3b4d27e3e6ea706c6312c9eb522d57b8abea49c9032a3aaa56da", + "split": [ + 7, + 2 + ] + }, + { + "covers": 392, + "minimum_degree_two": false, + "sets_sha256": "a3c4f2b4b5158dc63cd336f0a68b44241d3043f19b492d9bc641e5f16be3ac90", + "split": [ + 7, + 3 + ] + }, + { + "covers": 126, + "minimum_degree_two": true, + "sets_sha256": "bb37521780fcc729fb67a56d62aca6dfd5f96fdeda0dd92f27af84950a28a01d", + "split": [ + 7, + 3 + ] + }, + { + "covers": 490, + "minimum_degree_two": false, + "sets_sha256": "c863e7020becb0914e655ad90284076ab195a8e17f870c4b8249a44580a4d288", + "split": [ + 7, + 4 + ] + }, + { + "covers": 224, + "minimum_degree_two": true, + "sets_sha256": "0c130dce417dc1075e8643b733cf60283b7ce41c3bca0b5d3edab9e1343c73b4", + "split": [ + 7, + 4 + ] + }, + { + "covers": 392, + "minimum_degree_two": false, + "sets_sha256": "ce224a2521f0244e411c93024bc092cfddc0cda022b42c71d37f18578011d135", + "split": [ + 7, + 5 + ] + }, + { + "covers": 273, + "minimum_degree_two": true, + "sets_sha256": "a17b5b5c0c42618afdbcd3242128b79d212a569518fa67dd6311b5a0da9c30cb", + "split": [ + 7, + 5 + ] + }, + { + "covers": 196, + "minimum_degree_two": false, + "sets_sha256": "656e57effb3766da046adcda2c0fe8e1d06059f10514fdd6067f4f6b51fbb149", + "split": [ + 7, + 6 + ] + }, + { + "covers": 175, + "minimum_degree_two": true, + "sets_sha256": "3c0a0f42a01bfba65ae1310fc381ce6bd7cef911ec2cff8f20f99e749cea9aaf", + "split": [ + 7, + 6 + ] + }, + { + "covers": 56, + "minimum_degree_two": false, + "sets_sha256": "5df278afde6d61689806862e0466988eac8c72c3d8ffdcc53b46cb7b936fbabe", + "split": [ + 7, + 7 + ] + }, + { + "covers": 56, + "minimum_degree_two": true, + "sets_sha256": "5df278afde6d61689806862e0466988eac8c72c3d8ffdcc53b46cb7b936fbabe", + "split": [ + 7, + 7 + ] + }, + { + "covers": 7, + "minimum_degree_two": false, + "sets_sha256": "e4705ea75cb2002405d1cae5ce528636179a5acfd06dcd5714bd4e6068ade694", + "split": [ + 7, + 8 + ] + }, + { + "covers": 7, + "minimum_degree_two": true, + "sets_sha256": "e4705ea75cb2002405d1cae5ce528636179a5acfd06dcd5714bd4e6068ade694", + "split": [ + 7, + 8 + ] + }, + { + "covers": 0, + "minimum_degree_two": false, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 8, + 0 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 8, + 0 + ] + }, + { + "covers": 8, + "minimum_degree_two": false, + "sets_sha256": "c36124c928e1bb2f67ed48f350e8b13c5f19ec7a100324bb54ce89e469f0b799", + "split": [ + 8, + 1 + ] + }, + { + "covers": 0, + "minimum_degree_two": true, + "sets_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "split": [ + 8, + 1 + ] + }, + { + "covers": 28, + "minimum_degree_two": false, + "sets_sha256": "926a2033ad29a270cb2e909f554add9f799fc592a68f94b874473a4e7c38204b", + "split": [ + 8, + 2 + ] + }, + { + "covers": 12, + "minimum_degree_two": true, + "sets_sha256": "27db57dcdb36488a06364e8c6ff41709ecd582760afc7dada6a4e523a5af4fe3", + "split": [ + 8, + 2 + ] + }, + { + "covers": 56, + "minimum_degree_two": false, + "sets_sha256": "e8e4784b884f91235467dc92a31cf4630cf27d9d5a340a0d7ebffa7d2d5338fb", + "split": [ + 8, + 3 + ] + }, + { + "covers": 24, + "minimum_degree_two": true, + "sets_sha256": "ee8396bf7330733717795ec99ef05ce3a8b4a5b0dad701b6b2ae9d18e5796157", + "split": [ + 8, + 3 + ] + }, + { + "covers": 70, + "minimum_degree_two": false, + "sets_sha256": "967f947ff42af271bb82b9ad6bc030b316eeb610a476f3af726b06296c680cb4", + "split": [ + 8, + 4 + ] + }, + { + "covers": 44, + "minimum_degree_two": true, + "sets_sha256": "decbcbd340b29bdd39927f43ba52418ccbeed127d3a307b9b1ce92c7055ae47b", + "split": [ + 8, + 4 + ] + }, + { + "covers": 56, + "minimum_degree_two": false, + "sets_sha256": "df7b9e5a2a1ceb747b3afd2dfc1721a90575aec48090130a0f25cfb52fb468ad", + "split": [ + 8, + 5 + ] + }, + { + "covers": 48, + "minimum_degree_two": true, + "sets_sha256": "50f5cadb74e8041fbd8e77537cff7dcd0b62d29972c234c51a422d7f0fcc8eb2", + "split": [ + 8, + 5 + ] + }, + { + "covers": 28, + "minimum_degree_two": false, + "sets_sha256": "b3092be8968a63eb3db9161f207317862b4e7f7805419b1012099341a9c604b9", + "split": [ + 8, + 6 + ] + }, + { + "covers": 28, + "minimum_degree_two": true, + "sets_sha256": "b3092be8968a63eb3db9161f207317862b4e7f7805419b1012099341a9c604b9", + "split": [ + 8, + 6 + ] + }, + { + "covers": 8, + "minimum_degree_two": false, + "sets_sha256": "2f87d897316dbb0e75403e2b2f78b06e371006e30195bd56ae2bb718e6732048", + "split": [ + 8, + 7 + ] + }, + { + "covers": 8, + "minimum_degree_two": true, + "sets_sha256": "2f87d897316dbb0e75403e2b2f78b06e371006e30195bd56ae2bb718e6732048", + "split": [ + 8, + 7 + ] + }, + { + "covers": 1, + "minimum_degree_two": false, + "sets_sha256": "edfb7d8565987f3a40cbdf3bc0ba4e9e975ef86fed31636c39f704789aac6b55", + "split": [ + 8, + 8 + ] + }, + { + "covers": 1, + "minimum_degree_two": true, + "sets_sha256": "edfb7d8565987f3a40cbdf3bc0ba4e9e975ef86fed31636c39f704789aac6b55", + "split": [ + 8, + 8 + ] + } + ], + "covers": 23552, + "degree_two_covers": 5074, + "n": 4 + } + ], + "source_impact": { + "calls": [ + { + "call": "pr2542_engine.cyclic_census(7, 18, budget=9, simple=True, prefix=pref)", + "kind": "invalid_word_budget", + "line": 61, + "path": "research/f7-17point-cover-audit-seedcfa215c2/verify.py" + }, + { + "call": "cyclic_census(7, 20, budget=27, simple=True, prefix=pref)", + "kind": "invalid_word_budget", + "line": 41, + "path": "research/universal-f7-singleton-l20-seed06704c39/census20.py" + }, + { + "call": "cyclic_census(7, 18, budget=9, simple=True, prefix=pref)", + "kind": "invalid_word_budget", + "line": 75, + "path": "research/universal-f7-singleton-l20-seed06704c39/verify.py" + }, + { + "call": "cyclic_census(7, 18, budget=9, simple=True)", + "kind": "invalid_word_budget", + "line": 83, + "path": "research/universal-f7-singleton-l20-seed06704c39/verify.py" + }, + { + "call": "joint_covers(5, splits10)", + "kind": "set_actual_sizes", + "line": 86, + "path": "research/universal-f7-singleton-seedb859517b/search.py" + }, + { + "call": "cyclic_census(7, 18, budget=9, simple=True, prefix=pref)", + "kind": "invalid_word_budget", + "line": 140, + "path": "research/universal-f7-singleton-seedb859517b/search.py" + }, + { + "call": "joint_covers(5, set_level_splits(5, 10))", + "kind": "set_actual_sizes", + "line": 158, + "path": "research/universal-f7-singleton-seedb859517b/test_engine.py" + }, + { + "call": "joint_covers(5, set_level_splits(5, 10))", + "kind": "set_actual_sizes", + "line": 173, + "path": "research/universal-f7-singleton-seedb859517b/test_engine.py" + }, + { + "call": "joint_covers(5, set_level_splits(5, 10))", + "kind": "set_actual_sizes", + "line": 68, + "path": "research/universal-f7-singleton-seedb859517b/verify.py" + }, + { + "call": "cyclic_census(7, 18, budget=9, simple=True)", + "kind": "invalid_word_budget", + "line": 84, + "path": "research/universal-f7-singleton-seedb859517b/verify.py" + } + ], + "conditional_rows_without_word_census": { + "10,7": { + "assumed_excess_floors": [ + 3, + 0 + ], + "conditional_survivors": [], + "unfiltered_rows": 6 + }, + "11,6": { + "assumed_excess_floors": [ + 5, + 0 + ], + "conditional_survivors": [ + { + "b_ex": 1, + "c": 1, + "e_ex": 5, + "shared": 1 + }, + { + "b_ex": 0, + "c": 1, + "e_ex": 6, + "shared": 1 + } + ], + "unfiltered_rows": 7 + }, + "6,11": { + "assumed_excess_floors": [ + 0, + 5 + ], + "conditional_survivors": [ + { + "b_ex": 6, + "c": 1, + "e_ex": 0, + "shared": 1 + }, + { + "b_ex": 5, + "c": 1, + "e_ex": 1, + "shared": 1 + } + ], + "unfiltered_rows": 7 + }, + "7,10": { + "assumed_excess_floors": [ + 0, + 3 + ], + "conditional_survivors": [], + "unfiltered_rows": 6 + }, + "8,9": { + "assumed_excess_floors": [ + 0, + 0 + ], + "conditional_survivors": [], + "unfiltered_rows": 0 + }, + "9,8": { + "assumed_excess_floors": [ + 0, + 0 + ], + "conditional_survivors": [], + "unfiltered_rows": 0 + } + }, + "corrected_n7_word_censuses_replayed": false, + "large_sidon_floor_censuses_replayed": false, + "native_word_rule": { + "anchors": { + "#define BUDGET 27": 33, + "if (coll + newcoll > BUDGET) continue;": 93, + "if (nq & 1) {": 86 + }, + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c" + }, + "scope": "six pinned Python caller files plus the PR2691 native rule; not every repository call site", + "set_module_imports": { + "research/f7-17point-cover-audit-seedcfa215c2/cover17.py": [ + "functools" + ], + "research/f7-17point-cover-audit-seedcfa215c2/search17.py": [ + "json", + "pathlib", + "sys", + "time" + ] + } + }, + "subjects": { + "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "research/universal-f7-singleton-l20-seed06704c39/engine.py": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "research/universal-f7-singleton-seedb859517b/engine.py": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + "witnesses": { + "degree_counterexample": { + "coverage": 8, + "filtered_covers": 0, + "length": 6, + "minimum_degree": 1, + "minimum_restored_length": 6, + "points": [ + 0, + 1, + 2, + 3, + 4 + ], + "prefixes": [ + 0, + 1, + 3, + 2, + 0, + 4, + 0 + ], + "split": [ + 3, + 2 + ], + "unfiltered_covers": 18, + "word": "010122" + }, + "linear_transport": { + "degrees_after": [ + 0, + 1, + 1, + 1, + 2, + 2, + 3, + 4 + ], + "degrees_before": [ + 2, + 2, + 2, + 2, + 2, + 3, + 3, + 4 + ], + "isolated_vertex": 12, + "points": [ + 0, + 1, + 2, + 3, + 4, + 6, + 8, + 12 + ], + "transformed": [ + 0, + 1, + 2, + 3, + 5, + 6, + 9, + 12 + ] + }, + "old_parity": { + "actual_bit0_budget": 9, + "actual_old_engine": { + "5": { + "hits": 0, + "leaves": 0, + "nodes": 7 + }, + "9": { + "hits": 1, + "leaves": 1, + "nodes": 9 + }, + "None": { + "hits": 1, + "leaves": 1, + "nodes": 9 + } + }, + "bit0_excess": 8, + "bit0_split": [ + 6, + 2 + ], + "prefixes": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8, + 0 + ], + "weight_excess": 0, + "weight_split": [ + 4, + 4 + ], + "word": "01021323", + "wrong_budget": 5 + } + } +} diff --git a/research/f7-set-word-pruning-boundary/SOURCES.json b/research/f7-set-word-pruning-boundary/SOURCES.json new file mode 100644 index 0000000000..51139dc7ad --- /dev/null +++ b/research/f7-set-word-pruning-boundary/SOURCES.json @@ -0,0 +1,170 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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-17point-cover-audit-seedcfa215c2/cover17.py", + "usage": "input", + "git_blob": "5add3747a3b88951fd5634ed8106dbcf60cecd20", + "sha256": "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/search17.py", + "usage": "input", + "git_blob": "ef17635967fb14201119c70dd2bd426d073b5322", + "sha256": "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "usage": "input", + "git_blob": "79a3fe6e4f1f8abe9b909923a218e8dc8c825842", + "sha256": "2e6b6dadb285ae30115629c7dd0ed441f4e61e1979ddacbe129ef31926114278" + }, + { + "path": "research/f7-bit0-false-prune/README.md", + "usage": "provenance", + "git_blob": "83b23ff085f24451350dd9fe54b8efad68dc80dd", + "sha256": "d2507c556e23b36601d64c24ac394ab7192bd897d25f94e18471c86f83617efb" + }, + { + "path": "research/f7-union-support-audit/README.md", + "usage": "provenance", + "git_blob": "2c913f603f4190a15eda7fbe3def58524e0826dd", + "sha256": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a" + }, + { + "path": "research/f7-union-support-audit/census.cpp", + "usage": "input", + "git_blob": "5b290af8c8dd74f0b5a8ad0aec9bf2d55492507d", + "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "provenance", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a" + }, + { + "path": "research/f7-weight-parity-census-correction/README.md", + "usage": "provenance", + "git_blob": "0221748ce35d4a2dc6ee5ce61be210eb34a2ea83", + "sha256": "9bc7867ccfa97a682e4683052647d4bf8f191da5a219271f87d3e0a10de1446a" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "usage": "input", + "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + { + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "usage": "input", + "git_blob": "37d1c1ecfb705a55543dddfe87f43467cd4c50a2", + "sha256": "b4722f59811b9920e1f364e68a228ad5ad34cf98f9c490a3655d78dc2e9ae23b" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "usage": "input", + "git_blob": "649272d37b29aedb44f5a275189d0f7c05840d7b", + "sha256": "b403d815dad917440e238a7cafe4e15aa296f590e87c85c86653f06cba243055" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/verify.py", + "usage": "input", + "git_blob": "66a8d9f6a3b566ded57f7903089e6a02b2ffebd1", + "sha256": "a874a233fbb3800156731e1023404e40929157382ef84a8418ab538620fd7e40" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/search.py", + "usage": "input", + "git_blob": "2bb66b86822fdc248330ffb55bfe955ff4640ea9", + "sha256": "d8bad428035806848f9e0dc6caa3193e1a9abbad6a589dff3ef0e0b66f5f006c" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/test_engine.py", + "usage": "input", + "git_blob": "31c673bbc4b890c1bf5e2d0d98669c1787ce96c5", + "sha256": "7b62e83cc980a1f959cab09663433a0953bf487867b60cf10099ab9e0345c942" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/verify.py", + "usage": "input", + "git_blob": "8776d416cd5a5a7951f4082b4478d58b86795cb1", + "sha256": "7befdc8be7084c51482d2813de29c3e97d8d4fee52c1ac7a7e1b455e84fc0f56" + } + ], + "references": [ + { + "pr": 2542, + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "retained_base_bytes_match": true + }, + { + "pr": 2634, + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "retained_base_bytes_match": true + }, + { + "pr": 2691, + "head": "88dda3534071442773106e9c0b941b9d39a3cea8", + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "sha256": "b4722f59811b9920e1f364e68a228ad5ad34cf98f9c490a3655d78dc2e9ae23b", + "retained_base_bytes_match": true + }, + { + "pr": 2773, + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "path": "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "retained_base_bytes_match": true + }, + { + "pr": 2973, + "head": "d48f3945dbb1ef5d06835744c4082b3bd04181c0", + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a", + "retained_base_bytes_match": true + }, + { + "pr": 3005, + "head": "68e67922294d96a42f479f80fdc352eb04a9b550", + "path": "research/f7-union-support-audit/census.cpp", + "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949", + "retained_base_bytes_match": true + } + ] +} diff --git a/research/f7-set-word-pruning-boundary/TASK.json b/research/f7-set-word-pruning-boundary/TASK.json new file mode 100644 index 0000000000..503edd188d --- /dev/null +++ b/research/f7-set-word-pruning-boundary/TASK.json @@ -0,0 +1,176 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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": "Audit PR2542 joint_covers at actual bit-0 split sizes, its optional degree-two contract, and the source-impact boundary to word exclusions and PR2773 set-level rows.", + "scope_change_reason": "The tiny parity witness and independent full n=7 implementation are already covered by PR2973, the tiny audit and PR3005. Check the retained set interface and degree implication, without another large word census.", + "bottleneck_link": "Prevent an invalid word prune or adjacency assumption from closing a route, while retaining separately justified set-cover evidence.", + "budget_minutes": 60, + "stop_rule": "Stop after exact small-set comparisons, explicit contract counterexamples and a pinned source-impact map. No n=7 enumeration, supplier change or family expansion.", + "outcome": "completed", + "evidence": "RESULT.json: all 32906 zero-containing sets at n=1..4, 200 exact split/filter comparisons, direct old-engine parity control, minimal-word degree counterexample, and six Python budgeted call sites plus the native rule. The large word and Sidon censuses are not replayed.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing. No independent human review claimed.", + "open_questions": [ + { + "question": "Should a maintained successor split actual-size set-cover and simple-cycle APIs?", + "why_it_matters": "Minimum word length does not imply a degree-two prefix set; the degree-one minimal witness falsifies the retained generic justification.", + "first_step": "Specify the simple-cycle contract |P|=L>=4 separately and retain actual bit-0 split semantics, with both new counterexamples as controls.", + "blocked_by": "An interface maintenance decision; frozen predecessors remain immutable." + }, + { + "question": "Which retained historical callers should explicitly route mathematical exclusion requests to corrected evidence?", + "why_it_matters": "Six Python calls and the PR2691 native rule still reproduce the invalid filter; counter agreement cannot restore soundness.", + "first_step": "Use the pinned call-site map to distinguish historical counter reproduction from exclusion, then annotate or provide a maintained successor entry point.", + "blocked_by": "Independent scientific review of corrected n=7 receipts is separate; no large replay is part of this package." + } + ], + "scope_key": "641feda6be471c89abb9/pr2542-joint-covers-actual-bit0-all-subsets-n1-4", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317", + "predecessor_heads": { + "2542": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "2634": "e2f30d93efbef5658334072aa855aa95e795e394", + "2691": "88dda3534071442773106e9c0b941b9d39a3cea8", + "2773": "6739c799799621878a9249c93e2b12cc799c1482", + "2973": "d48f3945dbb1ef5d06835744c4082b3bd04181c0", + "3005": "68e67922294d96a42f479f80fdc352eb04a9b550" + }, + "task_card": { + "track": "adversarial-audit", + "object": "Actual-size bit-0 set enumeration and the minimum-degree implication at the retained set/word boundary", + "method": "Pruning-free subset oracle, exact witness sets, literal prefix traces, source-authenticated actual functions and AST call-site inventory", + "bounded_domain": "n=1..4; every subset containing zero; all ordered bit-0 split sizes; minimum-degree flag off/on; three fixed-word/coordinate controls", + "milestone": "audit and finite certificate", + "required_observable_improvement": "Distinguish invalid word-exclusion receipts from separately checked set behavior; falsify one retained interface justification", + "cost_budget": "No arithmetic, supplier or kappa saving claimed", + "unresolved_costs": "No physical consumer or restoration implementation proposed", + "expansion_decision": "narrow and stop", + "falsification_test": "Any returned-set mismatch, dropped positive witness, source mismatch, enabled degree caller or accepted node cap fails", + "reproduction": "python3 -I -B research/f7-set-word-pruning-boundary/verify.py" + }, + "existing_checks_assessed": [ + { + "source": "PR2973", + "coverage": "Tiny parity witness, corrected collision budgets and source-impact reasoning; own full corrected n=7 engine", + "remaining_for_this_scope": "Actual retained set enumeration and degree-contract audit" + }, + { + "source": "research/f7-bit0-false-prune", + "coverage": "Small canonical word domains and the old balanced-budget witness", + "remaining_for_this_scope": "All-small-subset interface, not another word-domain replay" + }, + { + "source": "PR3005", + "coverage": "Separate union-support full n=7 word implementation and small unpruned word oracle", + "remaining_for_this_scope": "Independent implementation question is already covered; no duplicate full replay" + } + ], + "overlap": { + "queries": [ + "--task census-pruning-audit", + "joint_covers; set-level boundary; bit-0 split", + "010122; require_min_degree; minimal length walks" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-17T17:04:11.636955+00:00", + "complete_pagination": true, + "records": 245 + }, + "discussions": { + "fetched_at": "2026-10-17T17:04:42.538402+00:00", + "complete_pagination": true, + "records": 1985 + } + }, + "limitation": "Offline complete snapshots; includes local main packages but not every diff or nested file. No matches is not novelty.", + "nearest": [ + "PR2973", + "PR3005", + "research/f7-bit0-false-prune", + "PR2542/2634/2691", + "PR2773" + ], + "added_value": "Actual retained set-function equality across all small subsets, explicit minimal-word degree counterexample, and source-bound dependence boundary.", + "final_coverage": { + "open_prs": { + "fetched_at": "2026-10-17T17:26:19.594925+00:00", + "complete_pagination": true, + "records": 249 + }, + "discussions": { + "fetched_at": "2026-10-17T17:27:03.117721+00:00", + "complete_pagination": true, + "records": 2001 + } + }, + "independent_parallel_scope": "The concurrently claimed connector-covering-code capacity audit concerns its newer projected length-22 rule, a different source and question from PR2542 joint_covers." + }, + "refresh_checkpoints": [ + { + "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "checked_at_utc": "2026-10-17T17:16:47Z", + "decision": "Start from canonical main." + }, + { + "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "checked_at_utc": "2026-10-17T17:29:04.263616+00:00", + "change": "None; guidance, selected record and relevant sources unchanged.", + "decision": "Preserve pinned inputs and continue the same scoped audit." + }, + { + "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "checked_at_utc": "2026-10-17T17:34:49.829806+00:00", + "change": "No changes from the entry main commit; priorities, catalogue, selected record and relevant predecessors unchanged.", + "decision": "Complete the bounded audit; no larger census or family expansion." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19001818" +} diff --git a/research/f7-set-word-pruning-boundary/VERIFY.json b/research/f7-set-word-pruning-boundary/VERIFY.json new file mode 100644 index 0000000000..02c5f7eeb4 --- /dev/null +++ b/research/f7-set-word-pruning-boundary/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-17point-cover-audit-seedcfa215c2/cover17.py", + "research/f7-17point-cover-audit-seedcfa215c2/search17.py", + "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", + "research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "research/f7-union-support-audit/census.cpp", + "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "research/universal-f7-singleton-l20-seed06704c39/verify.py", + "research/universal-f7-singleton-seedb859517b/engine.py", + "research/universal-f7-singleton-seedb859517b/search.py", + "research/universal-f7-singleton-seedb859517b/test_engine.py", + "research/universal-f7-singleton-seedb859517b/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 32906 sets, 200 exact split/filter witness sets, known parity and new degree/coordinate controls, source-impact inventory and fail-closed cap." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py", + "-v" + ], + "timeout_seconds": 60, + "checks": "Meaningful source, budget, partition, duplicate, caller and receipt corruption controls." + } + ] +} diff --git a/research/f7-set-word-pruning-boundary/test_verify.py b/research/f7-set-word-pruning-boundary/test_verify.py new file mode 100644 index 0000000000..820e66b88d --- /dev/null +++ b/research/f7-set-word-pruning-boundary/test_verify.py @@ -0,0 +1,77 @@ +"""Failure controls for the source-bound set/word interface audit.""" + +import copy +import json +from pathlib import Path +import types +import unittest +from unittest.mock import patch + + +HERE = Path(__file__).resolve().parent +audit = types.ModuleType("boundary_audit") +audit.__file__ = str(HERE / "verify.py") +exec(compile((HERE / "verify.py").read_bytes(), audit.__file__, "exec"), audit.__dict__) + + +class BoundaryControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.sources = audit.source_bytes() + + def test_actual_source_counterexamples_and_controls(self): + subject = audit.load_bytes(self.sources[audit.OLD], audit.OLD) + witnesses = audit.fixed_witnesses(subject) + self.assertEqual(witnesses["degree_counterexample"]["filtered_covers"], 0) + self.assertTrue(all(audit.controls(self.sources[audit.OLD]).values())) + + def test_changed_source_is_rejected_before_execution(self): + original = Path.read_bytes + target = audit.ROOT / audit.OLD + + def changed(path): + data = original(path) + return data + b"\n# corrupted audit subject\n" if path == target else data + + with patch.object(Path, "read_bytes", changed): + with self.assertRaisesRegex(audit.AuditFailure, "source hash mismatch"): + audit.source_bytes() + + def test_wrong_partition_and_duplicate_output_are_rejected(self): + with self.assertRaisesRegex(audit.AuditFailure, "wrong bit-0 partition"): + audit.canonical_results([((0, 1), (2, 3))], 2, (2, 2)) + row = ((0, 2), (1, 3)) + with self.assertRaisesRegex(audit.AuditFailure, "duplicate returned cover"): + audit.canonical_results([row, row], 2, (2, 2)) + + def test_set_domain_catches_balanced_budget_mutant(self): + data = self.sources[audit.OLD] + anchor = b"budget = A + B - even_nonzero" + replacement = b"budget = 2 * (((s+t)//2)*((s+t)//2-1)//2) - even_nonzero" + mutant = audit.load_bytes(data.replace(anchor, replacement), audit.OLD) + with self.assertRaisesRegex(audit.AuditFailure, "set disagreement"): + audit.exhaustive_sets(mutant) + + def test_source_impact_rejects_new_degree_filter_caller(self): + sources = self.sources.copy() + path = "research/universal-f7-singleton-seedb859517b/search.py" + sources[path] = sources[path].replace( + b"joint_covers(5, splits10)", + b"joint_covers(5, splits10, require_min_degree=True)") + with self.assertRaisesRegex(audit.AuditFailure, "retained caller enables"): + audit.source_impact(sources) + + def test_receipt_rejects_changed_count_or_missing_case(self): + expected = json.loads((HERE / "RESULT.json").read_text()) + for kind in ("count", "case"): + changed = copy.deepcopy(expected) + if kind == "count": + changed["small_domain"][3]["covers"] += 1 + else: + changed["small_domain"][3]["cases"].pop() + with self.assertRaisesRegex(audit.AuditFailure, "receipt mismatch"): + audit.compare_receipt(changed, expected) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/f7-set-word-pruning-boundary/verify.py b/research/f7-set-word-pruning-boundary/verify.py new file mode 100644 index 0000000000..dd1db288d3 --- /dev/null +++ b/research/f7-set-word-pruning-boundary/verify.py @@ -0,0 +1,336 @@ +#!/usr/bin/env python3 +"""Audit retained set/word pruning contracts; no seven-label enumeration. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. +Apache-2.0. The authenticated predecessor engines retain their authorship. +""" + +import argparse +import ast +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from math import comb +from pathlib import Path +import types + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +OLD = "research/universal-f7-singleton-seedb859517b/engine.py" +COPIES = ( + OLD, + "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py", +) +SET_MODULE = "research/f7-17point-cover-audit-seedcfa215c2/cover17.py" +CALLERS = ( + "research/universal-f7-singleton-seedb859517b/search.py", + "research/universal-f7-singleton-seedb859517b/verify.py", + "research/universal-f7-singleton-seedb859517b/test_engine.py", + "research/universal-f7-singleton-l20-seed06704c39/verify.py", + "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "research/f7-17point-cover-audit-seedcfa215c2/verify.py", +) +MARKER = "PASS_F7_SET_WORD_BOUNDARY" + + +class AuditFailure(Exception): + """An explicit failure, including when Python runs with -O.""" + + +def require(condition, message): + if not condition: + raise AuditFailure(message) + + +def source_bytes(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + result = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + require(sha256(data).hexdigest() == row["sha256"], + "source hash mismatch: " + row["path"]) + result[row["path"]] = data + return result + + +def load_bytes(data, path): + # Compile authenticated source directly, without reading a .pyc or + # changing a frozen file. Both loaded modules use only the stdlib. + module = types.ModuleType("audited_subject") + module.__file__ = str(ROOT / path) + exec(compile(data, module.__file__, "exec"), module.__dict__) + return module + + +def prefixes(word): + points = [0] + for label in word: + points.append(points[-1] ^ (1 << label)) + return points + + +def support(points): + return {x ^ y for x in points for y in points} + + +def degrees(points): + # Pairwise Hamming distances, unlike the subject's coordinate flips. + return {x: sum((x ^ y).bit_count() == 1 for y in points) for x in points} + + +def split_points(points, weight=False): + return tuple(tuple(x for x in sorted(points) + if ((x.bit_count() if weight else x) & 1) == parity) + for parity in (0, 1)) + + +def within_excess(parts): + return sum(comb(len(part), 2) - len({x ^ y for x, y in combinations(part, 2)}) + for part in parts) + + +def canonical_results(rows, n, split): + result = [] + for even, odd in rows: + points = tuple(sorted(even + odd)) + require(len(set(points)) == len(points), "duplicate point in result") + require(0 in even, "normalization lost zero") + require((even, odd) == split_points(points), "wrong bit-0 partition") + require((len(even), len(odd)) == split, "wrong actual split") + require(all(0 <= x < 1 << n for x in points), "point outside domain") + result.append(points) + require(len(result) == len(set(result)), "duplicate returned cover") + return set(result) + + +def point_set_hash(point_sets): + payload = json.dumps(sorted(point_sets), separators=(",", ":")).encode() + return sha256(payload).hexdigest() + + +def subset_oracle(n): + """Every zero-containing set, without capacity/collision/degree pruning.""" + size = 1 << n + covers, filtered = {}, {} + for mask in range(1 << (size - 1)): + points = (0,) + tuple(x for x in range(1, size) if mask >> (x - 1) & 1) + if len(support(points)) != size: + continue + split = tuple(map(len, split_points(points))) + covers.setdefault(split, set()).add(points) + if min(degrees(points).values()) >= 2: + filtered.setdefault(split, set()).add(points) + return covers, filtered + + +def forbidden_word_census(*args, **kwargs): + raise AuditFailure("set-level check reached the word census") + + +def exhaustive_sets(subject): + subject.cyclic_census = forbidden_word_census + receipt = [] + for n in range(1, 5): + oracle = subset_oracle(n) + for split in oracle[0]: + require(split in subject.set_level_splits(n, sum(split)), + f"set-level split selector loses a cover {(n, split)}") + cases = [] + for s in range(1, (1 << (n - 1)) + 1): + for t in range((1 << (n - 1)) + 1): + for flag in (False, True): + expected = oracle[int(flag)].get((s, t), set()) + actual = canonical_results( + subject.joint_covers(n, [(s, t)], require_min_degree=flag), + n, (s, t)) + require(actual == expected, f"set disagreement {(n, s, t, flag)}") + cases.append({"split": [s, t], "minimum_degree_two": flag, + "covers": len(actual), + "sets_sha256": point_set_hash(actual)}) + receipt.append({"n": n, "all_sets": 1 << ((1 << n) - 1), + "covers": sum(map(len, oracle[0].values())), + "degree_two_covers": sum(map(len, oracle[1].values())), + "cases": cases}) + return receipt + + +def fixed_witnesses(subject): + word = tuple(map(int, "01021323")) + trace = prefixes(word) + points = tuple(sorted(set(trace))) + require(trace == [0, 1, 3, 2, 6, 4, 12, 8, 0], "wrong old counterexample") + require(len(support(points)) == 16 and len(points) == 8, "not a simple cover") + bit_parts, weight_parts = split_points(points), split_points(points, True) + require(tuple(map(len, bit_parts)) == (6, 2), "wrong bit split") + require(tuple(map(len, weight_parts)) == (4, 4), "wrong weight split") + require(within_excess(bit_parts) == 8, "wrong bit collision excess") + require(within_excess(weight_parts) == 0, "wrong weight collision excess") + old_control = {} + for budget in (None, 5, 9): + row = subject.cyclic_census(4, 8, budget=budget, simple=True, + prefix=word, max_nodes=100) + old_control[str(budget)] = {k: row[k] for k in ("nodes", "leaves", "hits")} + require(row["hits"] == (0 if budget == 5 else 1), "old prune control failed") + right = canonical_results(subject.joint_covers(4, [(6, 2)]), 4, (6, 2)) + wrong = canonical_results(subject.joint_covers(4, [(4, 4)]), 4, (4, 4)) + require(points in right and points not in wrong, "actual-size boundary failed") + + short = tuple(map(int, "010122")) + short_trace = prefixes(short) + short_set = tuple(sorted(set(short_trace))) + require(short_trace[-1] == 0 and Counter(short) == {0: 2, 1: 2, 2: 2}, + "three-label witness does not restore") + require(len(support(short_set)) == 8, "three-label witness does not cover") + require(min(degrees(short_set).values()) == 1, "degree-one witness lost") + unfiltered = canonical_results(subject.joint_covers(3, [(3, 2)]), 3, (3, 2)) + filtered = canonical_results(subject.joint_covers(3, [(3, 2)], True), 3, (3, 2)) + require(short_set in unfiltered and not filtered, "degree-filter counterexample failed") + require(len(unfiltered) == 18, "three-label split control changed") + + # T puts weight parity in output bit 0. It changes the singleton alphabet. + transform = lambda x: (x & ~1) | (x.bit_count() & 1) + moved = tuple(sorted(map(transform, points))) + require(all(transform(transform(x)) == x for x in range(16)), "T not invertible") + require(all(transform(x ^ y) == transform(x) ^ transform(y) + for x in range(16) for y in range(16)), "T not linear") + require(len(support(moved)) == 16, "linear map lost coverage") + require(min(degrees(points).values()) == 2 and degrees(moved)[12] == 0, + "adjacency transport counterexample failed") + require(moved in wrong, "transformed set not at bit split (4,4)") + moved_filtered = canonical_results(subject.joint_covers(4, [(4, 4)], True), 4, (4, 4)) + require(moved not in moved_filtered, "degree filter should reject isolated point") + return {"old_parity": {"word": "01021323", "prefixes": trace, + "bit0_split": [6, 2], "weight_split": [4, 4], + "bit0_excess": 8, "weight_excess": 0, + "wrong_budget": 5, "actual_bit0_budget": 9, + "actual_old_engine": old_control}, + "degree_counterexample": {"word": "010122", "prefixes": short_trace, + "points": short_set, "coverage": 8, + "length": 6, "minimum_restored_length": 6, + "minimum_degree": 1, "split": [3, 2], + "unfiltered_covers": 18, "filtered_covers": 0}, + "linear_transport": {"points": points, "transformed": moved, + "degrees_before": sorted(degrees(points).values()), + "degrees_after": sorted(degrees(moved).values()), + "isolated_vertex": 12}} + + +def source_impact(sources): + calls = [] + for path in CALLERS: + for node in ast.walk(ast.parse(sources[path])): + if not isinstance(node, ast.Call): + continue + name = node.func.id if isinstance(node.func, ast.Name) else getattr(node.func, "attr", "") + budgeted = name == "cyclic_census" and any(k.arg == "budget" for k in node.keywords) + if name == "joint_covers" or budgeted: + if name == "joint_covers": + require(len(node.args) == 2 and not node.keywords, + "retained caller enables a new filter or argument") + calls.append({"path": path, "line": node.lineno, + "kind": "set_actual_sizes" if name == "joint_covers" else "invalid_word_budget", + "call": ast.unparse(node)}) + require(sum(c["kind"] == "set_actual_sizes" for c in calls) == 4, "set caller inventory changed") + require(sum(c["kind"] == "invalid_word_budget" for c in calls) == 6, "word caller inventory changed") + imports = {} + for path in (SET_MODULE, "research/f7-17point-cover-audit-seedcfa215c2/search17.py"): + names = [] + for node in ast.walk(ast.parse(sources[path])): + if isinstance(node, ast.Import): + names.extend(alias.name for alias in node.names) + elif isinstance(node, ast.ImportFrom): + names.append(node.module) + require(set(names) <= {"functools", "json", "sys", "time", "pathlib"}, + "new non-stdlib set-module dependency") + imports[path] = sorted(names) + cover = load_bytes(sources[SET_MODULE], SET_MODULE) + row_counts = {} + for s, t in ((9, 8), (8, 9), (10, 7), (7, 10), (11, 6), (6, 11)): + rows = cover.sharp_rows(7, s, t) + lo, hi = ((3, 0) if s == 10 else (0, 3) if t == 10 + else (5, 0) if s == 11 else (0, 5) if t == 11 else (0, 0)) + survivors = cover.surviving_rows(7, s, t, lo, hi)["rows"] + require(len(survivors) == (2 if 11 in (s, t) else 0), "conditional set rows changed") + row_counts[f"{s},{t}"] = {"unfiltered_rows": len(rows["rows"]), + "assumed_excess_floors": [lo, hi], + "conditional_survivors": survivors} + native_path = "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c" + native_text = sources[native_path].decode() + anchors = ("#define BUDGET 27", "if (nq & 1) {", "if (coll + newcoll > BUDGET) continue;") + native_rule = {} + for anchor in anchors: + require(anchor in native_text, "native word-rule anchor changed") + native_rule[anchor] = native_text[:native_text.index(anchor)].count("\n") + 1 + return {"scope": "six pinned Python caller files plus the PR2691 native rule; not every repository call site", + "calls": sorted(calls, key=lambda c: (c["path"], c["line"])), + "native_word_rule": {"path": native_path, "anchors": native_rule}, + "set_module_imports": imports, + "conditional_rows_without_word_census": row_counts, + "large_sidon_floor_censuses_replayed": False, + "corrected_n7_word_censuses_replayed": False} + + +def controls(data): + subject = load_bytes(data, OLD) + try: + subject.joint_covers(3, [(3, 2)], max_nodes=1) + except OverflowError: + pass + else: + raise AuditFailure("node cap was accepted as a complete result") + # Mutate only the in-memory subject; frozen inputs remain unchanged. + old = b"budget = A + B - even_nonzero" + new = b"budget = 2 * (((s + t) // 2) * (((s + t) // 2) - 1) // 2) - even_nonzero" + require(data.count(old) == 1, "balanced-budget mutation anchor changed") + mutant = load_bytes(data.replace(old, new), OLD) + points = tuple(sorted(set(prefixes(tuple(map(int, "01021323")))))) + returned = canonical_results(mutant.joint_covers(4, [(6, 2)]), 4, (6, 2)) + require(points not in returned, "balanced-size mutant survived witness") + return {"cap_raises": True, "balanced_size_mutant_rejected": True, + "partition_misinterpretation_rejected": True, + "degree_filter_counterexample_detected": True, + "linear_map_adjacency_loss_detected": True} + + +def compute(): + sources = source_bytes() + require(all(sources[path] == sources[OLD] for path in COPIES), "old copies differ") + subject = load_bytes(sources[OLD], OLD) + witnesses = fixed_witnesses(subject) + receipt = exhaustive_sets(subject) + result = {"schema_version": 1, "kind": "scoped_source_audit_and_finite_certificate", + "subjects": {p: sha256(sources[p]).hexdigest() for p in COPIES}, + "all_sets": sum(r["all_sets"] for r in receipt), + "exact_domain_comparisons": sum(len(r["cases"]) for r in receipt), + "small_domain": receipt, "witnesses": witnesses, + "source_impact": source_impact(sources), + "controls": controls(sources[OLD])} + require(result["all_sets"] == 32906 and result["exact_domain_comparisons"] == 200, + "finite domain coverage changed") + return result + + +def compare_receipt(actual, expected): + # JSON normalizes tuple/list representation; compare every field. + require(json.loads(json.dumps(actual)) == expected, "receipt mismatch") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print recomputed receipt; write nothing") + args = parser.parse_args() + result = compute() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + return + compare_receipt(result, json.loads((HERE / "RESULT.json").read_text())) + print(f"{MARKER} sets=32906 comparisons=200 degree_counterexample=010122 no_new_kappa") + + +if __name__ == "__main__": + main()