diff --git a/research/connector-capacity-parity-audit/README.md b/research/connector-capacity-parity-audit/README.md new file mode 100644 index 0000000000..11e76c254b --- /dev/null +++ b/research/connector-capacity-parity-audit/README.md @@ -0,0 +1,232 @@ +# The simple-word parity-capacity filter and its repeated-prefix boundary + +The `Engine::capacity` predicate in conorholds' retained +[connector-covering-code](../connector-covering-code/README.md) is a **necessary +condition for a simple restored universal word**, under its four-low-coordinate, +three-high-coordinate projection. The proof below includes repeated **low** +vertices and binds every rejection to the actual source. A separately implemented +position-pair oracle agrees with the compiled predicate on **791,827 declared gap +cases**, with **53,379 accepted**. Accepted gaps are not constructed words. + +The simplicity premise matters. The credited universal word +`010201030102010345464546` has 24 steps and 23 distinct prefixes. The actual +predicate rejects its projection: nine positions at low vertex zero represent +only eight distinct high states. Thus it is not a necessary condition for +arbitrary restored words; applying it to repeated-prefix length-22 candidates +would need an additional argument. This is an explicit boundary control, **not an +error in the predecessor**, whose length-22 path engine is explicitly restricted +to simple words and handles repeated-prefix cases separately. + +This is a scoped proof and finite implementation audit. It does not reprove +`f(7)=24`, rerun either complete seven-label census, admit a supplier, or change +kappa. The new evidence concerns one predicate in the newer length-22 argument. +The reconstruction of #2973's old counterexample is credited calibration. + +## Source boundary + +The audited source is `cycle_search.cpp` at main introduction +`e67ca5f26351e09c5bb314821633e511212f88ec`, SHA256 +`597844fc32cde19c1d4104633fa6d3eb0d28c1ca140f8f3d2ba2cb632ecd30d1`. +The package base is `463113d675af7410ac91d53a4fed51ec6494eb9a`. +The claim is in [discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19001874). +[SOURCES.json](SOURCES.json) pins the exact old Python/C engines, callers, +corrected #2973 engine, and successor source. Frozen sources are unchanged. + +[audit.cpp](audit.cpp) includes the original C++ file with its entry point +renamed and calls `Engine::capacity` directly. It does not copy or alter that +predicate. Its oracle lists individual time positions and then every unordered +pair; it does not use the source's aggregated products, `low_points`, or parity +routine. The source generates the 5 A and 77 B low templates for this finite +comparison. Completeness of that template generator is **not** established here. +A further Python oracle checks separately specified inputs and actual universal +words against the compiled predicate. + +## Necessary-condition proof + +Write a full prefix as `(a,h)` with low component `a in F2^4` and high +component `h in F2^3`. Rotate a restored word to end in a low step and translate +its starting prefix to zero. Let `a_i` be the low prefix before low step `i`, +and let `g_i` be the number of preceding high steps since the previous low step. +Block `i` contributes exactly `g_i+1` nonclosing prefix positions, all at `a_i`. +The terminal closing prefix is not an additional position. + +Each high singleton step flips the Hamming parity of `h`; a low step leaves it +unchanged. Consequently the high-parity sequence in block `i` starts at + +``` +p_i = (g_0 + ... + g_(i-1)) mod 2 +``` + +and alternates for `g_i` steps. With `s_i=g_i+1`, its even and odd position counts +are `floor((s_i + [p_i=0])/2)` and the remainder. This is exactly the source's +`high_parity` update and its `even` expression. Summing over **every** block +with the same `a_i=a` gives `E_a,O_a`, and `S_a=E_a+O_a`. + +For a **simple** full word, these positions are distinct full states, including +between different blocks at the same low vertex. There are only eight high +states, so `g_i<=7` and `S_a<=8`. Restoration requires an even total number of +high steps. These justify the source's first three rejection conditions. The +word need not have distinct low prefixes. + +For each low difference `d`, count unordered pairs of distinct full positions +whose high difference has parity `epsilon`. Their exact counts are + +``` +C(0,0) = sum_a (choose(E_a,2) + choose(O_a,2)) +C(0,1) = sum_a E_a O_a +C(d,0) = sum_{a= 3; C(0,1) >= 4; +C(d,0) >= 4 and C(d,1) >= 4 for each d != 0. +``` + +Every source rejection is therefore necessary. Collisions may make these +conditions too weak; passing is not sufficient for a lift, an endpoint join, +a simple word, or coverage. The proof applies to every nonnegative gap vector +in this source contract, beyond the bounded vectors exercised below. + +### Which parity changes preserve this test? + +For any `lambda in F2^4`, replace high parity by +`wt(h) + lambda dot a (mod 2)`. A pair at low difference `d` changes its parity +by the fixed bit `lambda dot d`. Thus it merely swaps the two buckets for that +`d`. For `d=0` no swap occurs; for `d!=0` both thresholds are four. All sixteen +choices give the same verdict. Full-word time parity is the choice +`lambda=(1,1,1,1)`; it is a valid alternative **for this particular test**. +Resetting high parity independently at each block is not this transformation. +Nor can a single high coordinate be inferred from the number of high steps. +This explains the precise parity premise rather than declaring every change +of partition valid or invalid. + +## Finite evidence and controls + +[RESULT.json](RESULT.json) is compared with a fresh run, not trusted as an input +certificate of successful execution. The declared native domains are: + +| Domain | Gap vectors per source template | Templates | Cases | Predicate accepts | +|---|---|---:|---:|---:| +| A core | `0<=g_i<=3`, eight gaps summing to 14 | 5 | 33,640 | 1,924 | +| B core | `0<=g_i<=2`, ten gaps summing to 12 | 77 | 520,905 | 51,305 | +| A boundary | At most two nonzero gaps, each in `1..8` | 5 | 9,285 | 0 | +| B boundary | At most two nonzero gaps, each in `1..8` | 77 | 227,997 | 150 | + +These are complete **predicate-input** domains, not complete word searches. +Boundary domains include out-of-contract gaps of eight to test rejection. +Their exact sizes are independently computed in Python by generating-function +coefficients or `1+8b+64*choose(b,2)`. The oracle records the first failed bound; +there are no source/oracle disagreements. + +The controls also include: + +- The retained simple universal 24-step fixture, directly checked for 24 distinct + prefixes and all 128 differences. All 176 eligible three-high-coordinate + projections, orientations and low-step endings pass the actual predicate. + Of these, 120 have repeated low prefixes. All sixteen parity changes above + are checked on each: 2,816 exact bucket permutation checks. +- A separate Python/source comparison on both complete binary-gap cubes for low + words `01021323` and `0001021323`, plus two discrimination fixtures: 1,282 + queries. The universal projections and repeated-prefix boundary are additional + source queries. +- Resetting parity at each block changes 1,148 B-core verdicts; dropping pairs + between equal-low blocks changes 542. The explicit fixtures are + `0001021323 / 0101202222` and `0001203231 / 1111111122`, respectively. Both pass + the correct capacity predicate and fail the mutation. Their complete pair + profiles are recorded: reset changes `C(6,1)` from 4 to 3, and omission + changes `C(0,0)` from 6 to 2. **They are gap fixtures, not universal-word witnesses**. +- The nonsimple universal word above, projected with high coordinates `{0,1,2}`, + gives low word `0012131213` and gaps `(7,7,0,0,0,0,0,0,0,0)`. At low zero, + nine positions but eight distinct high states make the simplicity-specific + guard fail. Removing this premise would invalidate the proof. +- #2973's `01021323` calibration: prefixes `0,1,3,2,6,4,12,8`, all 16 + differences, weight split `(4,4)`, bit-0 split `(6,2)`, bit-0 excess 8, + balanced budget 5, and valid actual-size bit-0 budget 9. + +All acceptance checks remain active under Python `-O`; no `assert` is used. +Source digests are checked before compilation. Native builds and runs are serial, +time-limited, and use a temporary directory removed on exit. No word CSP is run. +The registered failure-control command changes private copies of the actual +native predicate: a parity reset flips the first discrimination fixture, and +relaxing the fiber bound to nine admits the repeated-prefix control. Altered +source hashes, a corrupted receipt and a truncated native query all reject. + +## Which predecessor exclusions need replacement evidence? + +| Evidence | Exact affected implication | Status within this audit | +|---|---|---| +| #2542 `search.py` length-18 call | `cyclic_census(7,18,budget=9,simple=True)` groups by `nq & 1`, not the time-balanced weight classes used to derive 9 | Old zero-hit receipt cannot certify that exclusion. #2973 supplies a corrected length-18 receipt; #3005 reports separate replacement enumeration. Neither full enumeration is rerun here. | +| #2634 `census20.py` and vendored engine | The same Python engine is byte-identical; the length-20 call substitutes budget 27 | Its partial word traversal and inherited length-18 replay do not establish completeness. They need corrected evidence wherever relied upon. | +| #2691 `f7_census.c` | The C traversal uses `nq & 1` and `BUDGET=27` | Completing all shards reproduced the same invalid filter. Its old 6,305,209,079-node exclusion is not repaired by cross-language agreement. #2973/#3005 provide separate length-20 evidence. | +| #2973 corrected engine and #3005 union-support engine | Distinct weight-parity sets, valid target budgets, complete split coverage | Existing replacement evidence; this package pins #2973's partition and credits #3005. No new full replay or admission. | +| `connector-covering-code` simple length-22 branch | Actual high-parity pair capacity after the four-plus-three projection | This one predicate's necessity and repeated-low bookkeeping are checked here. Remaining path tables, propagation, symmetry reductions and complete enumeration are not checked. | +| That successor's repeated-prefix branch | Exclusion of shorter words with non-simple prefix walks | Requires its separate minimum-cover/classification and support arguments. The universal 24-step control disproves an unrestricted extension of this predicate; it does not disprove a length-22 exclusion. Those separate arguments are not checked here. | + +The correction does not itself revoke the old counting identity, explicit +witnesses, or later set-level #2773/#2870/#2911/#2933/#2961 arguments. Their +hypotheses and evidence are separate. The actual-size set-enumerator question +is separate from this successor audit. No retained old package is edited and +no final seven-source bound is declared false by the tiny counterexample. + +## Reproduce + +From the repository root, Python 3.12 and a C++17 compiler are sufficient: + +```sh +python3 -I -B scripts/research_package.py --package research/connector-capacity-parity-audit +``` + +The registered ordinary and optimized commands each print: + +```text +PASS_CONNECTOR_CAPACITY_PARITY cases=791827 accepted=53379 positive_projections=176 gauges=2816 python_queries=1282 repeated_prefix_control=1 no_full_census +``` + +The third registered command prints +`PASS_CAPACITY_FAILURE_CONTROLS source_pin=1 native_mutants=2 malformed_query=2 receipt=1`. +All four native domain rows also passed an AddressSanitizer/UndefinedBehaviorSanitizer +build with identical counters and no diagnostics; this development check is +recorded in TASK.json and is not required by the portable replay. + +Direct replay is `python3 -I -B research/connector-capacity-parity-audit/verify.py`. +`--write-receipt` explicitly regenerates the receipt; ordinary replay never +rewrites it. [TASK.json](TASK.json) records environment and completed checks. + +## Open next questions + +An independent implementation of the complete B length-22 path exclusion would +close a different remaining computational obligation. Start by checking its +endpoint, disjointness and conditional-coverage propagation against explicit +path-domain tuples, with planted feasible controls, before proposing a full +82-orbit run. This package gives neither completeness of those rules nor a +resource budget for that search. Published coding/classification premises and +the non-simple branch likewise remain separate obligations. Replaying the old +unsound counts again would not resolve any of these questions. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +conorholds supplied the successor, the native predicate and the simple 24-step +fixture. Nicholas Stone supplied #2691 and the #2973 correction and tiny +counterexample; Nick Petalas supplied #3005's independent union-support replay. +Aaron Wang supplied the #2542/#2634 census and later set-level lineage. Ross +Richardson supplied the #943 prefix-walk model; Douglas Colkitt supplied #1185 +and the retained Gray upper witness. jwr's `f7-bit0-false-prune` already checks +the tiny counterexample and a small word domain; this calibration is not claimed +as new. The substantial AI reviews credited by the predecessor are retained as +prior evidence, not represented as independent human review. + +New derivation, code, checking and writing used OpenAI Codex. Apache-2.0; +predecessor attribution is preserved. No independent human or formal-kernel +review is claimed. diff --git a/research/connector-capacity-parity-audit/RESULT.json b/research/connector-capacity-parity-audit/RESULT.json new file mode 100644 index 0000000000..8da69fbe3d --- /dev/null +++ b/research/connector-capacity-parity-audit/RESULT.json @@ -0,0 +1,672 @@ +{ + "historical_control": { + "balanced_budget": 5, + "coverage": 16, + "partitions": { + "bit0": { + "actual_budget": 9, + "excess": 8, + "sizes": [ + 6, + 2 + ] + }, + "weight": { + "actual_budget": 5, + "excess": 0, + "sizes": [ + 4, + 4 + ] + } + }, + "prefixes": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8 + ], + "word": "01021323" + }, + "native_domains": [ + { + "accepted": 1924, + "cases": 33640, + "domain": "A-core", + "mutant_disagreements": [ + 0, + 0 + ], + "mutant_examples": [ + "", + "" + ], + "reasons": [ + 1924, + 0, + 0, + 0, + 0, + 0, + 616, + 1040, + 308, + 519, + 6084, + 120, + 280, + 502, + 8719, + 91, + 1633, + 128, + 1957, + 94, + 195, + 379, + 4108, + 22, + 1771, + 33, + 1156, + 13, + 551, + 47, + 954, + 14, + 32, + 17, + 291, + 42 + ], + "repeated_low_cases": 6728 + }, + { + "accepted": 0, + "cases": 9285, + "domain": "A-boundary", + "mutant_disagreements": [ + 0, + 0 + ], + "mutant_examples": [ + "", + "" + ], + "reasons": [ + 0, + 2140, + 3520, + 64, + 537, + 2, + 1120, + 900, + 227, + 111, + 60, + 0, + 259, + 174, + 118, + 4, + 18, + 0, + 1, + 0, + 9, + 0, + 15, + 0, + 4, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "repeated_low_cases": 1857 + }, + { + "accepted": 51305, + "cases": 520905, + "domain": "B-core", + "mutant_disagreements": [ + 1148, + 542 + ], + "mutant_examples": [ + "0001021323/0101202222/correct=1/mutant=0", + "0001203231/1111111122/correct=1/mutant=0" + ], + "reasons": [ + 51305, + 0, + 0, + 1071, + 450, + 0, + 0, + 1241, + 952, + 8458, + 34589, + 8502, + 13724, + 22853, + 71997, + 10753, + 59944, + 6564, + 10692, + 3409, + 13339, + 19880, + 58075, + 7687, + 45498, + 4341, + 24044, + 2974, + 13941, + 2687, + 4915, + 973, + 11798, + 958, + 2552, + 739 + ], + "repeated_low_cases": 453255 + }, + { + "accepted": 150, + "cases": 227997, + "domain": "B-boundary", + "mutant_disagreements": [ + 7, + 0 + ], + "mutant_examples": [ + "0102010233/0500000007/correct=1/mutant=0", + "" + ], + "reasons": [ + 150, + 52745, + 86240, + 8929, + 5588, + 503, + 0, + 31579, + 5038, + 12682, + 2984, + 1789, + 5828, + 5574, + 1842, + 487, + 1504, + 461, + 414, + 106, + 2032, + 682, + 430, + 19, + 288, + 12, + 34, + 2, + 44, + 0, + 9, + 2, + 0, + 0, + 0, + 0 + ], + "repeated_low_cases": 198387 + } + ], + "positive_controls": { + "coverage": 128, + "gauge_checks": 2816, + "projections": 176, + "repeated_low_projections": 120, + "simple24_word": [ + 0, + 1, + 0, + 2, + 0, + 1, + 0, + 5, + 2, + 3, + 4, + 3, + 6, + 3, + 4, + 3, + 5, + 3, + 4, + 3, + 6, + 3, + 4, + 3 + ] + }, + "python_controls": { + "mutant_witnesses": [ + { + "correct_accepts": true, + "correct_profile": [ + [ + 7, + 15 + ], + [ + 6, + 5 + ], + [ + 12, + 11 + ], + [ + 5, + 5 + ], + [ + 10, + 8 + ], + [ + 11, + 10 + ], + [ + 5, + 4 + ], + [ + 11, + 10 + ], + [ + 8, + 7 + ], + [ + 6, + 6 + ], + [ + 7, + 5 + ], + [ + 5, + 4 + ], + [ + 8, + 7 + ], + [ + 6, + 6 + ], + [ + 7, + 5 + ], + [ + 5, + 4 + ] + ], + "gaps": [ + 0, + 1, + 0, + 1, + 2, + 0, + 2, + 2, + 2, + 2 + ], + "low": [ + 0, + 0, + 0, + 1, + 0, + 2, + 1, + 3, + 2, + 3 + ], + "mutant_accepts": false, + "mutant_profile": [ + [ + 8, + 14 + ], + [ + 6, + 5 + ], + [ + 13, + 10 + ], + [ + 6, + 4 + ], + [ + 11, + 7 + ], + [ + 11, + 10 + ], + [ + 6, + 3 + ], + [ + 11, + 10 + ], + [ + 9, + 6 + ], + [ + 6, + 6 + ], + [ + 7, + 5 + ], + [ + 5, + 4 + ], + [ + 9, + 6 + ], + [ + 6, + 6 + ], + [ + 7, + 5 + ], + [ + 5, + 4 + ] + ], + "mutation": "reset" + }, + { + "correct_accepts": true, + "correct_profile": [ + [ + 6, + 16 + ], + [ + 13, + 13 + ], + [ + 10, + 10 + ], + [ + 10, + 10 + ], + [ + 8, + 8 + ], + [ + 5, + 5 + ], + [ + 8, + 8 + ], + [ + 8, + 8 + ], + [ + 7, + 6 + ], + [ + 5, + 5 + ], + [ + 6, + 6 + ], + [ + 6, + 6 + ], + [ + 6, + 6 + ], + [ + 5, + 5 + ], + [ + 4, + 4 + ], + [ + 4, + 4 + ] + ], + "gaps": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2 + ], + "low": [ + 0, + 0, + 0, + 1, + 2, + 0, + 3, + 2, + 3, + 1 + ], + "mutant_accepts": false, + "mutant_profile": [ + [ + 2, + 12 + ], + [ + 13, + 13 + ], + [ + 10, + 10 + ], + [ + 10, + 10 + ], + [ + 8, + 8 + ], + [ + 5, + 5 + ], + [ + 8, + 8 + ], + [ + 8, + 8 + ], + [ + 7, + 6 + ], + [ + 5, + 5 + ], + [ + 6, + 6 + ], + [ + 6, + 6 + ], + [ + 6, + 6 + ], + [ + 5, + 5 + ], + [ + 4, + 4 + ], + [ + 4, + 4 + ] + ], + "mutation": "omit" + } + ], + "source_queries": 1282 + }, + "repeated_prefix_boundary": { + "coverage": 128, + "distinct_high_states_at_low_zero": 8, + "distinct_prefixes": 23, + "gaps": [ + 7, + 7, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "interpretation": "Outside the source simple-cycle contract; not a source bug.", + "low": [ + 0, + 0, + 1, + 2, + 1, + 3, + 1, + 2, + 1, + 3 + ], + "positions_at_low_zero": 9, + "source_accepts": false, + "word": "010201030102010345464546" + }, + "schema": "connector-capacity-parity-audit/v1", + "source_impact": { + "corrected_partition": "Hamming-weight parity", + "old_calls": [ + { + "budget": 9, + "length": 18, + "pr": 2542 + }, + { + "budget": 27, + "length": 20, + "pr": 2634 + }, + { + "budget": 27, + "length": 20, + "pr": 2691 + } + ], + "old_python_engines_identical": true, + "scope": "Exact source locators and historical calibration, not fresh seven-label censuses." + }, + "sources": { + "research/connector-covering-code/README.md": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4", + "research/connector-covering-code/cycle_search.cpp": "597844fc32cde19c1d4104633fa6d3eb0d28c1ca140f8f3d2ba2cb632ecd30d1", + "research/f7-union-support-audit/README.md": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a", + "research/f7-weight-parity-census-correction/MATH.md": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a", + "research/f7-weight-parity-census-correction/engine/corrected_census.c": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a", + "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c": "b4722f59811b9920e1f364e68a228ad5ad34cf98f9c490a3655d78dc2e9ae23b", + "research/universal-f7-singleton-l20-seed06704c39/census20.py": "b403d815dad917440e238a7cafe4e15aa296f590e87c85c86653f06cba243055", + "research/universal-f7-singleton-l20-seed06704c39/engine.py": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "research/universal-f7-singleton-seedb859517b/engine.py": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "research/universal-f7-singleton-seedb859517b/search.py": "d8bad428035806848f9e0dc6caa3193e1a9abbad6a589dff3ef0e0b66f5f006c" + } +} diff --git a/research/connector-capacity-parity-audit/SOURCES.json b/research/connector-capacity-parity-audit/SOURCES.json new file mode 100644 index 0000000000..d652922b87 --- /dev/null +++ b/research/connector-capacity-parity-audit/SOURCES.json @@ -0,0 +1,110 @@ +{ + "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/connector-covering-code/README.md", + "usage": "input", + "git_blob": "c194503e34e43988d5f83fec70a6f94e89e3db5d", + "sha256": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4" + }, + { + "path": "research/connector-covering-code/cycle_search.cpp", + "usage": "input", + "git_blob": "72c8255384c117a0c616398d7982451e6f7a1021", + "sha256": "597844fc32cde19c1d4104633fa6d3eb0d28c1ca140f8f3d2ba2cb632ecd30d1" + }, + { + "path": "research/f7-union-support-audit/README.md", + "usage": "input", + "git_blob": "2c913f603f4190a15eda7fbe3def58524e0826dd", + "sha256": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "input", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "usage": "input", + "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + { + "path": "research/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-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" + } + ], + "references": [ + { + "contribution": "connector-covering-code", + "head": "e67ca5f26351e09c5bb314821633e511212f88ec", + "author": "conorholds" + }, + { + "pr": 2542, + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "author": "Aaron Wang (navinor)" + }, + { + "pr": 2634, + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "author": "Aaron Wang (navinor)" + }, + { + "pr": 2691, + "head": "88dda3534071442773106e9c0b941b9d39a3cea8", + "author": "Nicholas Stone" + }, + { + "pr": 2973, + "head": "d48f3945dbb1ef5d06835744c4082b3bd04181c0", + "author": "Nicholas Stone" + }, + { + "pr": 3005, + "head": "68e67922294d96a42f479f80fdc352eb04a9b550", + "author": "Nick Petalas" + } + ] +} diff --git a/research/connector-capacity-parity-audit/TASK.json b/research/connector-capacity-parity-audit/TASK.json new file mode 100644 index 0000000000..8dcc215372 --- /dev/null +++ b/research/connector-capacity-parity-audit/TASK.json @@ -0,0 +1,196 @@ +{ + "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": "Independently prove and test Engine::capacity in conorholds connector-covering-code at e67ca5f2: high parity, repeated low blocks, all sixteen low-linear parity changes, and the simple-only boundary. Reconstruct PR2973 calibration and trace affected predecessor word exclusions.", + "scope_change_reason": "Main already contains the tiny counterexample audit and PR3005 full independent length20 replay. One remaining implementation obligation in the newer length22 successor is more useful than reconstructing those results. This remains a bounded pruning audit, not a larger word search.", + "bottleneck_link": "A source-bound necessity proof prevents an unsound parity exclusion and distinguishes a sound simple-word filter from an unjustified revisit-aware extension. No scalar, supplier or exponent gain is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop after the one predicate proof, bounded oracle comparisons and source-impact handoff. No full length20/22 replay, high-path CSP search, literature classification validation or supplier adoption.", + "outcome": "completed", + "evidence": "Written necessary-condition proof; direct original C++ predicate versus independent position-pair enumeration on 791827 declared gap cases; actual universal simple24 projections; explicit universal repeated-prefix counterexample outside the simple contract; parity-gauge and semantic mutation controls. Finite counts are not complete word exclusions.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance with derivation, implementation, checking and writing. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can an independent implementation check the complete B length22 path exclusion, including its remaining propagation rules?", + "why_it_matters": "The successor README reports that the complete B search relies on a single native implementation; a checked capacity predicate closes only one part.", + "first_step": "Compare endpoint, equal-low disjointness and conditional-coverage propagation with explicit small path-domain tuples and planted feasible controls, then set a separate full-replay budget.", + "blocked_by": "No completeness proof or independent replay of those other rules or the published classification is supplied here." + } + ], + "scope_key": "f4a1c1da9a553967d3c6/connector-covering-code-capacity-slot-pairs", + "selection": { + "track": "adversarial-audit", + "priority_revision": 6, + "method": "Handoff-first review of discussion1166/1317 and PR2973 Open next question1; specific-card lookup after checking newer main evidence.", + "chooser_nonce": "9002c0620e3b764139af9b103bec4b66", + "existing_checks": "Catalogue existing_checks is empty, hence unknown. Inspected PR2973, PR3005, f7-bit0-false-prune and the successor existing controls before narrowing to one predicate." + }, + "research_decision": { + "milestone": "audit", + "decision": "narrow and stop after the scoped predicate audit", + "complete_cost_budget": "No new supplier or physical mechanism is proposed. Native realization, consumer, restoration, hosting and all-size costs remain outside scope rather than being set to zero." + }, + "validation": { + "environment": { + "python": "CPython 3.12.3", + "compiler": "GCC C++ 13.3.0 (Ubuntu 13.3.0-6ubuntu2~24.04.1)", + "native_flags": [ + "-std=c++17", + "-O2", + "-Wall", + "-Wextra", + "-Werror" + ], + "dependencies": "Python standard library and C++17 compiler; serial native runs" + }, + "commands": [ + { + "command": "python3 -I -B scripts/research_package.py --package research/connector-capacity-parity-audit --check-only", + "result": "PASS_PACKAGE_METADATA_AND_PINS" + }, + { + "command": "python3 -I -B scripts/research_package.py --package research/connector-capacity-parity-audit", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE research/connector-capacity-parity-audit outcome=completed; all three registered commands passed in 14.703 seconds." + }, + { + "command": "python3 -I -B research/connector-capacity-parity-audit/check_failure_controls.py", + "result": "PASS_CAPACITY_FAILURE_CONTROLS source_pin=1 native_mutants=2 malformed_query=2 receipt=1" + }, + { + "command": "c++ -std=c++17 -O1 -g -fsanitize=address,undefined -fno-omit-frame-pointer -Wall -Wextra -Werror research/connector-capacity-parity-audit/audit.cpp -o \"$audit_binary\"; \"$audit_binary\"", + "result": "All four native domain rows match RESULT.json; no sanitizer diagnostics. audit_binary is a caller-chosen temporary path." + } + ], + "counts": { + "native_gap_cases": 791827, + "capacity_accepts": 53379, + "simple_universal_projections": 176, + "repeated_low_positive_projections": 120, + "gauge_checks": 2816, + "separate_python_queries": 1282, + "universal_nonsimple_boundary_controls": 1 + }, + "not_checked": [ + "Complete n7 length18/20 replays", + "Complete simple22 word/CSP enumeration", + "Completeness of low-orbit and high-path catalogues", + "Other source propagation rules and classification/non-simple reductions", + "Published coding/classification proofs", + "Supplier, selected frontier and all-size multiplication obligations", + "Hosted CI, proof-assistant or independent human review" + ], + "exact_predecessor_head_comparisons": [ + { + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "result": "byte-identical to pinned main input" + }, + { + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "path": "research/universal-f7-singleton-seedb859517b/search.py", + "result": "byte-identical to pinned main input" + }, + { + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "result": "byte-identical to pinned main input" + }, + { + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "path": "research/universal-f7-singleton-l20-seed06704c39/census20.py", + "result": "byte-identical to pinned main input" + }, + { + "head": "88dda3534071442773106e9c0b941b9d39a3cea8", + "path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c", + "result": "byte-identical to pinned main input" + }, + { + "head": "d48f3945dbb1ef5d06835744c4082b3bd04181c0", + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "result": "byte-identical to pinned main input" + }, + { + "head": "68e67922294d96a42f479f80fdc352eb04a9b550", + "path": "research/f7-union-support-audit/README.md", + "result": "byte-identical to pinned main input" + }, + { + "head": "e67ca5f26351e09c5bb314821633e511212f88ec", + "path": "research/connector-covering-code/cycle_search.cpp", + "result": "byte-identical to pinned main input" + } + ] + }, + "coordination": { + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317", + "handoff": "PR2973 Open next question1, as answered by the newer main successor e67ca5f26351e09c5bb314821633e511212f88ec", + "status": "Claim is in discussion #1317; artifact remains local-only pending publication.", + "overlap_queries": [ + "--task census-pruning-audit", + "connector-covering-code / parity capacity" + ], + "snapshot": { + "open_prs_fetched_at": "2026-10-17T17:37:12.534077+00:00", + "open_prs_records": 251, + "discussions_fetched_at": "2026-10-17T17:39:04.580509+00:00", + "discussion_records": 2015, + "complete_pagination": true, + "limitation": "Offline snapshot can miss later changes; no novelty certificate." + }, + "nearby_work": "PR2973 correction; PR3005 full independent word replay; jwr tiny audit; concurrent actual-size PR2542 joint_covers audit. This audit concerns the successor capacity rule and its simple-only boundary.", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19001874", + "upstream_checkpoint": { + "commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "checked_at": "2026-10-17T17:44:27Z", + "priority_revision": 6, + "result": "Canonical main unchanged from the starting base; no guidance, selected-record or scientific-input changes. Preserve original source pins." + } + } +} diff --git a/research/connector-capacity-parity-audit/VERIFY.json b/research/connector-capacity-parity-audit/VERIFY.json new file mode 100644 index 0000000000..b8e5f15852 --- /dev/null +++ b/research/connector-capacity-parity-audit/VERIFY.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-covering-code/README.md", + "research/connector-covering-code/cycle_search.cpp", + "research/f7-union-support-audit/README.md", + "research/f7-weight-parity-census-correction/MATH.md", + "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-seedb859517b/engine.py", + "research/universal-f7-singleton-seedb859517b/search.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Source pins; actual C++ capacity versus slot oracle; complete bounded gap domains; true universal positives; repeated-prefix boundary; historical calibration and mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Same complete bounded audit with Python assertions disabled; all require checks remain active." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check_failure_controls.py" + ], + "timeout_seconds": 300, + "checks": "Private-copy source hash and fresh-receipt corruption rejection under -O; actual compiled parity-reset and fiber-cap mutations; truncated native query rejection." + } + ] +} diff --git a/research/connector-capacity-parity-audit/audit.cpp b/research/connector-capacity-parity-audit/audit.cpp new file mode 100644 index 0000000000..4ba91bbb49 --- /dev/null +++ b/research/connector-capacity-parity-audit/audit.cpp @@ -0,0 +1,175 @@ +// Prepared for commdata2338, with substantial OpenAI Codex assistance. +// Apache-2.0. The included predecessor retains conorholds' attribution. +// Execute its actual predicate; do not copy or patch its implementation. +#define main predecessor_main +#include "../connector-covering-code/cycle_search.cpp" +#undef main + +namespace audit { +using Profile = std::array, 16>; +struct Slot { int low, side, block; }; +struct Result { + bool accepted; + int reason; + Profile profile{}; +}; + +void require(bool condition, const std::string& message) { + if (!condition) throw std::runtime_error(message); +} + +// Definition-level oracle: list positions, then enumerate unordered pairs. +// No source parity routine, source low_points, or aggregated product formula. +Result oracle(const LowWord& low, const LowWord& gaps, int mutant = 0) { + require(low.size() == gaps.size(), "oracle length mismatch"); + std::vector slots; + std::array occupied{}; + int point = 0, side = 0; + bool oversized_block = false; + for (size_t block = 0; block < low.size(); ++block) { + require(gaps[block] >= 0 && gaps[block] <= 8, "oracle gap outside audit domain"); + oversized_block |= gaps[block] > 7; + if (mutant == 1) side = 0; // Wrong: reset at every low step. + for (int step = 0; step <= gaps[block]; ++step) { + slots.push_back({point, side, static_cast(block)}); + ++occupied[point]; + if (step < gaps[block]) side = 1 - side; + } + point ^= 1 << low[block]; + } + require(point == 0, "oracle low projection not restored"); + Result result{false, 0, {}}; + for (size_t i = 0; i < slots.size(); ++i) + for (size_t j = i + 1; j < slots.size(); ++j) { + const auto& a = slots[i]; const auto& b = slots[j]; + if (mutant == 2 && a.low == b.low && a.block != b.block) continue; + ++result.profile[a.low ^ b.low][a.side ^ b.side]; + } + if (oversized_block) { result.reason = 1; return result; } + // Restore testing uses the actual total high-step count, even for mutants. + if (std::accumulate(gaps.begin(), gaps.end(), 0) % 2) { result.reason = 2; return result; } + for (int count : occupied) if (count > 8) { result.reason = 3; return result; } + for (int difference = 0; difference < 16; ++difference) + for (int bit = 0; bit < 2; ++bit) { + int needed = difference == 0 && bit == 0 ? 3 : 4; + if (result.profile[difference][bit] < needed) { + result.reason = 4 + 2 * difference + bit; + return result; + } + } + result.accepted = true; + return result; +} + +std::string digits(const LowWord& value) { + std::string out; + for (int x : value) out += static_cast('0' + x); + return out; +} + +struct CountsAudit { + uint64_t cases = 0, accepted = 0, repeated_low = 0; + std::array reasons{}; + std::array mutant_disagreements{}; + std::array mutant_examples{}; + void check(const Engine& engine, const LowWord& gaps) { + auto expected = oracle(engine.low_word, gaps); + bool actual = engine.capacity(gaps); + require(actual == expected.accepted, + "capacity mismatch low=" + digits(engine.low_word) + " gaps=" + digits(gaps)); + ++cases; accepted += actual; ++reasons[expected.reason]; + std::set low_points; int point = 0; + for (int label : engine.low_word) { low_points.insert(point); point ^= 1 << label; } + repeated_low += low_points.size() < engine.low_word.size(); + for (int mutant = 1; mutant <= 2; ++mutant) { + auto changed = oracle(engine.low_word, gaps, mutant); + if (changed.accepted == actual) continue; + ++mutant_disagreements[mutant - 1]; + if (mutant_examples[mutant - 1].empty()) + mutant_examples[mutant - 1] = digits(engine.low_word) + "/" + digits(gaps) + + "/correct=" + std::to_string(actual) + "/mutant=" + std::to_string(changed.accepted); + } + } + void print(const std::string& name) const { + std::cout << "{\"domain\":\"" << name << "\",\"cases\":" << cases + << ",\"accepted\":" << accepted << ",\"repeated_low_cases\":" << repeated_low + << ",\"reasons\":["; + for (size_t i = 0; i < reasons.size(); ++i) std::cout << (i ? "," : "") << reasons[i]; + std::cout << "],\"mutant_disagreements\":[" << mutant_disagreements[0] + << ',' << mutant_disagreements[1] << "],\"mutant_examples\":[\"" + << mutant_examples[0] << "\",\"" << mutant_examples[1] << "\"]}\n"; + } +}; + +// Complete bounded composition domain. This enumerates gap vectors only; +// no high paths, source words, or CSP search are generated. +void compositions(const Engine& engine, int cap, int total, CountsAudit& count) { + LowWord gaps(engine.blocks); + std::function visit = [&](int position, int remaining) { + if (position == engine.blocks) { + if (remaining == 0) count.check(engine, gaps); + return; + } + for (int next = 0; next <= cap; ++next) { + int left = remaining - next; + if (left < 0 || left > cap * (engine.blocks - position - 1)) continue; + gaps[position] = next; visit(position + 1, left); + } + }; + visit(0, total); +} + +void bounded_domains(const Tables& tables) { + for (bool b : {false, true}) { + CountsAudit core, boundary; + auto low_words = universal_templates(b); + for (const auto& low : low_words) { + Engine engine(tables, low, b ? Counts{4,4,4} : Counts{6,4,4}, Clock::time_point::max()); + compositions(engine, b ? 2 : 3, b ? 12 : 14, core); + // Exactly zero, one, or two nonzero gaps, each 1..8. This reaches + // both sides of the eight-state capacity and odd-restoration guards. + LowWord gaps(low.size()); boundary.check(engine, gaps); + for (int i = 0; i < engine.blocks; ++i) for (int x = 1; x <= 8; ++x) { + gaps[i] = x; boundary.check(engine, gaps); + for (int j = i + 1; j < engine.blocks; ++j) for (int y = 1; y <= 8; ++y) { + gaps[j] = y; boundary.check(engine, gaps); gaps[j] = 0; + } + gaps[i] = 0; + } + } + core.print(b ? "B-core" : "A-core"); + boundary.print(b ? "B-boundary" : "A-boundary"); + } +} + +// Query mode lets a separately written Python oracle check the compiled +// source without importing any algorithm above. Bounded, nonnegative inputs. +void query(const Tables& tables) { + std::string low_text, gap_text; + size_t count = 0; + while (std::cin >> low_text) { + require(static_cast(std::cin >> gap_text), "missing gap vector"); + require(++count <= 10000, "query cap exceeded"); + require(low_text.size() == gap_text.size() && low_text.size() <= 10, "invalid query length"); + LowWord low, gaps; + for (char c : low_text) { require(c >= '0' && c <= '3', "invalid low label"); low.push_back(c - '0'); } + for (char c : gap_text) { require(c >= '0' && c <= '8', "invalid gap"); gaps.push_back(c - '0'); } + Engine engine(tables, low, Counts{0,0,0}, Clock::time_point::max()); + std::cout << engine.capacity(gaps) << '\n'; + } + require(std::cin.eof(), "query input failure"); +} +} // namespace audit + +int main(int argc, char** argv) { + try { + const Tables tables; + if (argc == 2 && std::string(argv[1]) == "--query") audit::query(tables); + else if (argc == 1) audit::bounded_domains(tables); + else throw std::runtime_error("usage: audit [--query]"); + return 0; + } catch (const std::exception& error) { + std::cerr << "FAIL_CAPACITY_AUDIT " << error.what() << '\n'; + return 1; + } +} diff --git a/research/connector-capacity-parity-audit/check_failure_controls.py b/research/connector-capacity-parity-audit/check_failure_controls.py new file mode 100644 index 0000000000..82350572ee --- /dev/null +++ b/research/connector-capacity-parity-audit/check_failure_controls.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Reproduce source, receipt and predicate mutation controls in a private copy. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = Path("research/connector-covering-code/cycle_search.cpp") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def execute(argv, *, data=None, timeout=120): + return subprocess.run(argv, input=data, text=True, capture_output=True, + check=False, timeout=timeout) + + +def failure(result, diagnostic): + require(result.returncode != 0 and diagnostic in result.stderr + result.stdout, + "failure control did not reject as expected: " + diagnostic) + + +def main(): + compiler = shutil.which(os.environ.get("CXX", "c++")) + require(compiler is not None, "C++17 compiler required") + manifest = json.loads((HERE / "VERIFY.json").read_text()) + with tempfile.TemporaryDirectory(prefix="capacity-controls-") as temp: + root = Path(temp) + package = root / HERE.relative_to(ROOT) + shutil.copytree(HERE, package) + for name in manifest["inputs"]: + dest = root / name + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, dest) + source = root / NATIVE + original = source.read_text() + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + # A source change must reject before compilation, regardless of mode. + source.write_text(original + "\n// mutation control\n") + failure(execute(command, timeout=15), "source digest mismatch") + source.write_text(original) + + # Compile the actual altered predicate, not merely a changed oracle. + mutations = [ + ("reset", "high_parity ^= gaps[i] & 1;", "high_parity = 0;", + "0001021323 0101202222\n", "0\n"), + ("fiber_cap", "if (sizes[point] > 8) return false;", + "if (sizes[point] > 9) return false;", "0012131213 7700000000\n", "1\n"), + ] + for name, old, new, data, expected in mutations: + require(original.count(old) == 1, "ambiguous source mutation: " + name) + source.write_text(original.replace(old, new)) + binary = root / name + built = execute([compiler, "-std=c++17", "-O2", "-Wall", "-Wextra", "-Werror", + str(package / "audit.cpp"), "-o", str(binary)], timeout=60) + require(built.returncode == 0, "mutant compilation failed: " + built.stderr) + result = execute([str(binary), "--query"], data=data, timeout=20) + require(result.returncode == 0 and result.stdout == expected and not result.stderr, + "actual native mutation did not discriminate: " + name) + failure(execute([str(binary), "--query"], data="01021323\n", timeout=20), + "missing gap vector") + source.write_text(original) + + # A valid source replay must reject a plausible but altered receipt. + receipt_path = package / "RESULT.json" + receipt = json.loads(receipt_path.read_text()) + receipt["native_domains"][0]["accepted"] += 1 + receipt_path.write_text(json.dumps(receipt)) + failure(execute(command, timeout=180), "receipt differs from fresh checks") + print("PASS_CAPACITY_FAILURE_CONTROLS source_pin=1 native_mutants=2 malformed_query=2 receipt=1") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, subprocess.SubprocessError) as error: + raise SystemExit("FAIL_CAPACITY_FAILURE_CONTROLS " + str(error)) from error diff --git a/research/connector-capacity-parity-audit/verify.py b/research/connector-capacity-parity-audit/verify.py new file mode 100644 index 0000000000..77cbca8d91 --- /dev/null +++ b/research/connector-capacity-parity-audit/verify.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +"""Audit one pinned capacity filter, not the complete f(7) exclusion. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import hashlib +import itertools +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/connector-covering-code/cycle_search.cpp" +POSITIVE = (0, 1, 0, 2, 0, 1, 0, 5, 2, 3, 4, 3, + 6, 3, 4, 3, 5, 3, 4, 3, 6, 3, 4, 3) +MUTANTS = ( + ((0, 0, 0, 1, 0, 2, 1, 3, 2, 3), (0, 1, 0, 1, 2, 0, 2, 2, 2, 2), "reset"), + ((0, 0, 0, 1, 2, 0, 3, 2, 3, 1), (1, 1, 1, 1, 1, 1, 1, 1, 2, 2), "omit"), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def live_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + checked = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + actual = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(actual == row["sha256"], "source digest mismatch: " + row["path"]) + checked[row["path"]] = actual + require(str(SOURCE.relative_to(ROOT)) in checked, "native source is not pinned") + return checked + + +def run(command, *, input_text=None, timeout=120): + result = subprocess.run(command, input=input_text, text=True, capture_output=True, + timeout=timeout, check=False) + require(result.returncode == 0, + "command failed: " + " ".join(map(str, command)) + "\n" + result.stderr[-3000:]) + require(not result.stderr, "unexpected native diagnostics: " + result.stderr[-3000:]) + return result.stdout + + +def prefix_points(word): + state = 0 + points = [] + for label in word: + points.append(state) + state ^= 1 << label + return points, state + + +def historical_control(): + points, final = prefix_points((0, 1, 0, 2, 1, 3, 2, 3)) + require(points == [0, 1, 3, 2, 6, 4, 12, 8] and final == 0, "tiny walk differs") + require(len({a ^ b for a in points for b in points}) == 16, "tiny cover fails") + results = {} + for name, functional in (("bit0", lambda x: x & 1), + ("weight", lambda x: x.bit_count() % 2)): + sides = [[p for p in points if functional(p) == side] for side in (0, 1)] + excess = sum(len(side) * (len(side) - 1) // 2 + - len({a ^ b for a, b in itertools.combinations(side, 2)}) + for side in sides) + actual_budget = sum(len(side) * (len(side) - 1) // 2 for side in sides) - 7 + results[name] = {"sizes": list(map(len, sides)), "excess": excess, + "actual_budget": actual_budget} + require(results == {"bit0": {"sizes": [6, 2], "excess": 8, "actual_budget": 9}, + "weight": {"sizes": [4, 4], "excess": 0, "actual_budget": 5}}, + "historical parity calibration differs") + return {"word": "01021323", "prefixes": points, "coverage": 16, + "balanced_budget": 5, "partitions": results} + + +def source_impact(): + old = (ROOT / "research/universal-f7-singleton-seedb859517b/engine.py").read_bytes() + vendor = (ROOT / "research/universal-f7-singleton-l20-seed06704c39/engine.py").read_bytes() + require(old == vendor and b"elif nq & 1:" in old, "old Python partition binding differs") + call18 = (ROOT / "research/universal-f7-singleton-seedb859517b/search.py").read_text() + call20 = (ROOT / "research/universal-f7-singleton-l20-seed06704c39/census20.py").read_text() + old_c = (ROOT / "research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c").read_text() + corrected = (ROOT / "research/f7-weight-parity-census-correction/engine/corrected_census.c").read_text() + require("cyclic_census(7, 18, budget=9, simple=True" in call18, "length18 caller differs") + require("cyclic_census(7, 20, budget=27, simple=True" in call20, "length20 caller differs") + require("if (nq & 1)" in old_c and "#define BUDGET 27" in old_c, "old C rule differs") + require("int p=parity(nq)" in corrected and "__builtin_popcount((unsigned)x)&1" in corrected, + "corrected partition binding differs") + return {"old_python_engines_identical": True, + "old_calls": [{"pr": 2542, "length": 18, "budget": 9}, + {"pr": 2634, "length": 20, "budget": 27}, + {"pr": 2691, "length": 20, "budget": 27}], + "corrected_partition": "Hamming-weight parity", + "scope": "Exact source locators and historical calibration, not fresh seven-label censuses."} + + +def slot_profile(low, gaps, *, gauge=0, mutant=None): + """Literal time positions and unordered pairs; no aggregate formula.""" + require(len(low) == len(gaps), "slot length mismatch") + points, final = prefix_points(low) + require(final == 0, "unrestored low word") + slots = [] + elapsed_high = 0 + for block, (point, gap) in enumerate(zip(points, gaps)): + require(0 <= gap <= 8, "gap outside audit domain") + start = 0 if mutant == "reset" else elapsed_high + slots.extend((point, ((start + offset) % 2) ^ ((point & gauge).bit_count() % 2), block) + for offset in range(gap + 1)) + elapsed_high += gap + profile = [[0, 0] for _ in range(16)] + for a, b in itertools.combinations(slots, 2): + if mutant == "omit" and a[0] == b[0] and a[2] != b[2]: + continue + profile[a[0] ^ b[0]][a[1] ^ b[1]] += 1 + counts = [sum(slot[0] == point for slot in slots) for point in range(16)] + accepted = (max(gaps) <= 7 and elapsed_high % 2 == 0 and max(counts) <= 8 + and all(value >= (3 if (d, side) == (0, 0) else 4) + for d, row in enumerate(profile) for side, value in enumerate(row))) + return accepted, profile + + +def projection(word, high): + low_coordinates = [label for label in range(7) if label not in high] + low, gaps, gap = [], [], 0 + for label in word: + if label in high: + gap += 1 + else: + low.append(low_coordinates.index(label)) + gaps.append(gap) + gap = 0 + require(gap == 0, "projection must end in a low step") + return tuple(low), tuple(gaps) + + +def query(executable, cases): + data = "".join("".join(map(str, low)) + " " + "".join(map(str, gaps)) + "\n" + for low, gaps in cases) + lines = run([str(executable), "--query"], input_text=data).splitlines() + require(len(lines) == len(cases) and all(x in ("0", "1") for x in lines), + "malformed or incomplete query response") + return [line == "1" for line in lines] + + +def positive_and_gauge_controls(executable): + points, final = prefix_points(POSITIVE) + require(final == 0 and len(set(points)) == 24, "positive is not a simple restored24") + require(len({x ^ y for x in points for y in points}) == 128, "positive is not universal") + cases = [] + gauge_checks = repeated = 0 + for high in itertools.combinations(range(7), 3): + if sum(label not in high for label in POSITIVE) > 10: + continue + for base in (POSITIVE, POSITIVE[::-1]): + for rotation in range(24): + word = base[rotation:] + base[:rotation] + if word[-1] in high: + continue + low, gaps = projection(word, high) + baseline, profile = slot_profile(low, gaps) + require(baseline, "capacity oracle rejects universal positive") + for gauge in range(16): + accepted, changed = slot_profile(low, gaps, gauge=gauge) + require(accepted == baseline, "gauge changed capacity verdict") + for d in range(16): + flip = (d & gauge).bit_count() % 2 + require(changed[d] == [profile[d][flip], profile[d][1 ^ flip]], + "gauge bucket permutation failed") + gauge_checks += 1 + cases.append((low, gaps)) + repeated += len(set(prefix_points(low)[0])) < len(low) + require(len(cases) == 176 and all(query(executable, cases)), "source rejects positive projection") + return {"simple24_word": list(POSITIVE), "coverage": 128, "projections": len(cases), + "repeated_low_projections": repeated, "gauge_checks": gauge_checks} + + +def bounded_python_controls(executable): + # Two declared complete 0/1-gap cubes, unrelated to the source traversal. + lows = ((0, 1, 0, 2, 1, 3, 2, 3), MUTANTS[0][0]) + cases = [(low, gap) for low in lows for gap in itertools.product(range(2), repeat=len(low))] + cases += [(low, gaps) for low, gaps, _ in MUTANTS] + expected = [slot_profile(low, gaps)[0] for low, gaps in cases] + require(query(executable, cases) == expected, "Python/source differential mismatch") + witness_receipts = [] + for low, gaps, mutation in MUTANTS: + good, profile = slot_profile(low, gaps) + bad, changed = slot_profile(low, gaps, mutant=mutation) + require(good and not bad, "semantic mutation witness stopped discriminating") + witness_receipts.append({"mutation": mutation, "low": list(low), "gaps": list(gaps), + "correct_profile": profile, "mutant_profile": changed, + "correct_accepts": good, "mutant_accepts": bad}) + return {"source_queries": len(cases), "mutant_witnesses": witness_receipts} + + +def repeated_prefix_boundary(executable): + # PR1185's retained upper witness: a real universal word outside the + # simple-cycle contract. Position counts are not distinct-state counts. + word = tuple(map(int, "010201030102010345464546")) + points, final = prefix_points(word) + require(final == 0 and len(set(points)) == 23, "repeated-prefix witness differs") + require(len({x ^ y for x in points for y in points}) == 128, "repeated word not universal") + low, gaps = projection(word, (0, 1, 2)) + low_points, _ = prefix_points(low) + positions_at_zero = sum(gaps[i] + 1 for i, point in enumerate(low_points) if point == 0) + distinct_at_zero = len({p & 7 for p in points if p >> 3 == 0}) + require((positions_at_zero, distinct_at_zero) == (9, 8), "fiber multiplicity control differs") + require(not slot_profile(low, gaps)[0] and query(executable, [(low, gaps)]) == [False], + "simple-only guard no longer rejects the repeated-prefix control") + return {"word": "".join(map(str, word)), "coverage": 128, "distinct_prefixes": 23, + "low": list(low), "gaps": list(gaps), "positions_at_low_zero": positions_at_zero, + "distinct_high_states_at_low_zero": distinct_at_zero, "source_accepts": False, + "interpretation": "Outside the source simple-cycle contract; not a source bug."} + + +def expected_cases(blocks, cap, total): + # Generating-function coefficients, independent of the native recursion. + coefficients = [1] + for _ in range(blocks): + coefficients = [sum(coefficients[i - j] for j in range(cap + 1) + if 0 <= i - j < len(coefficients)) + for i in range(len(coefficients) + cap)] + return coefficients[total] + + +def native_checks(executable): + rows = [json.loads(line) for line in run([str(executable)]).splitlines()] + require([row["domain"] for row in rows] == ["A-core", "A-boundary", "B-core", "B-boundary"], + "native domain inventory mismatch") + core = {"A": 5 * expected_cases(8, 3, 14), "B": 77 * expected_cases(10, 2, 12)} + for row in rows: + family, kind = row["domain"].split("-") + blocks, orbits = (8, 5) if family == "A" else (10, 77) + expected = (core[family] if kind == "core" else + orbits * (1 + 8 * blocks + 64 * blocks * (blocks - 1) // 2)) + require(row["cases"] == expected, "incomplete native domain") + require(sum(row["reasons"]) == expected and row["accepted"] == row["reasons"][0], + "native reason counts disagree") + require(all(rows[2]["mutant_disagreements"]), "B mutation controls are vacuous") + require(rows[2]["accepted"] > 0 and rows[2]["repeated_low_cases"] > 0, "vacuous B domain") + return rows + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", action="store_true", help="explicitly regenerate RESULT.json") + args = parser.parse_args() + sources = live_sources() + compiler = shutil.which(os.environ.get("CXX", "c++")) + require(compiler is not None, "C++17 compiler required") + with tempfile.TemporaryDirectory(prefix="connector-capacity-audit-") as temp: + executable = Path(temp) / "audit" + run([compiler, "-std=c++17", "-O2", "-Wall", "-Wextra", "-Werror", + str(HERE / "audit.cpp"), "-o", str(executable)], timeout=60) + receipt = {"schema": "connector-capacity-parity-audit/v1", "sources": sources, + "historical_control": historical_control(), + "source_impact": source_impact(), + "native_domains": native_checks(executable), + "positive_controls": positive_and_gauge_controls(executable), + "python_controls": bounded_python_controls(executable), + "repeated_prefix_boundary": repeated_prefix_boundary(executable)} + destination = HERE / "RESULT.json" + if args.write_receipt: + destination.write_text(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + else: + require(receipt == json.loads(destination.read_text()), "receipt differs from fresh checks") + cases = sum(row["cases"] for row in receipt["native_domains"]) + accepted = sum(row["accepted"] for row in receipt["native_domains"]) + print(f"PASS_CONNECTOR_CAPACITY_PARITY cases={cases} accepted={accepted} " + "positive_projections=176 gauges=2816 python_queries=1282 repeated_prefix_control=1 no_full_census") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError, subprocess.SubprocessError) as error: + raise SystemExit("FAIL_CONNECTOR_CAPACITY_PARITY " + str(error)) from error