From 68e67922294d96a42f479f80fdc352eb04a9b550 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 18:00:30 +0100 Subject: [PATCH] test(research): independently replay seven-label exclusion --- .../f7-union-support-audit/ENVIRONMENT.json | 74 ++++ research/f7-union-support-audit/FULL.json | 118 +++++ research/f7-union-support-audit/QUICK.json | 411 ++++++++++++++++++ research/f7-union-support-audit/README.md | 256 +++++++++++ research/f7-union-support-audit/SOURCES.json | 42 ++ research/f7-union-support-audit/TASK.json | 106 +++++ research/f7-union-support-audit/VERIFY.json | 31 ++ research/f7-union-support-audit/census.cpp | 201 +++++++++ research/f7-union-support-audit/oracle.py | 90 ++++ research/f7-union-support-audit/ruff.toml | 4 + research/f7-union-support-audit/verify.py | 208 +++++++++ 11 files changed, 1541 insertions(+) create mode 100644 research/f7-union-support-audit/ENVIRONMENT.json create mode 100644 research/f7-union-support-audit/FULL.json create mode 100644 research/f7-union-support-audit/QUICK.json create mode 100644 research/f7-union-support-audit/README.md create mode 100644 research/f7-union-support-audit/SOURCES.json create mode 100644 research/f7-union-support-audit/TASK.json create mode 100644 research/f7-union-support-audit/VERIFY.json create mode 100644 research/f7-union-support-audit/census.cpp create mode 100644 research/f7-union-support-audit/oracle.py create mode 100644 research/f7-union-support-audit/ruff.toml create mode 100644 research/f7-union-support-audit/verify.py diff --git a/research/f7-union-support-audit/ENVIRONMENT.json b/research/f7-union-support-audit/ENVIRONMENT.json new file mode 100644 index 0000000000..efde3ec395 --- /dev/null +++ b/research/f7-union-support-audit/ENVIRONMENT.json @@ -0,0 +1,74 @@ +{ + "platform": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41", + "python": "3.12.15", + "compilers": { + "c++": "c++ (Debian 14.2.0-19) 14.2.0\nCopyright (C) 2024 Free Software Foundation, Inc.\nThis is free software; see the source for copying conditions. There is NO\nwarranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.\n\n", + "clang++": "Debian clang version 19.1.7 (3+b1)\nTarget: x86_64-pc-linux-gnu\nThread model: posix\nInstalledDir: /usr/lib/llvm-19/bin\n" + }, + "runs": [ + { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/f7-union-support-audit" + ], + "exit": 0, + "stdout": "CHECK Fresh C++20 build; tiny historical false prune; 270 exact word-set/oracle comparisons over eight complete small domains; 12 cap/error controls; four compiled mutants; UBSan/bounds complete comparison. Requires an installed C++20 compiler.\nPASS_F7_INDEPENDENT_QUICK\nCHECK Fresh C++20 build and six uncapped n=7 traversals from the empty prefix, exact comparison of all non-timing fields with FULL.json, empty witness files and successful completion.\nPASS_F7_INDEPENDENT_FULL\nPASS_REGISTERED_RESEARCH_PACKAGE research/f7-union-support-audit outcome=completed\n", + "stderr": "", + "seconds": 114.977 + }, + { + "argv": [ + "python3.12", + "-I", + "-O", + "-Werror", + "-B", + "research/f7-union-support-audit/verify.py", + "--compiler", + "clang++" + ], + "exit": 0, + "stdout": "PASS_F7_INDEPENDENT_QUICK\n", + "stderr": "", + "seconds": 5.775 + }, + { + "argv": [ + "python3.12", + "-I", + "-O", + "-Werror", + "-B", + "research/f7-union-support-audit/verify.py", + "--full", + "--compiler", + "clang++" + ], + "exit": 0, + "stdout": "PASS_F7_INDEPENDENT_FULL\n", + "stderr": "", + "seconds": 86.861 + } + ], + "native_source_sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949", + "build_flags": [ + "-std=c++20", + "-O3", + "-Wall", + "-Wextra", + "-Wpedantic", + "-Wconversion", + "-Wsign-conversion", + "-Wshadow", + "-Werror" + ], + "sanitizer_flags": [ + "-O1", + "-fsanitize=undefined,bounds", + "-fno-sanitize-recover=all" + ], + "note": "Both complete receipts are compared exactly. Timings are local command wall times, not a comparative benchmark. Subsequent tuple-unpacking/import-lint edits were rechecked by the quick command without changing census.cpp." +} diff --git a/research/f7-union-support-audit/FULL.json b/research/f7-union-support-audit/FULL.json new file mode 100644 index 0000000000..4399bff28b --- /dev/null +++ b/research/f7-union-support-audit/FULL.json @@ -0,0 +1,118 @@ +{ + "cases": [ + { + "attempts": 2260000903, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 15112797, + "entered": 322881109, + "hits": 0, + "length": 20, + "n": 7, + "prune": true, + "restoration_prunes": 783614111, + "same_prunes": 838232725, + "size_prunes": 300160162, + "split": [ + 10, + 10 + ] + }, + { + "attempts": 785502139, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 5126921, + "entered": 112232469, + "hits": 0, + "length": 20, + "n": 7, + "prune": true, + "restoration_prunes": 150127584, + "same_prunes": 400234383, + "size_prunes": 117780783, + "split": [ + 10, + 9 + ] + }, + { + "attempts": 42550772, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 566106, + "entered": 6082255, + "hits": 0, + "length": 20, + "n": 7, + "prune": true, + "restoration_prunes": 2265584, + "same_prunes": 26552511, + "size_prunes": 7084317, + "split": [ + 10, + 8 + ] + }, + { + "attempts": 100157693, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 2452, + "entered": 14322217, + "hits": 0, + "length": 20, + "n": 7, + "prune": true, + "restoration_prunes": 4709034, + "same_prunes": 65136566, + "size_prunes": 15987425, + "split": [ + 9, + 9 + ] + }, + { + "attempts": 174540, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 0, + "entered": 25087, + "hits": 0, + "length": 20, + "n": 7, + "prune": true, + "restoration_prunes": 0, + "same_prunes": 117261, + "size_prunes": 32193, + "split": [ + 10, + 7 + ] + }, + { + "attempts": 1675590, + "candidate_leaves": 0, + "cap": 0, + "complete": true, + "cross_prunes": 0, + "entered": 239661, + "hits": 0, + "length": 18, + "n": 7, + "prune": true, + "restoration_prunes": 71026, + "same_prunes": 1082685, + "size_prunes": 282219, + "split": [ + 9, + 9 + ] + } + ] +} diff --git a/research/f7-union-support-audit/QUICK.json b/research/f7-union-support-audit/QUICK.json new file mode 100644 index 0000000000..97cfdd3681 --- /dev/null +++ b/research/f7-union-support-audit/QUICK.json @@ -0,0 +1,411 @@ +{ + "failure_controls": 12, + "fixtures": { + "counterexample": { + "bit0_split": [ + 6, + 2 + ], + "coverage": 16, + "path": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8 + ], + "simple": true, + "split": [ + 4, + 4 + ], + "weight_budget": 5, + "wrong_excess": 8 + }, + "l20_splits": [ + [ + 9, + 9 + ], + [ + 10, + 7 + ], + [ + 10, + 8 + ], + [ + 10, + 9 + ], + [ + 10, + 10 + ] + ], + "l24_upper_word": "010201030102010345464546" + }, + "historical_control": { + "bit0_budget_5": { + "hits": 0, + "leaves": 0, + "nodes": 7, + "words": [] + }, + "without_budget": { + "hits": 1, + "leaves": 1, + "nodes": 9, + "words": [ + [ + 0, + 1, + 0, + 2, + 1, + 3, + 2, + 3 + ] + ] + } + }, + "rejected_mutants": 4, + "sanitized_case": [ + 4, + 10 + ], + "small_domains": [ + { + "comparisons": 8, + "hits_by_split": [ + { + "hits": 1, + "split": [ + 1, + 2 + ], + "words_sha256": "70a9fe6fedbafdbbc1714543d259da1ff147f45de03fccf15f9e43e9d53f2bd7" + }, + { + "hits": 1, + "split": [ + 2, + 1 + ], + "words_sha256": "baac6c1bb1baceeaf9d975c84efad4dc9f5cdbee48bb956178cd7c2939c5e9b5" + }, + { + "hits": 1, + "split": [ + 2, + 2 + ], + "words_sha256": "df757987c3815022a626f713d53e06655b746a907733d792263c18bb1cb49345" + } + ], + "length": 4, + "n": 2, + "restored": 3, + "simple_universal_wrong_bit0_rejections": 0, + "universal": 3 + }, + { + "comparisons": 8, + "hits_by_split": [ + { + "hits": 3, + "split": [ + 1, + 2 + ], + "words_sha256": "15eb778d306bfaf1dc93051233d093da40d3b57fda4cc99a452a6958113c806b" + }, + { + "hits": 3, + "split": [ + 2, + 1 + ], + "words_sha256": "9993f9a370028c231c073f5dc214ed181590563cc82b06fb9047dff58cd4fd61" + }, + { + "hits": 9, + "split": [ + 2, + 2 + ], + "words_sha256": "c6fc70d009bd2d89affab095507cc27b0e8f1aba18980f915c6e6aeac734dd9b" + } + ], + "length": 6, + "n": 2, + "restored": 15, + "simple_universal_wrong_bit0_rejections": 0, + "universal": 15 + }, + { + "comparisons": 18, + "hits_by_split": [ + { + "hits": 3, + "split": [ + 2, + 3 + ], + "words_sha256": "5edba4d812b050f621519820edd4d4ca7646ecc89f946c950ce9f0c837c457a9" + }, + { + "hits": 3, + "split": [ + 3, + 2 + ], + "words_sha256": "a9a07f399bcd1826064148e993cf781e2175759e6044fd0af8817afc141256e7" + }, + { + "hits": 4, + "split": [ + 3, + 3 + ], + "words_sha256": "af0f54f461676d1e44f409918a5b330f01f6d5da796fe68e7604f74e21d5baaf" + } + ], + "length": 6, + "n": 3, + "restored": 15, + "simple_universal_wrong_bit0_rejections": 0, + "universal": 10 + }, + { + "comparisons": 32, + "hits_by_split": [ + { + "hits": 42, + "split": [ + 2, + 3 + ], + "words_sha256": "23d4029930d5c5bac4ac13021f0739f59a36a33f385dec4c489d76f2c0e681a2" + }, + { + "hits": 2, + "split": [ + 2, + 4 + ], + "words_sha256": "e1b4aa3215396f2a7fbcf813eb1131cc06482edcd2d12471767da1030ad77322" + }, + { + "hits": 42, + "split": [ + 3, + 2 + ], + "words_sha256": "ca71d1e842ab82a3efd317f06b40fae9e97d14f1b22ac3d6fa62b015c2e75d3f" + }, + { + "hits": 68, + "split": [ + 3, + 3 + ], + "words_sha256": "3e366365c962fd59a48ed6c651dc11100d0b7fab6b8c3ba37a136cfccfe30d39" + }, + { + "hits": 12, + "split": [ + 3, + 4 + ], + "words_sha256": "df1236006adc990138d8fc99b816ad2c09388df7ca93d87a2dc60bed893bfc9f" + }, + { + "hits": 2, + "split": [ + 4, + 2 + ], + "words_sha256": "6d3c2f6b773d14686fd4c4e94cc919acf87b6e2d4d8cc7b9f7837ca0bea50465" + }, + { + "hits": 12, + "split": [ + 4, + 3 + ], + "words_sha256": "74676dd9eea0be75bf658a3197ca59824beb49dc26c40682cfe7d427aa9628d4" + }, + { + "hits": 2, + "split": [ + 4, + 4 + ], + "words_sha256": "0c1a7f3e42b10b44cf87efa63321db0b71525d89cb4ef4a54e23297e626bb438" + } + ], + "length": 8, + "n": 3, + "restored": 210, + "simple_universal_wrong_bit0_rejections": 0, + "universal": 182 + }, + { + "comparisons": 32, + "hits_by_split": [ + { + "hits": 2, + "split": [ + 3, + 4 + ], + "words_sha256": "ed6ef50fa9ffa2fcced6823ed74395b8da9cc1400bfe956239771b119befc95e" + }, + { + "hits": 2, + "split": [ + 4, + 3 + ], + "words_sha256": "8a8d576e8b8eafeed6bdc3f9353cb3152bafe5da4f28325fbeef7f472015e5a9" + }, + { + "hits": 22, + "split": [ + 4, + 4 + ], + "words_sha256": "4465704c18a530c4656f36c5db8a2329726a8b4c4518d8b2b2e0040aa45adef3" + } + ], + "length": 8, + "n": 4, + "restored": 105, + "simple_universal_wrong_bit0_rejections": 6, + "universal": 26 + }, + { + "comparisons": 50, + "hits_by_split": [ + { + "hits": 60, + "split": [ + 3, + 4 + ], + "words_sha256": "067bf7166673dafec13ceeb4bd41c53dba62f8a220fa4eb38cbed3c8e350c64c" + }, + { + "hits": 30, + "split": [ + 3, + 5 + ], + "words_sha256": "08f342edfa2fc64ad6feedcae512b48a89acc8c55c5542dce3612a2289a4275f" + }, + { + "hits": 60, + "split": [ + 4, + 3 + ], + "words_sha256": "6f1b459cefcf6850423189f050b5dc8ff5f2938f82fbc13f4ffde7b2960453c2" + }, + { + "hits": 480, + "split": [ + 4, + 4 + ], + "words_sha256": "711b50f03bef1705d9dc40700bdac57a6d3261e0e87dcf8de0c534d9b5a9057f" + }, + { + "hits": 270, + "split": [ + 4, + 5 + ], + "words_sha256": "fbbebc31845a9734806546797d1ee80b1d96ec5f572bc1bc86f761d6eae3c415" + }, + { + "hits": 30, + "split": [ + 5, + 3 + ], + "words_sha256": "66dd9b48556c35dee282c3cd8e8808e39c632e5efff62b9bce47447c0ab040e8" + }, + { + "hits": 270, + "split": [ + 5, + 4 + ], + "words_sha256": "9f8194de5adb998ec60b66bb7c1d58b9bfe6f429f099f8f224880dd93b59c971" + }, + { + "hits": 110, + "split": [ + 5, + 5 + ], + "words_sha256": "ffbc678888a7d570a224b0d1706fbdf114fceaaf46685f21520f6b5c02fa7fd3" + } + ], + "length": 10, + "n": 4, + "restored": 3150, + "simple_universal_wrong_bit0_rejections": 20, + "universal": 1310 + }, + { + "comparisons": 50, + "hits_by_split": [], + "length": 10, + "n": 5, + "restored": 945, + "simple_universal_wrong_bit0_rejections": 0, + "universal": 0 + }, + { + "comparisons": 72, + "hits_by_split": [ + { + "hits": 144, + "split": [ + 5, + 6 + ], + "words_sha256": "730d148b8cb75bfbf966465560e2b97d052f3e1c30633faab88bc801c9cb0984" + }, + { + "hits": 144, + "split": [ + 6, + 5 + ], + "words_sha256": "f1c667f408f1df4f7278f474ad4a12a2fbc20abb77281dbd732d531ba5b7f7f3" + }, + { + "hits": 828, + "split": [ + 6, + 6 + ], + "words_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + } + ], + "length": 12, + "n": 5, + "restored": 51975, + "simple_universal_wrong_bit0_rejections": 248, + "universal": 1116 + } + ] +} diff --git a/research/f7-union-support-audit/README.md b/research/f7-union-support-audit/README.md new file mode 100644 index 0000000000..2c913f603f --- /dev/null +++ b/research/f7-union-support-audit/README.md @@ -0,0 +1,256 @@ +# Independent union-support census of the seven-label exclusion + +A separately implemented complete census corroborates Nicholas Stone's +[#2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973) exclusion +of restored universal seven-label words of length 20. All five admissible +weight-split representatives have zero hits. The length-18 control also has +zero hits. Together with the directly checked existing length-24 witness, +this corroborates `22 <= f(7) <= 24` in Ross Richardson's PR943 singleton +prefix-walk model. It is not a new bound, a supplier admission or a change to +selected kappa. + +The new [C++20 engine](census.cpp) uses an iterative stack of complete prefix +states and a bound on the **union** of same-parity pair supports. It neither +imports nor adapts the old or corrected census engines. The +[Python oracle](oracle.py) instead partitions word positions into positive +even blocks and checks literal pairwise-XOR coverage. This supplies the +independent full-domain implementation missing from #2973's open questions. +[#2984](https://github.com/CrocSwap/integer-mult-bounds/pull/2984) independently +accelerates the predecessor's representation but explicitly retains its DFS +and pruning logic. This package addresses a different verification gap. + +## Evidence + +[FULL.json](FULL.json) contains fresh uncapped runs from the empty prefix, +not shard receipts or a validation of historical counters. `entered` counts +accepted prefix states including the root. `attempts` counts label extensions +before rejection, so neither count should be compared to another engine's +node count without reconciling its definition. + +| Length | Weight split | Entered prefixes | Attempted extensions | Hits | +| ---: | ---: | ---: | ---: | ---: | +| 20 | 10,10 | 322,881,109 | 2,260,000,903 | 0 | +| 20 | 10,9 | 112,232,469 | 785,502,139 | 0 | +| 20 | 10,8 | 6,082,255 | 42,550,772 | 0 | +| 20 | 9,9 | 14,322,217 | 100,157,693 | 0 | +| 20 | 10,7 | 25,087 | 174,540 | 0 | +| 18 | 9,9 | 239,661 | 1,675,590 | 0 | + +Every run returns exit 0, `complete=true`, `cap=0` and an empty witness file. +All branches are rejected before a candidate restored leaf survives. These +are not counts of all restored words. GCC 14.2 and Clang 19.1 independently +compiled the same new source and produced identical complete JSON receipts. +The registered GCC replay of both obligations took 115.0 seconds; Clang's +full command took 86.9 seconds on the recorded Linux WSL2 host. This is not a controlled speed comparison with #2973 or #2984. +[ENVIRONMENT.json](ENVIRONMENT.json) records commands and versions. + +[QUICK.json](QUICK.json) records 270 exact engine/oracle comparisons over +all splits at `(n,L)=(2,4),(2,6),(3,6),(3,8),(4,8),(4,10),(5,10),(5,12)`. Each split is +run with the support bounds enabled and disabled. Every witness set must +match, including zero-hit splits. With support pruning disabled, every +restored-leaf count must also match. Canonical universal counts are +`3,15,10,182,26,1310,0,1116`. These positive cases test revisits as well as simple +walks. The oracle enumerates 51,975 restored canonical words at `(5,12)`. + +Twelve controls check caps, malformed parameters and failed witness output. +Four compiled mutants test a bit-0 partition, rejection of revisits, an +unsound strengthened support bound and omission of the last label. All are detected. +The full `(4,10)` comparison also passes an undefined-behavior/bounds sanitizer +build. Critical checks remain enabled under Python `-O`. + +## The old error, reproduced at its source + +The prefix states of `01021323` are +`[0,1,3,2,6,4,12,8]`, followed by the restored zero. Their pairwise XORs +cover all 16 masks. Weight parity gives sizes `4,4`; bit 0 gives `6,2`. +The bit-0 within-group collision excess is 8, exceeding the substituted +balanced budget `2*C(4,2)-7 = 5`. Its valid actual-size budget is +`C(6,2)+C(2,2)-7 = 9`. + +The pinned [PR2542 engine](../universal-f7-singleton-seedb859517b/engine.py), +`cyclic_census`, groups new points using `nq & 1`. Quick replay calls that +actual function on this one forced simple word. Without a collision budget +it returns one leaf and one universal word. With budget 5 it returns neither. +The new engine and oracle do not call that function. This historical audit +subject is the only predecessor code executed here. + +The affected word-census exclusions are PR2542's `n=7,L=18,budget=9` +invocation, PR2634's vendored word traversal and PR2691's C completion of +that traversal. Their old counters reproduce a filter, not its necessity. +The new six-case census provides separate corrected exclusion evidence; +it does not make the old prune sound. The set-level lemmas and explicit +witnesses in those packages require separate assessment. In particular, +this result does not revoke later set-level Fourier or Sidon arguments. +Frozen predecessor files stay unchanged. + +## Why the new enumeration is complete + +For a restored word of even length `L`, let `P` be its distinct nonclosing +prefix states. A prefix at index `d` has weight parity `d mod 2`. Let `E,O` +be the distinct even/odd states, with final sizes `s,t`. Both sizes are at +most `L/2`, since the closing zero repeats the initial zero. Revisited +points add no pairs and no capacity. + +At a partial prefix, let `e,o` be the current sizes and let + +``` +U = {x XOR y : x,y in E, x != y} union {x XOR y : x,y in O, x != y} +V = {x XOR y : x in E, y in O} +``` + +`U` is maintained as one union, not two separate support counts. A completion +can introduce at most + +``` +C(s,2) + C(t,2) - C(e,2) - C(o,2) +``` + +additional same-parity pairs, and at most `s*t-e*o` additional cross pairs. +Each additional pair contributes at most one new mask. Therefore a universal +completion necessarily satisfies + +``` +|U| + C(s,2) + C(t,2) - C(e,2) - C(o,2) >= 2^(n-1)-1 +|V| + s*t-e*o >= 2^(n-1) +``` + +These bounds include overlaps between the two same-parity supports, unlike +#2973's separate within-side excess bound. Both remain necessary with +revisits to already visited states. A new state adds its XORs with every +previous state on the appropriate side. Copying the complete node into the +next stack slot makes backtracking restore all sets and counters together. + +Other pruning is elementary: + +- Only labels `0..used` may follow, with `used r`. +- Reject a new point when its side is already full. After depth `d= ceil((s*t-64)/2) +sum_x A_x*B_x <= B0+a*b +``` + +The lower bound double-counts cross-pair collisions: +`sum_y C(r_y,2)=2*sum_x A_x*B_x`, with `r_y>=1` on all 64 odd masks. +For the upper bound, expand `A_x*B_x` on shared support and bound the residual +product by `a*b`. At `(9,8)`, `B0=1`, so `a*b=0`, whereas the lower bound +is 4. The remaining five splits are precisely the complete L20 runs. +[oracle.py](oracle.py) recomputes this finite split list independently. +At length 18 the same argument leaves only `(9,9)`. + +Rotating a closed word by one position translates `P` by an odd-weight state, +swapping `E,O` without changing `P+P`. Relabeling by first occurrence restores +canonical form. Thus the mirrored splits need no separate exclusion. +Appending repeated pairs of any already used label preserves restoration and +coverage, so a shorter restored universal word would yield one of length 20. +Odd lengths cannot restore. The zero-hit runs therefore corroborate `f(7)>=22`. +The literal existing upper word `010201030102010345464546` restores and covers +all 128 masks, giving `f(7)<=24` independently of the census. + +## Reproduce + +Python 3.12 standard library and a C++20 compiler are required. The default +`c++` must support the warnings in `verify.py` and UBSan/bounds sanitizers. +The registered hook does not install a compiler. From the repository root: + +```sh +python3.12 -I -O -Werror -B research/f7-union-support-audit/verify.py +python3.12 -I -O -Werror -B research/f7-union-support-audit/verify.py --full +python3.12 -B scripts/research_package.py --package research/f7-union-support-audit +``` + +Expected markers are `PASS_F7_INDEPENDENT_QUICK` and +`PASS_F7_INDEPENDENT_FULL`. Each command compiles fresh native code and uses +a private temporary directory. `--compiler clang++` chooses the second tested +compiler. `--emit` prints reconstructed JSON rather than comparing it with +the committed receipt. Full mode has a 540-second native budget; timeout, +nonzero exit, a cap, a changed counter or a nonempty witness file fails. +Quick and full commands are separate obligations; full mode alone does not +run the small-domain controls. No predecessor artifact is regenerated. + +For the native CLI, run `census n L s t mode cap hits-file`, with `mode=1` +for the proved support bounds and `mode=0` to disable them. `cap=0` requests +an uncapped traversal; a positive cap counts attempted label extensions and +returns exit 2 with `complete=false` when reached. Exit 1 is an input, I/O or +internal failure. Only exit 0 with `complete=true` can support an exclusion. +The witness path is overwritten, so use a fresh workspace. + +## Open next questions + +Does a length-22 seven-label universal word exist? It would decide the +remaining gap in this abstract model. First derive its admissible weight +splits and estimate a separately bounded search before extending this engine, +whose enforced maximum length is 20. No length-22 exclusion or automatic +family expansion follows from this audit. + +A formal proof of the full traversal and pruning remains open. The written +completeness argument, independent oracle and cross-compiler runs are executable +evidence, not a proof-assistant kernel check. A first formalization step is +the two union-support completion inequalities, including revisits. +Structured questions and blockers are in [TASK.json](TASK.json). + +## Scope, attribution and engineering limits + +Scientific base main is `836b19bfa309ceafbc8ee32a15e8c4b10dde7e11`, priority +revision 6. [SOURCES.json](SOURCES.json) pins the exact old/corrected source +subjects and proposed exclusion receipt. [TASK.json](TASK.json) records the +bounded scope expansion, freshness, live overlap and canonical claim. +No old engine contributes candidate pruning or a full-run result to the new +engine. The result does not prove a statement outside the PR943 model. + +Credit Ross Richardson for that model, Aaron Wang for PR2542/PR2634 and the +set-level/census lineage, Nicholas Stone for PR2691, the parity correction, +corrected exclusion and counterexample in PR2973, Tekalign for PR2984's +separately scoped representation acceleration, and Douglas Colkitt for the +retained research and source-binding framework. Nick Petalas contributes this +independent union-support implementation, slot-partition oracle and replay. +Apache-2.0. Substantial automated assistance was used in research, implementation, +checking and writing. No independent human or formal-kernel review is claimed. + +Build the Lever led to a retained second implementation rather than another +receipt-only replay. Prove It Works required exact complete witness-set +comparison and actual uncapped native runs. Test Behavior, Not Implementation +led to positive universal fixtures and compiled incorrect implementations. + +Power-of-Ten inspection found no new recursive code. The native core uses +21 fixed stack slots, two 64-bit words per mask, at most ten points per side, +and a hard `2<=n<=7, 2n<=L<=20` input boundary. Its loop bound is twice +`sum(n^d,d=0..L)`, which fits uint64 throughout that domain. Every new function +is under 60 lines. All acceptance checks are explicit under `-O`, native +compilation treats the listed warnings as errors, and sanitizer controls run +in quick mode. `ruff check research/f7-union-support-audit` applies the local +strict diagnostic list. The one E402 suppression permits the explicitly +bounded sibling import under isolated Python. Each native process has a timeout and temporary outputs are +removed on success or failure. + +Rules 3, 8 and 9 need bounded runtime deviations. Python and C++ stream/runtime +libraries allocate; Python's slot oracle has a two-million-state iteration +and worklist limit in its enforced small domain. The new native search itself +uses fixed-capacity value storage and no callbacks. The historical control +loads one authenticated old module, makes two depth-eight, 100-node-capped +calls and checks their actual results. That old recursive code is an audit +subject, not a dependency of the new search. Reassess resource and runtime +controls before widening the domain. Hosted CI, the full selected supplier +cold replay and all-size multiplication obligations are not claimed passed. diff --git a/research/f7-union-support-audit/SOURCES.json b/research/f7-union-support-audit/SOURCES.json new file mode 100644 index 0000000000..13ffc1eb20 --- /dev/null +++ b/research/f7-union-support-audit/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "4450dbbd1d01929022259f523234590f4cce65b9", + "sha256": "ca056a6def333df7afd822c1f34adc2eaa9089b241fc2bdd5803b64066fc9355" + }, + { + "path": "research/f7-weight-parity-census-correction/README.md", + "usage": "input", + "git_blob": "0221748ce35d4a2dc6ee5ce61be210eb34a2ea83", + "sha256": "9bc7867ccfa97a682e4683052647d4bf8f191da5a219271f87d3e0a10de1446a" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/SUMMARIES.json", + "usage": "input", + "git_blob": "b82513ed4f33cba22d1c9fca95cc1928ac9090b2", + "sha256": "e58bcef2ee6e03c889061c001623a6159dd3cfffd0a35acb6f3ab630002261c2" + }, + { + "path": "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "usage": "input", + "git_blob": "bfa7e405969e41fe385a43856479eb8e32f34f8f", + "sha256": "265ead915d1b490c1923bce9b894ecac60f6195fc3d2ceadd6b25077238f415a" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + } + ] +} diff --git a/research/f7-union-support-audit/TASK.json b/research/f7-union-support-audit/TASK.json new file mode 100644 index 0000000000..182ee79b71 --- /dev/null +++ b/research/f7-union-support-audit/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "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": "changed", + "actual_scope": "Independently reproduce PR2542's wrong bit-0 prune and validate a new union-support completion bound against an unpruned slot-partition oracle; after that gate, independently implement and complete the five n=7,L=20 split representatives and the L18 control.", + "scope_change_reason": "The card's small audit was expanded only after six small domains and failure/mutant controls passed. PR2973 explicitly requests an independent full implementation, while live PR2984 retains the original DFS/pruning. A separate ten-minute native budget was declared before running the full census. This corroborates the proposed exclusion rather than extending the mathematical search domain or changing the selected frontier.", + "bottleneck_link": "Unsound word pruning can wrongly close a mechanism. This supplies independent full-domain evidence for the corrected exclusion instead of relying on shared old traversal counters; it does not improve the abstract bound, supplier or kappa.", + "budget_minutes": 60, + "stop_rule": "Do not run a seven-label census until the independent small-domain gate passes. Stop or narrow after a ten-minute native budget, any mismatch, cap or timeout. No length-22 search, supplier adoption or dependent construction expansion.", + "outcome": "completed", + "evidence": "QUICK.json: 270 exact engine/oracle comparisons, 12 error/cap controls, four rejected compiled mutants and a sanitizer comparison. FULL.json: six fresh uncapped zero-hit cases, reproduced identically with GCC14 and Clang19. README.md supplies the complete pruning, split, symmetry and padding arguments.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance in research, implementation, checking and writing. No independent human or formal-kernel review is claimed.", + "assignment": { + "initial_picker_nonce": "b3a8d49a40325d20e40d36b48f01aac4", + "initial_track": "bit-mechanisms", + "override_reason": "Prefer the revision-6 central census-audit handoff with an explicit missing independent implementation. Live PR2992 already covers the scatter guard, PR2993 covers a joint-frame audit, and the bit helper interfaces have extensive existing coverage.", + "scope_key": "f7-union-support-independent-iterative-n7-l20", + "milestone": "audit", + "full_native_budget_seconds": 600, + "consumer_and_supplier_costs": "Not applicable to this audit. No new construction or cost saving is claimed.", + "family_expansion_decision": "Stop after independent corroboration. No length-22 or dependent construction round is authorized by this result." + }, + "predecessors": [ + {"pr": 2542, "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", "credit": "Aaron Wang", "use": "Pinned historical wrong-prune audit subject"}, + {"pr": 2973, "head": "d48f3945dbb1ef5d06835744c4082b3bd04181c0", "credit": "Nicholas Stone", "use": "Counterexample, corrected proposed exclusion and open independent-implementation handoff"}, + {"pr": 2984, "head": "34d7c3feaf87b878d9524c215b678403b8afdc08", "credit": "Tekalign", "use": "Live overlapping representation acceleration; shares the predecessor DFS/pruning, not duplicated here"} + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18978045", + "overlap": { + "checked_at_utc": "2026-10-16T16:40:46Z", + "open_prs_complete": true, + "open_prs_records": 238, + "discussions_complete": true, + "discussions_records": 1704, + "closed_pr_bodies_complete": true, + "closed_pr_records": 2440, + "limits": "Titles/bodies/comments and local package notes, not every diff or nested file. No matches does not establish novelty." + }, + "submission_checkpoint": { + "main_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "checked_at_utc": "2026-10-16T16:59:05Z", + "priority_revision": 6, + "guidance_and_inputs_unchanged": true, + "coverage": "Complete pagination: 246 open PRs at 16:58:11Z, 1708 discussions at 16:58:39Z, 2440 closed/merged PR bodies at 16:59:04Z. PR2984 head remains 34d7c3feaf87b878d9524c215b678403b8afdc08. No competing independent full implementation was found; coverage excludes arbitrary code diffs.", + "decision": "Submit the bounded audit against the unchanged fetched main and retain exact historical source pins." + }, + "open_questions": [ + { + "question": "Does a restored universal seven-label word of length 22 exist?", + "why_it_matters": "It decides the remaining abstract gap f(7) in {22,24}, not a multiplication supplier or exponent by itself.", + "first_step": "Derive its complete weight-split domain and price a separately bounded experiment before extending the current hard L<=20 limit.", + "blocked_by": "No length-22 search or complete resource budget is supplied here." + }, + { + "question": "Can the union-support completion inequalities and complete traversal be checked by a proof-assistant kernel?", + "why_it_matters": "Executable cross-checks and written proofs still leave trust in the new native traversal and runtime.", + "first_step": "Formalize the two support-capacity inequalities for distinct prefix sets, including repeated visits.", + "blocked_by": "No formalization environment or kernel proof is included; this is not required to reproduce the finite receipts." + } + ] +} diff --git a/research/f7-union-support-audit/VERIFY.json b/research/f7-union-support-audit/VERIFY.json new file mode 100644 index 0000000000..a8d4bec16d --- /dev/null +++ b/research/f7-union-support-audit/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-weight-parity-census-correction/README.md", + "research/f7-weight-parity-census-correction/engine/SUMMARIES.json", + "research/f7-weight-parity-census-correction/engine/corrected_census.c", + "research/universal-f7-singleton-seedb859517b/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fresh C++20 build; tiny historical false prune; 270 exact word-set/oracle comparisons over eight complete small domains; 12 cap/error controls; four compiled mutants; UBSan/bounds complete comparison. Requires an installed C++20 compiler." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/verify.py", "--full"], + "timeout_seconds": 600, + "checks": "Fresh C++20 build and six uncapped n=7 traversals from the empty prefix, exact comparison of all non-timing fields with FULL.json, empty witness files and successful completion." + } + ] +} diff --git a/research/f7-union-support-audit/census.cpp b/research/f7-union-support-audit/census.cpp new file mode 100644 index 0000000000..5b290af8c8 --- /dev/null +++ b/research/f7-union-support-audit/census.cpp @@ -0,0 +1,201 @@ +// Independent singleton-prefix census. Nick Petalas. Apache-2.0. +#include +#include +#include +#include +#include +#include +#include +#include + +namespace { +constexpr int max_length = 20; +constexpr int max_side = max_length / 2; + +struct Bits { + std::array words{}; + bool contains(int x) const { + return (words[static_cast(x) / 64U] >> (x % 64)) & 1U; + } + void insert(int x) { words[static_cast(x) / 64U] |= std::uint64_t{1} << (x % 64); } + int size() const { return std::popcount(words[0]) + std::popcount(words[1]); } +}; + +struct Node { + Bits visited, same, cross; + std::array, 2> points{}; + std::array sizes{1, 0}; + int position = 0; + int used = 0; +}; + +struct Config { + int n, length; + std::array goal; + bool prune; + std::uint64_t cap; +}; + +struct Totals { + std::uint64_t attempts = 0, entered = 1, leaves = 0, hits = 0; + std::uint64_t restoration = 0, size = 0, same = 0, cross = 0; + bool complete = false; +}; + +std::uint64_t number(std::string_view text) { + std::uint64_t value = 0; + auto result = std::from_chars(text.data(), text.data() + text.size(), value); + if (result.ec != std::errc{} || result.ptr != text.data() + text.size()) { + throw std::invalid_argument("expected an unsigned decimal integer"); + } + return value; +} + +Config parse(char** argv) { + std::array v{}; + for (unsigned i = 0; i < v.size(); ++i) v[i] = number(argv[i + 1]); + if (v[0] < 2 || v[0] > 7 || v[1] < 2 * v[0] || v[1] > max_length || v[1] % 2 != 0 || + v[2] < 1 || v[3] < 1 || v[2] > v[1] / 2 || v[3] > v[1] / 2 || v[4] > 1) { + throw std::invalid_argument("require 2<=n<=7, even 2n<=L<=20, 1<=s,t<=L/2, mode=0 or 1"); + } + return {static_cast(v[0]), static_cast(v[1]), + {static_cast(v[2]), static_cast(v[3])}, v[4] == 1, v[5]}; +} + +int pairs(int size) { return size * (size - 1) / 2; } + +bool extend(Node& next, int label, int depth, const Config& c) { + next.position ^= 1 << label; + if (label == next.used) ++next.used; + const int remaining = c.length - depth; + if (std::popcount(static_cast(next.position)) + 2 * (c.n - next.used) > remaining) { + return false; + } + if (next.visited.contains(next.position)) return true; + const unsigned side = static_cast(depth % 2); + if (next.sizes[side] >= c.goal[side]) throw std::logic_error("point capacity exceeded"); + for (int j = 0; j < next.sizes[side]; ++j) { + next.same.insert(next.position ^ next.points[side][static_cast(j)]); + } + for (int j = 0; j < next.sizes[1U - side]; ++j) { + next.cross.insert(next.position ^ next.points[1U - side][static_cast(j)]); + } + next.points[side][static_cast(next.sizes[side]++)] = next.position; + next.visited.insert(next.position); + return true; +} + +bool viable(const Node& node, int depth, const Config& c, Totals& totals) { + // Only nonclosing positions can add distinct points in a restored word. + if (depth < c.length && + (node.sizes[0] + c.length / 2 - 1 - depth / 2 < c.goal[0] || + node.sizes[1] + c.length / 2 - (depth + 1) / 2 < c.goal[1])) { + ++totals.size; + return false; + } + if (!c.prune) return true; + const int half = 1 << (c.n - 1); + const int future_same = pairs(c.goal[0]) + pairs(c.goal[1]) - pairs(node.sizes[0]) - pairs(node.sizes[1]); + if (node.same.size() + future_same < half - 1) { + ++totals.same; + return false; + } + const int future_cross = c.goal[0] * c.goal[1] - node.sizes[0] * node.sizes[1]; + if (node.cross.size() + future_cross < half) { + ++totals.cross; + return false; + } + return true; +} + +void leaf(const Node& node, const Config& c, const std::array& word, + Totals& totals, std::ofstream& hits) { + if (node.position != 0 || node.used != c.n || node.sizes != c.goal) return; + if (node.visited.size() != node.sizes[0] + node.sizes[1]) throw std::logic_error("distinct-point invariant"); + if (node.same.contains(0) || node.cross.contains(0)) throw std::logic_error("nonzero-pair invariant"); + ++totals.leaves; + if (node.same.size() + node.cross.size() != (1 << c.n) - 1) return; + ++totals.hits; + for (int i = 0; i < c.length; ++i) hits << word[static_cast(i)]; + hits << '\n'; +} + +std::uint64_t iteration_bound(const Config& c) { + // At most n^d nodes at depth d. One descent and one return per edge. + std::uint64_t level = 1, nodes = 1; + for (int d = 1; d <= c.length; ++d) { + level *= static_cast(c.n); + nodes += level; + } + return 2 * nodes; +} + +Totals enumerate(const Config& c, std::ofstream& hits) { + std::array stack{}; + std::array next_label{}; + std::array word{}; + stack[0].visited.insert(0); + Totals totals; + int depth = 0; + const auto bound = iteration_bound(c); + for (std::uint64_t iteration = 0; iteration < bound; ++iteration) { + const auto index = static_cast(depth); + if (depth == c.length || next_label[index] >= c.n || next_label[index] > stack[index].used) { + if (depth == c.length) leaf(stack[index], c, word, totals, hits); + if (depth == 0) { totals.complete = true; return totals; } + --depth; + continue; + } + if (c.cap != 0 && totals.attempts == c.cap) return totals; + ++totals.attempts; + const int label = next_label[index]++; + Node candidate = stack[index]; + const int position = candidate.position ^ (1 << label); + const auto side = static_cast((depth + 1) % 2); + if (!candidate.visited.contains(position) && candidate.sizes[side] == c.goal[side]) { + ++totals.size; + continue; + } + if (!extend(candidate, label, depth + 1, c)) { ++totals.restoration; continue; } + if (!viable(candidate, depth + 1, c, totals)) continue; + word[index] = label; + ++depth; + stack[index + 1] = candidate; + next_label[index + 1] = 0; + ++totals.entered; + } + throw std::logic_error("finite tree bound exhausted"); +} + +void report(const Config& c, const Totals& t) { + if (t.attempts + 1 != t.entered + t.restoration + t.size + t.same + t.cross) { + throw std::logic_error("extension accounting invariant"); + } + std::cout << "{\"n\":" << c.n << ",\"length\":" << c.length + << ",\"split\":[" << c.goal[0] << ',' << c.goal[1] << "]" + << ",\"prune\":" << (c.prune ? "true" : "false") + << ",\"cap\":" << c.cap << ",\"complete\":" << (t.complete ? "true" : "false") + << ",\"attempts\":" << t.attempts << ",\"entered\":" << t.entered + << ",\"candidate_leaves\":" << t.leaves << ",\"hits\":" << t.hits + << ",\"restoration_prunes\":" << t.restoration << ",\"size_prunes\":" << t.size + << ",\"same_prunes\":" << t.same << ",\"cross_prunes\":" << t.cross << "}\n"; +} +} // namespace + +int main(int argc, char** argv) { + try { + if (argc != 8) throw std::invalid_argument("usage: census n L s t mode cap hits-file"); + const Config c = parse(argv); + std::ofstream hits(argv[7]); + hits.exceptions(std::ios::failbit | std::ios::badbit); + const Totals totals = enumerate(c, hits); + hits.close(); + report(c, totals); + std::cout.flush(); + if (!std::cout) throw std::runtime_error("failed to write summary"); + return totals.complete ? 0 : 2; + } catch (const std::exception& error) { + std::cerr << error.what() << '\n'; + return 1; + } +} diff --git a/research/f7-union-support-audit/oracle.py b/research/f7-union-support-audit/oracle.py new file mode 100644 index 0000000000..44988a40d5 --- /dev/null +++ b/research/f7-union-support-audit/oracle.py @@ -0,0 +1,90 @@ +"""Unpruned slot-partition oracle, independent of prefix-search pruning. + +Nick Petalas. Apache-2.0. +""" +from collections import Counter +from itertools import combinations + +MAX_ORACLE_STATES = 2_000_000 + + +def restored_words(n, length): + """Partition slots into n positive even blocks, ordered by their minima.""" + if not (2 <= n <= 5 and 2 * n <= length <= 12 and length % 2 == 0): + raise ValueError("oracle domain is 2<=n<=5, even 2n<=L<=12") + work = [((-1,) * length, tuple(range(length)), 0)] + for _ in range(MAX_ORACLE_STATES): + if not work: + return + word, free, label = work.pop() + if label == n: + if not free: + yield word + continue + # The smallest free slot must start the next block in canonical order. + maximum = len(free) - 2 * (n - label - 1) + for size in range(2, maximum + 1, 2): + for rest in combinations(free[1:], size - 1): + slots = (free[0], *rest) + new_word = tuple(label if i in slots else x for i, x in enumerate(word)) + new_free = tuple(i for i in free if i not in slots) + work.append((new_word, new_free, label + 1)) + if len(work) > MAX_ORACLE_STATES: + raise RuntimeError("oracle work capacity exceeded") + raise RuntimeError("oracle iteration limit exceeded") + + +def describe(word, n): + if not (2 <= n <= 7 and 2 * n <= len(word) <= 24): + raise ValueError("invalid word size") + if any(type(j) is not int or not 0 <= j < n for j in word): + raise ValueError("invalid label") + counts = Counter(word) + if set(counts) != set(range(n)) or any(c % 2 for c in counts.values()): + raise ValueError("word must use every label a positive even number of times") + path, position = [], 0 + for label in word: + path.append(position) + position ^= 1 << label + if position != 0: + raise RuntimeError("restoration invariant failed") + points = set(path) + groups = [{x for x in points if x.bit_count() % 2 == side} for side in range(2)] + bit0 = [{x for x in points if x % 2 == side} for side in range(2)] + wrong_excess = sum(len(g) * (len(g) - 1) // 2 - len({a ^ b for a, b in combinations(g, 2)}) + for g in bit0) + split = tuple(map(len, groups)) + budget = sum(s * (s - 1) // 2 for s in split) - ((1 << (n - 1)) - 1) + return {"path": path, "split": split, "bit0_split": tuple(map(len, bit0)), + "coverage": len({a ^ b for a in points for b in points}), + "wrong_excess": wrong_excess, "weight_budget": budget, + "simple": len(points) == len(word)} + + +def census(n, length): + all_words, hits = {}, {} + wrong_simple = 0 + for word in restored_words(n, length): + info = describe(word, n) + split = info["split"] + all_words[split] = all_words.get(split, 0) + 1 + if info["coverage"] == 1 << n: + encoded = "".join(map(str, word)) + hits.setdefault(split, set()).add(encoded) + wrong_simple += info["simple"] and info["wrong_excess"] > info["weight_budget"] + return all_words, hits, wrong_simple + + +def admissible_splits(length): + """Basic pair counting followed by the collision-product identity, n=7.""" + possible = [] + for s in range(1, length // 2 + 1): + for t in range(1, s + 1): + budget = s * (s - 1) // 2 + t * (t - 1) // 2 - 63 + if budget < 0 or s * t < 64: + continue + need = (s * t - 64 + 1) // 2 + if any(budget + a * b >= need for a in range(budget + 1) + for b in range(budget + 1 - a)): + possible.append((s, t)) + return possible diff --git a/research/f7-union-support-audit/ruff.toml b/research/f7-union-support-audit/ruff.toml new file mode 100644 index 0000000000..bd1ae30816 --- /dev/null +++ b/research/f7-union-support-audit/ruff.toml @@ -0,0 +1,4 @@ +target-version = "py312" + +[lint] +select = ["E4", "E7", "E9", "F", "I", "UP", "B", "PLW", "RUF"] diff --git a/research/f7-union-support-audit/verify.py b/research/f7-union-support-audit/verify.py new file mode 100644 index 0000000000..11cbdcb993 --- /dev/null +++ b/research/f7-union-support-audit/verify.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Fresh independent census checks. Nick Petalas. Apache-2.0.""" +import argparse +import hashlib +import json +import runpy +import subprocess +import sys +import tempfile +import time +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +# -I excludes the script directory. Only this package's explicit sibling is imported. +sys.path.insert(0, str(PACKAGE)) +from oracle import admissible_splits, census, describe # noqa: E402 + +FLAGS = ["-std=c++20", "-O3", "-Wall", "-Wextra", "-Wpedantic", "-Wconversion", + "-Wsign-conversion", "-Wshadow", "-Werror"] +CASES = [(2, 4), (2, 6), (3, 6), (3, 8), (4, 8), (4, 10), (5, 10), (5, 12)] +FULL_CASES = [(7, 20, 10, 10), (7, 20, 10, 9), (7, 20, 10, 8), + (7, 20, 9, 9), (7, 20, 10, 7), (7, 18, 9, 9)] + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def pins(): + source = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in source["files"]: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "changed input: " + row["path"]) + + +def compile_engine(directory, compiler, source=None, sanitize=False): + target = directory / "census" + path = PACKAGE / "census.cpp" + if source is not None: + path = directory / "mutant.cpp" + path.write_text(source) + flags = FLAGS + (["-O1", "-fsanitize=undefined,bounds", "-fno-sanitize-recover=all"] if sanitize else []) + subprocess.run([compiler, *flags, str(path), "-o", str(target)], check=True, + capture_output=True, text=True, timeout=60) + return target + + +def run_engine(binary, args, directory, timeout=60): + hits = directory / "hits.txt" + proc = subprocess.run([str(binary), *map(str, args), str(hits)], check=False, capture_output=True, + text=True, timeout=timeout) + require(proc.returncode in (0, 2), "engine error: " + proc.stderr) + result = json.loads(proc.stdout) + require(result["complete"] == (proc.returncode == 0), "exit/completeness mismatch") + require(hits.stat().st_size <= 5_000_000, "oversize witness output") + words = hits.read_text().splitlines() + require(len(words) == len(set(words)) == result["hits"], "duplicate or missing witnesses") + return result, set(words) + + +def compare_case(binary, directory, n, length): + counts, expected, wrong_simple = census(n, length) + rows = [] + limit = min(length // 2, 1 << (n - 1)) + for s in range(1, limit + 1): + for t in range(1, limit + 1): + wanted = expected.get((s, t), set()) + for mode in (0, 1): + result, words = run_engine(binary, (n, length, s, t, mode, 0), directory) + require(result["complete"] and words == wanted, f"oracle mismatch {n,length,s,t,mode}") + if mode == 0: + require(result["candidate_leaves"] == counts.get((s, t), 0), "unpruned restored count") + if wanted: + digest = hashlib.sha256(("\n".join(sorted(wanted)) + "\n").encode()).hexdigest() + rows.append({"split": [s, t], "hits": len(wanted), "words_sha256": digest}) + return {"n": n, "length": length, "restored": sum(counts.values()), + "universal": sum(map(len, expected.values())), "hits_by_split": rows, + "simple_universal_wrong_bit0_rejections": wrong_simple, + "comparisons": 2 * limit * limit} + + +def fixtures(): + tiny = describe((0, 1, 0, 2, 1, 3, 2, 3), 4) + require(tiny == {"path": [0, 1, 3, 2, 6, 4, 12, 8], "split": (4, 4), + "bit0_split": (6, 2), "coverage": 16, "wrong_excess": 8, + "weight_budget": 5, "simple": True}, "tiny counterexample") + splits = admissible_splits(20) + require(splits == [(9, 9), (10, 7), (10, 8), (10, 9), (10, 10)], "L20 split domain") + require(admissible_splits(18) == [(9, 9)], "L18 split domain") + upper = tuple(map(int, "010201030102010345464546")) + require(describe(upper, 7)["coverage"] == 128, "L24 upper witness") + return {"counterexample": tiny, "l20_splits": splits, "l24_upper_word": "".join(map(str, upper))} + + +def historical_control(): + # Authenticated audit subject only. The new engine and oracle never call it. + path = ROOT / "research/universal-f7-singleton-seedb859517b/engine.py" + subject = runpy.run_path(str(path))["cyclic_census"] + word = (0, 1, 0, 2, 1, 3, 2, 3) + unpruned = subject(4, 8, simple=True, prefix=word, max_nodes=100) + faulty = subject(4, 8, budget=5, simple=True, prefix=word, max_nodes=100) + require(unpruned["hits"] == 1 and unpruned["leaves"] == 1, "historical positive control") + require(faulty["hits"] == 0 and faulty["leaves"] == 0, "historical wrong prune not reproduced") + return {"without_budget": unpruned, "bit0_budget_5": faulty} + + +def failure_controls(binary, directory): + for cap in (1, 7, 100): + result, _ = run_engine(binary, (4, 8, 4, 4, 1, cap), directory) + require(not result["complete"] and result["attempts"] == cap, "cap falsely accepted") + bad = [(1, 8, 4, 4, 1, 0), (8, 20, 10, 10, 1, 0), (3, 7, 3, 3, 1, 0), + (3, 22, 3, 3, 1, 0), (3, 8, 5, 3, 1, 0), (3, 8, 3, 3, 2, 0), + (3, 8, 3, 3, 1, -1), (3, 8, 3, 3, 1, "1x")] + for args in bad: + proc = subprocess.run([str(binary), *map(str, args), str(directory / "bad-hits")], + check=False, capture_output=True, text=True, timeout=5) + require(proc.returncode == 1 and not proc.stdout, "invalid input accepted") + proc = subprocess.run([str(binary), "3", "8", "3", "3", "1", "0", str(directory)], + check=False, capture_output=True, text=True, timeout=5) + require(proc.returncode == 1 and not proc.stdout, "unwritable output accepted") + return 12 + + +def mutant_controls(directory, compiler): + original = (PACKAGE / "census.cpp").read_text() + mutations = [ + ("depth % 2", "next.position & 1"), + ("if (next.visited.contains(next.position)) return true;", "if (next.visited.contains(next.position)) return remaining == 0;"), + ("node.same.size() + future_same < half - 1", "node.same.size() + future_same < half"), + ("next_label[index] >= c.n", "next_label[index] >= c.n - 1"), + ] + _, expected, _ = census(3, 8) + for index, (old, new) in enumerate(mutations): + require(original.count(old) == 1, "ambiguous mutation") + sub = directory / str(index) + sub.mkdir() + binary = compile_engine(sub, compiler, original.replace(old, new)) + detected = False + for split, wanted in expected.items(): + try: + result, words = run_engine(binary, (3, 8, *split, 1, 0), sub) + detected |= not result["complete"] or words != wanted + except RuntimeError as error: + require(str(error).startswith("engine error:"), "unexpected mutant harness failure") + detected = True + require(detected, "surviving implementation mutant " + str(index)) + return len(mutations) + + +def quick(directory, compiler): + binary = compile_engine(directory, compiler) + checks = fixtures() + historical = historical_control() + rows = [compare_case(binary, directory, *case) for case in CASES] + by_case = {(row["n"], row["length"]): row for row in rows} + require(by_case[(2, 4)]["universal"] == 3 and by_case[(3, 6)]["universal"] == 10 + and by_case[(4, 8)]["universal"] == 26, "known positive controls") + failures = failure_controls(binary, directory) + mutants = mutant_controls(directory, compiler) + sanitized = directory / "sanitized" + sanitized.mkdir() + binary = compile_engine(sanitized, compiler, sanitize=True) + control = compare_case(binary, sanitized, 4, 10) + require(control == by_case[(4, 10)], "sanitizer result mismatch") + return {"fixtures": checks, "historical_control": historical, + "small_domains": rows, "failure_controls": failures, + "rejected_mutants": mutants, "sanitized_case": [4, 10]} + + +def full(directory, compiler): + binary = compile_engine(directory, compiler) + results = [] + deadline = time.monotonic() + 540 + for case in FULL_CASES: + remaining = deadline - time.monotonic() + require(remaining > 0, "full census budget exhausted") + result, words = run_engine(binary, (*case, 1, 0), directory, timeout=remaining) + require(result["complete"] and result["cap"] == 0 and result["hits"] == 0 and not words, + "full exclusion failed") + results.append(result) + return {"cases": results} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--full", action="store_true", help="six uncapped seven-label traversals, at most 540 native seconds") + parser.add_argument("--emit", action="store_true", help="print fresh receipt instead of comparing committed receipt") + parser.add_argument("--compiler", default="c++") + args = parser.parse_args() + pins() + with tempfile.TemporaryDirectory(prefix="f7-independent-") as temporary: + work = Path(temporary) + report = full(work, args.compiler) if args.full else quick(work, args.compiler) + filename = "FULL.json" if args.full else "QUICK.json" + # Normalize tuples to the JSON representation before the exact comparison. + report = json.loads(json.dumps(report)) + if args.emit: + print(json.dumps(report, indent=2, sort_keys=True)) + else: + require(report == json.loads((PACKAGE / filename).read_text()), "committed receipt mismatch") + print("PASS_F7_INDEPENDENT_FULL" if args.full else "PASS_F7_INDEPENDENT_QUICK") + + +if __name__ == "__main__": + main()