diff --git a/research/p112-intersection-counter-capacity/README.md b/research/p112-intersection-counter-capacity/README.md new file mode 100644 index 0000000000..d50905a50f --- /dev/null +++ b/research/p112-intersection-counter-capacity/README.md @@ -0,0 +1,192 @@ +# The intersection-counter engine refuses the P112 36-generator basis + +**Capacity refusal on one basis. No new κ.** The selected conditional exponent +stays `781451/250000000`. On the 36-generator kernel basis of the P112 +punctured frame code, `research/e7-intersection-counters/engine.py` returns +no set. At every legal batch size, including the named batch size 20, +`low_weight_words` raises `ValueError: dimension exceeds 27` before yielding +a word. The eight-word target stays the set recorded by open PR #7007. The +SHA256 of its seven positive words is +`ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. + +## Result + +The lines are the coordinate complement in +`research/p112-rank6-frame-coverage/engine.py`. An independent E8 builder +reproduces that ordered 120-line list and the same eight punctured positions. +The 112 live lines carry 1260 orthogonal 8-frames, and every live line lies +in 90 of them. The incidence matrix has rank 76. The kernel basis with an +identity on the free coordinates + +```text +(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16, 18, 20, + 24, 25, 26, 28, 30, 32, 34, 36, 40, 42, 48, 49, 50, 51, 52, 56, 58, 64, 80) +``` + +matches the free coordinates and weights recorded by PR #7007. The kernel +vector with a single 1 on a given free coordinate is unique, so this ordered +basis is that one. The SHA256 of `json.dumps` of the 36 generator integers is +`c93a6ec3f6d61b3bbf4086218c723761e517bc42ac2c26f551436d271a081e9d`. +Each generator is a positive integer below `2^112`. + +The seven target words are the coordinate partition from that PR, recomputed +here. They are pairwise disjoint, they cover every live line, each has weight +16, and each meets every live 8-frame evenly. In the pinned live order they +are + +```text +64691900160 +1034819666160 +280375465144335 +4772259772306660006937399132160 +15509841550538713979819718082560 +1216944648758260568639796318044160 +3955070108453721685622467917250560 +``` + +`json.dumps` of that sorted list has the hash above. Deleting the first +integer changes the hash. PR #7007's half-split census says these seven +words, together with zero, are the weight-at-most-16 codewords. This package +does not rerun that census and does not call `scan.c` or the bit-lane +iterator. + +The engine call injects `population_planes` and `at_most` from +`research/e7-bitsliced-exhaustion/binary.py`. Those two helpers are +keyword-only on the intersection engine. The bit-lane `low_weight_words` +rejects the same keywords with `TypeError`, so this stream is the +intersection engine. + +`checked_rows` accepts a batch size only when it is an integer in `1..20`. +The verifier calls `low_weight_words` on the 36-tuple at each of those twenty +integers, and at the adjacent integers 0 and 21. This is an exhaustive finite +census of that batch-size domain on this one input. The completeness argument +is the engine's own range check, plus one call at every integer it accepts +and one call at each adjacent integer it rejects. + +| Call | Result | +|---|---| +| Batch sizes 1..20 on the 36 generators | `dimension exceeds 27`, 0 yields | +| Batch sizes 0 and 21, and the non-integers `True` and `20.0` | `invalid batch size`, 0 yields | +| Batch size 20 on the reversed 36-tuple | `dimension exceeds 27`, 0 yields | +| Two copies of the first generator | `dependent generators`, 0 yields | +| First 27 generators at batch size 10 | `batch count exceeds 65536`, 0 yields | +| First 27 generators at batch size 20 | admitted; the first yield is 0, then the stream is closed | +| 27 generators followed by a copy of the first | `dimension exceeds 27`, 0 yields | + +Batch size 20 is the named comparison. It is the only legal batch size for +which `36 - batch_size <= 16`, so it is the only legal size that would pass +the later guard `batch count exceeds 65536`. The message actually raised is +the dimension guard, which the engine checks while reading generator index +27, before that later guard and before any lane table. The refusal is raised +at zero-based index 27, the 28th generator, after the first 27 generators +have been accepted. The same message at +the other nineteen legal sizes is the same guard, not a lane-split +disagreement. No timing is recorded. + +The ordered 27-prefix is a separate linear fact, read off the identity +coordinates. The basis vector `i` is the unique vector in this basis with a +1 at free coordinate `i`. A recorded support therefore lies in the prefix +span exactly when its bits at free coordinates 48, 49, 50, 51, 52, 56, 58, +64 and 80 are all zero. The first three published supports lie in that span. +The other four do not: each has a 1 on at least one of those coordinates, and +reassembling it from the first 27 generators does not recover it. Truncating +this ordered basis to the engine's capacity cannot contain the eight-word +set. The prefix stream itself is not enumerated. One yielded zero shows that +the public function admits that shorter tuple; it is not a census of the +prefix. + +## Scope + +Task card `replay-runtime`, priority revision 8, base +`17469fff78c22941280f04d39dc5a1faee09c840`. Scope status is **refined**. + +The card asks for a measured speedup that keeps coverage. The revision-8 +verification row requires the sets to be compared before a faster replay +counts as the same coverage. The merged package +`research/e6-intersection-counter-support` answers that question for the E6 +64-word hash +`ad4a1d101774e6c2da40cde3d097d39aa56ee5668dcdca858513c5fec3578215`. +Open PR #7007 records this P112 hash and states that its verifier does not +call `research/e7-intersection-counters/engine.py`. The D6 16-word hash +`23a7b374a6bc62bc2aca47843d52a01fa8e791ed3a98085133829d816c5094e8` is a +different code. This package runs the engine on the P112 basis only. + +The selected record at this base is `781451/250000000`. The priorities page +on the same base still prints the older PR #5599 decimal. This package uses +the selected record and does not change it. Orientation +`python3 -B scripts/research_selected_baseline.py` printed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` with that same fraction. That command +checks source bindings only. + +Ordered overlap check on 2026-11-10, after fetching upstream `main` at +`17469fff78c22941280f04d39dc5a1faee09c840`. `scripts/find_overlap.py +--refresh --include-closed` searched `ff8861dab18040c0`, `p112 +intersection-counter`, and `dimension exceeds 27`. Coverage: local notes at +that head, 10180 records, complete inventory; 317 open PR bodies fetched at +`2026-11-10T08:49:18Z`; 6971 discussion records fetched at +`2026-11-10T08:50:22Z`; 6175 closed PR bodies fetched at +`2026-11-10T08:51:11Z`. The two matches are open PR #7007 and discussion +reply 19507785. Both record this hash for the bit-lane census and state that +the intersection-counter engine was not run. No closed PR body contains the +hash. The helper searches titles and bodies, not code diffs. + +This is a refusal census of a finite parameter, not a yielded-set symmetric +difference and not an enumeration of the `2^36` codewords. It does not say +what a copy of the engine would return if the dimension guard were raised. +It does not say that every generating set of length 27 misses the eight +words. A failed search was not used. + +## Reproduce + +Python 3.12 and the standard library, from the repository root. Rebuilding +the 1260 frames and refusing twenty batch sizes finishes in well under a +second. No compiler is required. + +```sh +python3 -B scripts/research_package.py --package research/p112-intersection-counter-capacity --check-only +python3 -I -B research/p112-intersection-counter-capacity/verify.py +python3 -I -O -B research/p112-intersection-counter-capacity/verify.py +python3 -B scripts/research_package.py --package research/p112-intersection-counter-capacity +``` + +The direct verifier prints + +```text +PASS_P112_INTERSECTION_COUNTER_CAPACITY batch=20 legal_batches=20 yielded=0 message=dimension exceeds 27 hash=ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3 returned=False prefix_misses=4 enumerated=false timed=false no_new_kappa=true +``` + +Checked here: normal and optimized direct runs, metadata check, and the +registered package runner. The 27-dimensional E7 census, the #5729 timing +harness, the bit-lane scan, the half-split census, Lean, and Docker were +not run. + +## Open next questions + +1. If an opt-in copy raises only the dimension guard from 27 to 36, does + batch size 20 on this same basis yield the eight-word set with the hash + above? The published function stops before the lane loop, so the refusal + leaves that arithmetic comparison open. The first step is a separate + harness that does not edit + `research/e7-intersection-counters/engine.py`. The blocker is the + 36-dimensional stream. This package does not remove the guard. + +2. Does some other independent generating set of length at most 27, still + inside this code, make the same engine return these eight words at batch + size 20? The seven supports span seven dimensions, so the length cap + alone does not forbid every admissible input. The ordered 27-prefix + misses four supports, and searching a different generating set is a + different question. The first step is to name one such 27-tuple and + compare one batch-size-20 stream with this hash. + +## Credit + +The 120-line order and the punctured frame are the model in +`research/p112-rank6-frame-coverage`, from the PR1226/PR1323 listing used +by Cinna Davis. The intersection-counter engine is Nick Petalas's +`research/e7-intersection-counters/engine.py`. The injected population and +threshold routines are Ali Romman's PR #5729. The 36-generator basis, the +seven supports, and the open engine question are PR #7007. The E6 comparison +is merged PR #6960. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review and no formal-kernel acceptance are claimed. diff --git a/research/p112-intersection-counter-capacity/SOURCES.json b/research/p112-intersection-counter-capacity/SOURCES.json new file mode 100644 index 0000000000..d0053431e7 --- /dev/null +++ b/research/p112-intersection-counter-capacity/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/e7-bitsliced-exhaustion/binary.py", + "usage": "input", + "git_blob": "cad9fc43ec0244bce415a76bc61b6445ffbd7519", + "sha256": "e79ad4d1d4be1748cf09aacc4274a316000d4b5922f13495778892b9309dc56e" + }, + { + "path": "research/e7-intersection-counters/engine.py", + "usage": "input", + "git_blob": "0283d450aee499682b0fd0ed0585e6d98085ef8a", + "sha256": "882d0177e990b0534bb16ec188a622b6167051505bdb5a7b19b4462499a72e47" + }, + { + "path": "research/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + } + ] +} diff --git a/research/p112-intersection-counter-capacity/TASK.json b/research/p112-intersection-counter-capacity/TASK.json new file mode 100644 index 0000000000..6765231c52 --- /dev/null +++ b/research/p112-intersection-counter-capacity/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Does research/e7-intersection-counters/engine.py return the same 8-word P112 set on the 36-generator basis whose positive-word SHA256 is ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3? The named batch size is 20, and every other legal batch size is included because the refusal happens before the lane split.", + "scope_change_reason": "The replay-runtime card asks for a measured speedup that keeps coverage. Priority revision 8 says faster output is equivalent coverage only after the sets are compared. Open PR #7007 records this 8-word hash and leaves the intersection-counter engine unrun. This package runs that engine on the recorded 36-generator basis. It records no timing and leaves the selected conditional exponent unchanged.", + "bottleneck_link": "A faster iterator can certify a code only when it returns that code's low-weight words. On this 36-generator basis the opt-in engine refuses the input, so it does not supply those words. The selected conditional exponent is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop after the engine call on this 36-generator basis. Do not edit the frozen engine, enumerate the 2^36 code, time either iterator, or compare the E6 or D6 support sets.", + "outcome": "negative-result", + "evidence": "The rebuilt kernel basis has the pinned free coordinates, weights, and generator-list SHA256 c93a6ec3f6d61b3bbf4086218c723761e517bc42ac2c26f551436d271a081e9d. The seven partition supports have SHA256 ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3. low_weight_words raises ValueError dimension exceeds 27 with zero yields at each batch size 1..20. Batch size 20 is the only legal size for which the later batch-count guard would admit 36 generators, and the observed message is still the dimension guard. The ordered 27-prefix is admitted and its span misses four of the seven supports. No codeword enumeration was run.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "If an opt-in copy raises only the dimension guard from 27 to 36, does batch size 20 on this same basis yield the eight-word set with hash ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3?", + "why_it_matters": "The published engine stops before the lane loop, so this refusal does not say whether the intersection arithmetic agrees with the recorded set.", + "first_step": "Leave research/e7-intersection-counters/engine.py unchanged. In a separate harness, admit dimension 36 at batch size 20 and compare the yielded set with this hash.", + "blocked_by": "That comparison is a 36-dimensional stream. This package stops at the published guard and does not modify the frozen engine." + }, + { + "question": "Does some other independent generating set of length at most 27, still inside this code, make the same engine return these eight words at batch size 20?", + "why_it_matters": "The cap rejects every 36-generator input. The seven supports span only seven dimensions, so a shorter admissible generating set is a different question from truncating this ordered basis.", + "first_step": "Name 27 independent generators of a subspace that contains all seven supports, call low_weight_words once at batch size 20, and compare the yielded set with this hash.", + "blocked_by": "The ordered 27-prefix of this basis misses four supports, and this package does not search another generating set. The 2^36 census that identifies the eight words remains PR #7007." + } + ] +} diff --git a/research/p112-intersection-counter-capacity/VERIFY.json b/research/p112-intersection-counter-capacity/VERIFY.json new file mode 100644 index 0000000000..514be3b3f1 --- /dev/null +++ b/research/p112-intersection-counter-capacity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e7-bitsliced-exhaustion/binary.py", + "research/e7-intersection-counters/engine.py", + "research/p112-rank6-frame-coverage/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Rebuild the P112 36-generator kernel and the seven recorded supports, require hash ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3, and require low_weight_words to raise dimension exceeds 27 with no yield at every legal batch size, including the named batch size 20. Check the 27-prefix admission and the four supports outside that prefix." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the same batch-size census under optimized bytecode. The checks are ValueError guards, so optimization does not disable them." + } + ] +} diff --git a/research/p112-intersection-counter-capacity/verify.py b/research/p112-intersection-counter-capacity/verify.py new file mode 100644 index 0000000000..6284a86be9 --- /dev/null +++ b/research/p112-intersection-counter-capacity/verify.py @@ -0,0 +1,453 @@ +#!/usr/bin/env python3 +"""The intersection-counter engine refuses the P112 36-generator basis. + +The basis is the F2 kernel of the 1260 live orthogonal 8-frames. The target +is the seven weight-16 supports recorded with hash +ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3. +low_weight_words is called at every legal batch size. Each call raises +before yielding. Batch size 20 is the named comparison. +""" + +import inspect +import json +from functools import partial +from hashlib import sha256 +from itertools import combinations, product +from pathlib import Path +from runpy import run_path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTH = 112 +FRAME_SIZE = 8 +FRAME_COUNT = 1260 +RANK = 76 +DIMENSION = 36 +DEGREE = 90 +WEIGHT_BOUND = 16 +SUPPORT_COUNT = 7 +NAMED_BATCH = 20 +LEGAL_BATCHES = tuple(range(1, 21)) +PREFIX = 27 +LATE = DIMENSION - PREFIX +FREE_COORDINATES = ( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16, 18, 20, 24, 25, 26, + 28, 30, 32, 34, 36, 40, 42, 48, 49, 50, 51, 52, 56, 58, 64, 80, +) +BASIS_WEIGHTS = ( + 38, 34, 38, 30, 42, 34, 26, 30, 42, 30, 50, 30, 38, 42, 34, 22, 32, 32, + 32, 30, 32, 32, 30, 22, 24, 36, 20, 36, 28, 36, 28, 32, 32, 32, 32, 32, +) +PUBLISHED_SUPPORTS = ( + 64691900160, + 1034819666160, + 280375465144335, + 4772259772306660006937399132160, + 15509841550538713979819718082560, + 1216944648758260568639796318044160, + 3955070108453721685622467917250560, +) +SUPPORT_SHA256 = ( + "ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3" +) +GENERATOR_SHA256 = ( + "c93a6ec3f6d61b3bbf4086218c723761e517bc42ac2c26f551436d271a081e9d" +) +JSON_LIST_SHA256 = ( + "3a316d6d3226f84c1e46e4447fa8d5fd800bff4a1bc6498152523cd4a602b69b" +) +PAIRS = ((0, 1), (2, 3), (4, 5), (6, 7)) +MATCHINGS = (((0, 3), (1, 2)), ((0, 2), (1, 3)), ((0, 1), (2, 3))) +SPINOR_REPS = ((0, 0, 0, 0), (0, 0, 1, 1), (0, 1, 0, 1), (0, 1, 1, 0)) +DIMENSION_MESSAGE = "dimension exceeds 27" +BATCH_COUNT_MESSAGE = "batch count exceeds 65536" +DEPENDENT_MESSAGE = "dependent generators" +BATCH_MESSAGE = "invalid batch size" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + sources = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + checked = 0 + for row in sources["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + digest = sha256(path.read_bytes()).hexdigest() + need(digest == row["sha256"], "input hash mismatch: " + row["path"]) + checked += 1 + need(checked == 3, "three live inputs") + return checked + + +def support_hash(words): + payload = json.dumps(sorted(words)).encode() + return sha256(payload).hexdigest() + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def canonical(vector): + first = next(value for value in vector if value) + return tuple(vector) if first > 0 else tuple(-value for value in vector) + + +def independent_lines(): + roots = [] + for i, j in combinations(range(8), 2): + for si, sj in product((2, -2), repeat=2): + root = [0] * 8 + root[i], root[j] = si, sj + roots.append(tuple(root)) + for signs in product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(signs) + need(len(roots) == len(set(roots)) == 240, "E8 root count") + lines = [] + seen = set() + for root in roots: + key = max(root, tuple(-value for value in root)) + if key not in seen: + seen.add(key) + lines.append(root) + need(len(lines) == 120, "E8 line count") + puncture = [] + for pair in range(4): + for sign in (1, -1): + root = [0] * 8 + root[2 * pair] = 2 + root[2 * pair + 1] = 2 * sign + puncture.append(lines.index(tuple(root))) + return tuple(lines), tuple(puncture) + + +def pinned_model(): + model = run_path( + str(ROOT / "research/p112-rank6-frame-coverage/engine.py"), + run_name="p112_capacity_model", + )["model"]() + lines = tuple(tuple(row) for row in model["lines"]) + puncture = tuple(model["punctured_frame"]) + live = tuple(model["live"]) + own_lines, own_puncture = independent_lines() + need(lines == own_lines, "pinned lines differ from the E8 builder") + need(puncture == own_puncture, "pinned puncture differs") + need(live == tuple(i for i in range(120) if i not in set(puncture)), "live order") + need(len(live) == WIDTH, "width") + need(all(dot(line, line) == 8 for line in lines), "norms") + return lines, live + + +def orthogonal_frames(lines, live): + adjacency = [] + for index in live: + mask = 0 + for bit, other in enumerate(live): + if index != other and dot(lines[index], lines[other]) == 0: + mask |= 1 << bit + adjacency.append(mask) + frames = [] + stack = [((), (1 << WIDTH) - 1)] + steps = 0 + while stack: + steps += 1 + need(steps <= 200000, "frame enumeration exceeded its state cap") + chosen, candidates = stack.pop() + if len(chosen) == FRAME_SIZE: + frames.append(chosen) + continue + need_more = FRAME_SIZE - len(chosen) + while candidates: + if candidates.bit_count() < need_more: + break + bit = candidates & -candidates + candidates ^= bit + index = bit.bit_length() - 1 + stack.append((chosen + (index,), candidates & adjacency[index])) + frames = tuple(sorted(frames)) + need(len(frames) == len(set(frames)) == FRAME_COUNT, "live 8-frame count") + degree = [0] * WIDTH + for frame in frames: + need(len(frame) == FRAME_SIZE, "frame length") + for index in frame: + degree[index] += 1 + need( + all(dot(lines[live[i]], lines[live[j]]) == 0 + for i, j in combinations(frame, 2)), + "frame not orthogonal", + ) + need(set(degree) == {DEGREE}, "frame degree") + need(steps == 56262, "frame search did not finish in 56262 states") + return frames + + +def kernel(rows): + pivots = {} + for row in rows: + reduced = row + while reduced: + pivot = reduced.bit_length() - 1 + if pivot in pivots: + reduced ^= pivots[pivot] + else: + pivots[pivot] = reduced + break + order = sorted(pivots) + for pivot in order: + row = pivots[pivot] + for other in order: + if other != pivot and (pivots[other] >> pivot) & 1: + pivots[other] ^= row + free = tuple(j for j in range(WIDTH) if j not in pivots) + need(len(pivots) == RANK and free == FREE_COORDINATES, "P112 frame-code rank") + basis = [] + for coordinate in free: + vector = 1 << coordinate + for pivot in order: + if (pivots[pivot] & vector).bit_count() % 2: + vector |= 1 << pivot + basis.append(vector) + basis = tuple(basis) + need(tuple(vector.bit_count() for vector in basis) == BASIS_WEIGHTS, + "basis weights changed") + for index, vector in enumerate(basis): + pattern = tuple((vector >> place) & 1 for place in free) + identity = tuple(int(place == index) for place in range(DIMENSION)) + need(pattern == identity, "free coordinates are not a basis identity") + need(0 < vector < 1 << WIDTH, "kernel vector outside F_2^112") + need(all((vector & row).bit_count() % 2 == 0 for row in rows), + "a frame parity survives") + digest = sha256(json.dumps(list(basis)).encode()).hexdigest() + need(digest == GENERATOR_SHA256, "generator-list hash " + digest) + return basis + + +def partition_masks(lines, live): + by_root = {lines[old]: bit for bit, old in enumerate(live)} + + def pair_mask(matching): + mask = 0 + for left, right in matching: + for i in PAIRS[left]: + for j in PAIRS[right]: + for sign in (1, -1): + root = [0] * 8 + root[i] = 2 + root[j] = 2 * sign + mask |= 1 << by_root[canonical(root)] + return mask + + spinors = [ + lines[old] for old in live if all(abs(value) == 1 for value in lines[old]) + ] + need(len(spinors) == 64, "spinor line count") + + def relative(root): + return tuple( + 0 if root[2 * pair] == root[2 * pair + 1] else 1 for pair in range(4) + ) + + def spin_mask(representative): + patterns = {representative, tuple(1 - bit for bit in representative)} + mask = 0 + for root in spinors: + if relative(root) in patterns: + mask |= 1 << by_root[root] + return mask + + masks = tuple(pair_mask(item) for item in MATCHINGS) + tuple( + spin_mask(item) for item in SPINOR_REPS + ) + covered = 0 + for mask in masks: + need(mask.bit_count() == WEIGHT_BOUND, "partition block weight") + need(covered & mask == 0, "partition blocks meet") + covered |= mask + need(covered == (1 << WIDTH) - 1, "partition misses a live line") + return masks + + +def bind_engine(): + binary = run_path( + str(ROOT / "research/e7-bitsliced-exhaustion/binary.py"), + run_name="p112_capacity_population", + ) + engine_ns = run_path( + str(ROOT / "research/e7-intersection-counters/engine.py"), + run_name="p112_capacity_engine", + ) + engine = engine_ns["low_weight_words"] + signature = inspect.signature(engine) + for name in ("population_planes", "at_most"): + parameter = signature.parameters[name] + need(parameter.kind is inspect.Parameter.KEYWORD_ONLY, + name + " is not keyword-only on the intersection engine") + try: + binary["low_weight_words"]( + (1,), 1, 0, 1, + population_planes=binary["population_planes"], + at_most=binary["at_most"], + ) + except TypeError: + separated = True + else: + separated = False + need(separated, "the bit-lane enumerator accepted the intersection keywords") + bound = partial( + engine, + population_planes=binary["population_planes"], + at_most=binary["at_most"], + ) + return bound, engine_ns["checked_rows"] + + +def stream_outcome(engine, generators, batch, limit): + """Read at most `limit` yields. A ValueError aborts the stream.""" + stream = engine(generators, WIDTH, WEIGHT_BOUND, batch) + yielded = [] + try: + for word in stream: + yielded.append(word) + if len(yielded) >= limit: + break + except ValueError as exc: + return yielded, str(exc) + finally: + stream.close() + return yielded, None + + +def require_refusal(engine, generators, batch): + yielded, message = stream_outcome(engine, generators, batch, 1) + need(yielded == [], "a refused call yielded " + str(len(yielded)) + " words") + need(message == DIMENSION_MESSAGE, "unexpected refusal: " + str(message)) + return message + + +def coordinate_word(word, basis, free): + assembled = 0 + for bit, vector in zip(free, basis): + if (word >> bit) & 1: + assembled ^= vector + return assembled + + +def prefix_split(supports, basis): + """Split the seven supports by the identity coordinates of this basis.""" + inside = [] + outside = [] + for word in supports: + need(coordinate_word(word, basis, FREE_COORDINATES) == word, + "a recorded support is outside this kernel basis") + late = [bit for bit in FREE_COORDINATES[PREFIX:] if (word >> bit) & 1] + short = coordinate_word(word, basis[:PREFIX], FREE_COORDINATES[:PREFIX]) + if late: + outside.append(word) + need(short != word, "a late support still lay in the 27-prefix") + else: + inside.append(word) + need(short == word, "a zero late-coordinate support left the 27-prefix span") + return inside, outside + + +def guard_controls(engine, checked_rows, basis): + yielded, message = stream_outcome(engine, (basis[0], basis[0]), NAMED_BATCH, 1) + need(yielded == [] and message == DEPENDENT_MESSAGE, + "a repeated generator produced " + str(message)) + yielded, message = stream_outcome(engine, basis[:PREFIX], 10, 1) + need(yielded == [] and message == BATCH_COUNT_MESSAGE, + "the 27-prefix at batch 10 produced " + str(message)) + rows, count = checked_rows(basis[:PREFIX], WIDTH, WEIGHT_BOUND, NAMED_BATCH) + need(len(rows) == PREFIX and count == NAMED_BATCH, + "batch 20 rejected the 27-prefix inside checked_rows") + yielded, message = stream_outcome(engine, basis[:PREFIX], NAMED_BATCH, 1) + need(message is None and yielded == [0], + "the admitted 27-prefix did not yield zero first") + duplicated = basis[:PREFIX] + (basis[0],) + require_refusal(engine, duplicated, NAMED_BATCH) + for batch in (0, 21, True, 20.0): + yielded, message = stream_outcome(engine, basis, batch, 1) + need(yielded == [] and message == BATCH_MESSAGE, + "batch " + repr(batch) + " produced " + str(message)) + require_refusal(engine, tuple(reversed(basis)), NAMED_BATCH) + + +def check(): + need(sha256(json.dumps([1, 2]).encode()).hexdigest() == JSON_LIST_SHA256, + "JSON list encoding changed") + need(len(FREE_COORDINATES) == DIMENSION and len(BASIS_WEIGHTS) == DIMENSION, + "pinned basis shape") + need(len(LEGAL_BATCHES) == 20 and NAMED_BATCH in LEGAL_BATCHES, "batch domain") + need(DIMENSION - NAMED_BATCH == 16 and DIMENSION - 16 > 16, + "batch 20 is the only legal size whose later guard admits dimension 36") + authenticate() + lines, live = pinned_model() + frames = orthogonal_frames(lines, live) + rows = tuple(sum(1 << index for index in frame) for frame in frames) + basis = kernel(rows) + supports = partition_masks(lines, live) + need(set(supports) == set(PUBLISHED_SUPPORTS), "partition integers changed") + digest = support_hash(supports) + need(digest == SUPPORT_SHA256, "rebuilt support hash " + digest) + dropped = support_hash(PUBLISHED_SUPPORTS[1:]) + need(dropped != SUPPORT_SHA256, "dropping one support kept the hash") + need(all(all((word & row).bit_count() % 2 == 0 for row in rows) for word in supports), + "a recorded support leaves a frame") + inside, outside = prefix_split(PUBLISHED_SUPPORTS, basis) + need(inside == list(PUBLISHED_SUPPORTS[:3]), "prefix membership of the first three") + need(outside == list(PUBLISHED_SUPPORTS[3:]), "four supports use a later generator") + engine, checked_rows = bind_engine() + for batch in LEGAL_BATCHES: + require_refusal(engine, basis, batch) + guard_controls(engine, checked_rows, basis) + return { + "status": "PASS_P112_INTERSECTION_COUNTER_CAPACITY", + "claim": "exhaustive finite census of legal batch sizes on one input", + "width": WIDTH, + "frames": FRAME_COUNT, + "rank": RANK, + "dimension": DIMENSION, + "named_batch": NAMED_BATCH, + "legal_batches": list(LEGAL_BATCHES), + "engine_message": DIMENSION_MESSAGE, + "words_yielded": 0, + "engine_returned_set": False, + "sets_equal": False, + "disagreement": "capacity refusal before any yield", + "supports_sha256": digest, + "positive_supports": SUPPORT_COUNT, + "prefix_contains_supports": len(inside), + "prefix_misses_supports": len(outside), + "generator_sha256": GENERATOR_SHA256, + "codeword_enumeration": False, + "bit_lane_iterator_replayed": False, + "half_split_census_replayed": False, + "e7_census_replayed": False, + "timing_measured": False, + "selected_kappa": "781451/250000000", + "kappa_changed": False, + } + + +if __name__ == "__main__": + result = check() + print( + "PASS_P112_INTERSECTION_COUNTER_CAPACITY" + " batch={named_batch}" + " legal_batches={count}" + " yielded={words_yielded}" + " message={engine_message}" + " hash={supports_sha256}" + " returned={engine_returned_set}" + " prefix_misses={prefix_misses_supports}" + " enumerated=false" + " timed=false" + " no_new_kappa=true".format(count=len(result["legal_batches"]), **result) + ) + print(json.dumps(result, indent=2, sort_keys=True))