diff --git a/research/p112-punctured-frame-code/README.md b/research/p112-punctured-frame-code/README.md new file mode 100644 index 0000000000..9c9f80141a --- /dev/null +++ b/research/p112-punctured-frame-code/README.md @@ -0,0 +1,197 @@ +# The P112 punctured frame code matches the bit-lane iterator + +**Coverage check of a published replay engine on one P112 deletion. No new κ.** +The selected conditional exponent stays `781451/250000000`. On the 112 lines +left by one pinned orthogonal 8-frame, `low_weight_words` returns exactly the +words of weight at most 16 in the F2 incidence code of the 1260 orthogonal +8-frames. That code is 36-dimensional. Zero and exactly seven weight-16 words +occur, and no nonzero word is lighter. + +## Result + +The root list is the coordinate complement in +`research/p112-rank6-frame-coverage/engine.py`. The eight punctured lines are + +```text +(2, 2, 0, 0, 0, 0, 0, 0), (2, -2, 0, 0, 0, 0, 0, 0), +(0, 0, 2, 2, 0, 0, 0, 0), (0, 0, 2, -2, 0, 0, 0, 0), +(0, 0, 0, 0, 2, 2, 0, 0), (0, 0, 0, 0, 2, -2, 0, 0), +(0, 0, 0, 0, 0, 0, 2, 2), (0, 0, 0, 0, 0, 0, 2, -2) +``` + +at positions `0, 1, 26, 27, 44, 45, 54, 55` in that file's 120-line order. +They are pairwise orthogonal and each has norm 8. The stored live lines are +the other 112 lines, in increasing position. An independent E8 builder +reproduces the same ordered list. Its SHA256, of `json.dumps` of the 112 +coordinate lists, is +`4db9ba14034f55b0b95d69451e809a0c3bf618473209ae3d47d4992e180d14ab`. + +An orthogonal 8-frame is an 8-clique in the live orthogonality graph. There +are 1260 such frames, and every live line lies in 90 of them. The F2 +incidence matrix has rank 76. A 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) +``` + +is orthogonal to every frame row. + +| Quantity | Value | +|---|---:| +| Lines | 112 | +| Orthogonal 8-frames | 1260 | +| Incidence rank | 76 | +| Kernel dimension | 36 | +| Distinct codewords | 68719476736 | +| Least positive weight | 16 | +| Words of weight 16 | 7 | +| Words of weight at most 16 | 8 | + +The seven weight-16 words are disjoint and cover every live line, so their +symmetric difference is the all-ones word. With the axis pairs +`A={0,1}`, `B={2,3}`, `C={4,5}`, `D={6,7}`, they are: + +1. Both signs of every root joining `A` with `D`, or `B` with `C`. +2. Both signs of every root joining `A` with `C`, or `B` with `D`. +3. Both signs of every root joining `A` with `B`, or `C` with `D`. +4.–7. The spinor lines whose four within-pair sign disagreements lie in + `{0000,1111}`, `{0011,1100}`, `{0101,1010}`, or `{0110,1001}`. + +That description does not use the bit-lane engine. Each of the seven blocks +meets every live 8-frame evenly. Moving the top bit of the first block onto +the top bit of the second leaves a weight-16 word outside the seven, and +that word fails a frame parity. + +The blocks, as integers in the pinned live order, are + +```text +64691900160 +1034819666160 +280375465144335 +4772259772306660006937399132160 +15509841550538713979819718082560 +1216944648758260568639796318044160 +3955070108453721685622467917250560 +``` + +Their SHA256, of `json.dumps` of that sorted list, is +`ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. + +`scan.c` lists each half of the ordered basis by doubling. Splits after 18 +generators and after 16 generators each visit `2^36` codewords once. They +return one weight distribution, symmetric under complement, with the eight +words above as the weight-at-most-16 set: + +```text +0:1 16:7 20:336 22:3584 24:3752 26:10752 28:6864 30:50176 +32:872613 34:2243584 36:5633600 38:21482496 40:123827424 +42:275960832 44:878407488 46:1531507712 48:3797117779 +50:4774038528 52:8574631520 54:8427087872 56:11893702896 +58:8427087872 60:8574631520 62:4774038528 64:3797117779 +66:1531507712 68:878407488 70:275960832 72:123827424 +74:21482496 76:5633600 78:2243584 80:872613 82:50176 +84:6864 86:10752 88:3752 90:3584 92:336 96:7 112:1 +``` + +`low_weight_words` from `research/e7-bitsliced-exhaustion/binary.py`, at +batch size 20, returns that same eight-word set and no repeated yield. These +enumerations do not call each other. Batch size 16 was not run: one scan of +this dimension is the registered comparison. A copy of the set with one +support removed compares unequal. Clearing the top bit of a support produces +a weight-15 word that fails a frame parity, and the weight predicate rejects +a set that contains it. The engine rejects a repeated generator. On +generators `(1, 2, 4)`, weight bound 1 returns `{0,1,2,4}` and weight bound +0 returns only zero. + +## Scope + +Task card `replay-runtime`, priority revision 8, base +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Scope status is **refined**. + +The card asks for a new measured speedup that keeps coverage. The +revision-8 verification row instead says that faster output is not the same +coverage until checked. The merged E7 package compared the 27-dimensional +kernel. The E6 package compared width 36 and weight 16. This package is the +P112 half of the question that package left open. Width 112, weight bound +16, thirty-six generators. It does not time the engine, replace a consumer, +rerun the E6 or D6 census, or call the intersection-counter engine. + +The selected record's κ is `781451/250000000`. The priority note on this +base still quotes the older displayed value `0.00310045` from PR #5599. +This package uses the selected record and does not change it. + +Ordered overlap check on 2026-11-10, after fetching upstream `main` at +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. `scripts/find_overlap.py +--refresh` read 895 open pull requests and 6951 discussion records +(discussions fetched `2026-11-10T02:33:54Z`). The phrases "P112 punctured +frame", "p112 frame code", "punctured frame code" and "orthogonal 8-frame +incidence" matched three items, none of which builds this kernel. Open +#6948 is the E6 comparison and asks this question. Discussion reply +19507129 compares the intersection counter with the E6 64-word set and +names this P112 question as out of scope. Discussion reply 19507177 is the +D6 width-30 comparison. No fork `cursor/*` branch had named this P112 +frame-code comparison before this one. + +This is an exhaustive finite census of one finite code: all `2^36` kernel +words, through two half-splits, plus the engine's weight-at-most-16 yield +on the same basis. It is not a proof that the iterator is correct for every +generator matrix, and it is not an unrestricted nonexistence result. A +failed search was not used. The E6 and D6 equalities are not claimed as +P112 results. + +## Reproduce + +Python 3.12, `gcc`, and the standard library, from the repository root. The +two registered commands split the work because together they measured 608 +seconds on this host, above the 600-second command limit. The half-split +census is the shorter command. The engine batch is the longer one: a +separate run of that batch measured 494 seconds. + +```sh +python3 -B scripts/research_package.py --package research/p112-punctured-frame-code --check-only +python3 -I -B research/p112-punctured-frame-code/verify.py census +python3 -I -B research/p112-punctured-frame-code/verify.py engine +python3 -I -B research/p112-punctured-frame-code/verify.py +python3 -B scripts/research_package.py --package research/p112-punctured-frame-code +``` + +`verify.py` with no argument runs both parts in one process. With `census` +or `engine` it runs one part. The combined process prints + +```text +PASS_P112_PUNCTURED_FRAME_CODE width=112 frames=1260 dimension=36 minimum=16 supports=7 codewords=68719476736 mode=all batches=20 splits=18,16 e6_replayed=false d6_replayed=false no_new_kappa=true +``` + +Not run: the #5729 timing harness, a second engine batch, the E6 4-frame +census, the D6 6-frame census, the E7 kernel, +`research/e7-intersection-counters/engine.py`, Lean, Docker, and +`scripts/research_selected_baseline.py` as a scientific replay. The +selected record is provenance only. + +## Open next questions + +1. Does one reflected copy of this coordinate frame induce the same set + equality after the root list is transported? This pin is one orthogonal + 8-frame. First reflect one punctured root by one simple E8 root, rebuild + the 112-line list, and compare one half-split with the transported + images of these seven supports. +2. Does the opt-in intersection-counter engine return this same 8-word set? + A faster substitute is not coverage for this basis until the sets are + compared. This is not the E6 64-word hash and not the D6 16-word set. + First run `research/e7-intersection-counters/engine.py` on this + 36-generator basis at one batch size and compare it with the support + hash above. + +## Credit + +The 120-line coordinate order and this punctured frame are the model in +`research/p112-rank6-frame-coverage`, from the PR1226/PR1323 E8 listing +used by Cinna Davis. The bit-lane engine is Ali Romman's PR #5729, +`research/e7-bitsliced-exhaustion/binary.py`. The request to bind one other +code is the open question of the E6 frame-code comparison, open as #6948. +The D6 width-30 comparison is a different deletion and is not redone here. + +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-punctured-frame-code/SOURCES.json b/research/p112-punctured-frame-code/SOURCES.json new file mode 100644 index 0000000000..a57d0e1b59 --- /dev/null +++ b/research/p112-punctured-frame-code/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + } + ] +} diff --git a/research/p112-punctured-frame-code/TASK.json b/research/p112-punctured-frame-code/TASK.json new file mode 100644 index 0000000000..c10cf031d3 --- /dev/null +++ b/research/p112-punctured-frame-code/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "On the 112 live lines of the pinned coordinate-frame complement, does low_weight_words return exactly the weight-at-most-16 words of the 36-dimensional F2 incidence code of the 1260 orthogonal 8-frames?", + "scope_change_reason": "The replay-runtime card asks for a new measured speedup. The revision-8 verification row says a published faster replay is not equivalent coverage until checked. The merged E7 comparison and the E6 4-frame comparison already bound two codes. This package answers the P112 half of the question those comparisons left open. It does not time an engine or install one.", + "bottleneck_link": "Deletion and decoder certificates reuse this iterator only if another code still returns every low-weight word. This comparison binds that iterator to one P112 punctured frame code. It does not change a supplier bill or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after one P112 incidence code, two half-splits of its kernel, and one engine batch. Do not remeasure timings, rerun the E6 or D6 census, or load the intersection-counter engine.", + "outcome": "completed", + "evidence": "The incidence matrix of 1260 orthogonal 8-frames on the 112 live lines has F2 rank 76 and kernel dimension 36, with the recorded free coordinates. Half-splits after 18 and after 16 generators agree on all 2^36 weights. The only words of weight at most 16 are zero and seven disjoint weight-16 blocks, which are the three cross-pair matchings and the four even spinor pairs of the coordinate frame. low_weight_words at batch size 20 returns that set. A moved block, a weight-15 injection, a dropped support, and a repeated generator fail.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does one reflected copy of this coordinate frame induce the same set equality after the root list is transported?", + "why_it_matters": "This pin is one orthogonal 8-frame. A second frame is a different ordered basis even if the parameters match.", + "first_step": "Reflect one punctured root by one simple E8 root, rebuild the 112-line list, and compare one half-split with the transported images of these seven supports.", + "blocked_by": "No second frame is pinned in this package." + }, + { + "question": "Does the opt-in intersection-counter engine return this same 8-word set?", + "why_it_matters": "A faster substitute is not coverage for this basis until the sets are compared. This is not the E6 64-word hash and not the D6 16-word set.", + "first_step": "Run research/e7-intersection-counters/engine.py on this 36-generator basis at one batch size and compare it with the support hash recorded here.", + "blocked_by": "This package does not load that engine." + } + ] +} diff --git a/research/p112-punctured-frame-code/VERIFY.json b/research/p112-punctured-frame-code/VERIFY.json new file mode 100644 index 0000000000..eb15df88c0 --- /dev/null +++ b/research/p112-punctured-frame-code/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e7-bitsliced-exhaustion/binary.py", + "research/p112-rank6-frame-coverage/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "census" + ], + "timeout_seconds": 300, + "checks": "Hash the two live inputs, rebuild the 1260 live 8-frames, and compare half-splits at 18 and 16 generators with the geometric partition of seven weight-16 blocks. Reject a block that moves one bit between the first two blocks." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "engine" + ], + "timeout_seconds": 600, + "checks": "Rebuild the same kernel basis and compare low_weight_words at batch 20 and weight 16 with the seven-block partition. Reject a dropped support, a weight-15 injection, a repeated generator, and a toy bound change." + } + ] +} diff --git a/research/p112-punctured-frame-code/scan.c b/research/p112-punctured-frame-code/scan.c new file mode 100644 index 0000000000..5135cf4656 --- /dev/null +++ b/research/p112-punctured-frame-code/scan.c @@ -0,0 +1,192 @@ +/* Half-split census of one ordered binary basis of length 112 and dimension 36. + * + * Each generator is a 112-bit integer, written as 28 lowercase hex digits. + * A split s lists the span of the first s generators and the span of the + * rest by doubling. Every codeword is the XOR of exactly one pair. The + * integer popcount is the Hamming weight. This file does not implement the + * bit-lane iterator. + * + * Apache-2.0. + */ +#include +#include +#include +#include +#include +#include + +enum { DIM = 36, MAX_LOW = 64 }; + +typedef struct { uint64_t lo, hi; } Word; + +static Word basis[DIM]; +static Word *low_words; +static Word *high_words; +static size_t n_low; +static size_t n_high; +static pthread_mutex_t low_mu = PTHREAD_MUTEX_INITIALIZER; +static Word low_found[MAX_LOW]; +static int n_low_found; +static int overflow; + +typedef struct { + size_t begin, end; + uint64_t hist[113]; + uint64_t seen; +} Job; + +static Word wxor(Word a, Word b) { + Word c; + c.lo = a.lo ^ b.lo; + c.hi = a.hi ^ b.hi; + return c; +} + +static int weight(uint64_t lo, uint64_t hi) { + return __builtin_popcountll(lo) + __builtin_popcountll(hi); +} + +static int hex_value(char ch) { + if (ch >= '0' && ch <= '9') return ch - '0'; + if (ch >= 'a' && ch <= 'f') return ch - 'a' + 10; + return -1; +} + +static int load_basis(const char *path) { + FILE *fp = fopen(path, "r"); + char hex[80]; + if (!fp) return 0; + for (int i = 0; i < DIM; i++) { + uint64_t lo = 0, hi = 0; + if (fscanf(fp, "%79s", hex) != 1 || strlen(hex) != 28) { + fclose(fp); + return 0; + } + for (int k = 0; k < 28; k++) { + int v = hex_value(hex[k]); + if (v < 0) { + fclose(fp); + return 0; + } + hi = (hi << 4) | (lo >> 60); + lo = (lo << 4) | (unsigned)v; + } + if (hi >> 48) { + fclose(fp); + return 0; + } + basis[i].lo = lo; + basis[i].hi = hi; + } + fclose(fp); + return 1; +} + +static void span(Word *out, int start, int count, size_t expected) { + size_t len = 1; + out[0].lo = 0; + out[0].hi = 0; + for (int i = 0; i < count; i++) { + Word g = basis[start + i]; + for (size_t j = 0; j < len; j++) out[len + j] = wxor(out[j], g); + len <<= 1; + } + if (len != expected) { + fprintf(stderr, "span length mismatch\n"); + exit(1); + } +} + +static void *worker(void *arg) { + Job *job = arg; + memset(job->hist, 0, sizeof job->hist); + job->seen = 0; + for (size_t i = job->begin; i < job->end; i++) { + uint64_t hlo = high_words[i].lo; + uint64_t hhi = high_words[i].hi; + for (size_t j = 0; j < n_low; j++) { + uint64_t lo = hlo ^ low_words[j].lo; + uint64_t hi = hhi ^ low_words[j].hi; + int wt = weight(lo, hi); + job->hist[wt]++; + job->seen++; + if (wt <= 16 && wt) { + pthread_mutex_lock(&low_mu); + if (n_low_found >= MAX_LOW) overflow = 1; + else { + low_found[n_low_found].lo = lo; + low_found[n_low_found].hi = hi; + n_low_found++; + } + pthread_mutex_unlock(&low_mu); + } + } + } + return NULL; +} + +int main(int argc, char **argv) { + int split, threads, rc = 0; + long cpus; + Job *jobs; + pthread_t *ids; + uint64_t hist[113]; + uint64_t seen = 0; + if (argc != 3) { + fprintf(stderr, "usage: scan BASIS SPLIT\n"); + return 2; + } + split = atoi(argv[2]); + if (split < 1 || split >= DIM || !load_basis(argv[1])) { + fprintf(stderr, "bad basis or split\n"); + return 2; + } + n_low = 1ull << split; + n_high = 1ull << (DIM - split); + low_words = calloc(n_low, sizeof(Word)); + high_words = calloc(n_high, sizeof(Word)); + if (!low_words || !high_words) return 1; + span(low_words, 0, split, n_low); + span(high_words, split, DIM - split, n_high); + cpus = sysconf(_SC_NPROCESSORS_ONLN); + if (cpus < 1) cpus = 1; + if (cpus > 4) cpus = 4; + threads = (int)cpus; + jobs = calloc((size_t)threads, sizeof(Job)); + ids = calloc((size_t)threads, sizeof(pthread_t)); + if (!jobs || !ids) return 1; + for (int t = 0; t < threads; t++) { + size_t chunk = n_high / (size_t)threads; + jobs[t].begin = (size_t)t * chunk; + jobs[t].end = (t + 1 == threads) ? n_high : ((size_t)t + 1) * chunk; + if (pthread_create(&ids[t], NULL, worker, &jobs[t]) != 0) return 1; + } + memset(hist, 0, sizeof hist); + for (int t = 0; t < threads; t++) { + pthread_join(ids[t], NULL); + seen += jobs[t].seen; + for (int w = 0; w < 113; w++) hist[w] += jobs[t].hist[w]; + } + if (overflow) { + fprintf(stderr, "more than %d words of weight 1..16\n", MAX_LOW); + return 1; + } + printf("SPLIT %d\n", split); + printf("SEEN %llu\n", (unsigned long long)seen); + for (int i = 0; i < DIM; i++) { + printf("BASIS %d %d\n", i, weight(basis[i].lo, basis[i].hi)); + } + for (int w = 0; w < 113; w++) { + if (hist[w]) printf("HIST %d %llu\n", w, (unsigned long long)hist[w]); + } + for (int i = 0; i < n_low_found; i++) { + printf("LOW %012llx%016llx\n", + (unsigned long long)low_found[i].hi, + (unsigned long long)low_found[i].lo); + } + free(jobs); + free(ids); + free(low_words); + free(high_words); + return rc; +} diff --git a/research/p112-punctured-frame-code/verify.py b/research/p112-punctured-frame-code/verify.py new file mode 100644 index 0000000000..08c4c7df2b --- /dev/null +++ b/research/p112-punctured-frame-code/verify.py @@ -0,0 +1,467 @@ +#!/usr/bin/env python3 +"""Coverage of the published bit-lane iterator on one P112 punctured frame code. + +The half-split census is scan.c. It lists each half of an ordered kernel +basis by doubling and scores high XOR low by integer popcount. It does not +call low_weight_words. The engine is then compared with that set on this +basis alone. +""" + +import json +import subprocess +import sys +import tempfile +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 +CODEWORDS = 1 << DIMENSION +SPLIT_POINTS = (18, 16) +ENGINE_BATCH = 20 +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)) +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, +) +LINE_SHA256 = "4db9ba14034f55b0b95d69451e809a0c3bf618473209ae3d47d4992e180d14ab" +SUPPORT_SHA256 = "ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3" +HISTOGRAM = { + 0: 1, + 16: 7, + 20: 336, + 22: 3584, + 24: 3752, + 26: 10752, + 28: 6864, + 30: 50176, + 32: 872613, + 34: 2243584, + 36: 5633600, + 38: 21482496, + 40: 123827424, + 42: 275960832, + 44: 878407488, + 46: 1531507712, + 48: 3797117779, + 50: 4774038528, + 52: 8574631520, + 54: 8427087872, + 56: 11893702896, + 58: 8427087872, + 60: 8574631520, + 62: 4774038528, + 64: 3797117779, + 66: 1531507712, + 68: 878407488, + 70: 275960832, + 72: 123827424, + 74: 21482496, + 76: 5633600, + 78: 2243584, + 80: 872613, + 82: 50176, + 84: 6864, + 86: 10752, + 88: 3752, + 90: 3584, + 92: 336, + 96: 7, + 112: 1, +} + + +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 == 2, "two live inputs") + return checked + + +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 in (2, -2): + for sj in (2, -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 lines, tuple(puncture) + + +def pinned_model(): + model = run_path( + str(ROOT / "research/p112-rank6-frame-coverage/engine.py"), + run_name="p112_frame_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 == tuple(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(lines[i], lines[i]) == 8 for i in range(120)), "norms") + need(all(dot(lines[i], lines[j]) == 0 for i, j in combinations(puncture, 2)), + "punctured frame is not orthogonal") + roots = [list(lines[i]) for i in live] + digest = sha256(json.dumps(roots).encode()).hexdigest() + need(digest == LINE_SHA256, "live root-list hash") + return lines, puncture, 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 <= 5000000, "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") + for frame in frames: + need(all(dot(lines[live[i]], lines[live[j]]) == 0 + for i, j in combinations(frame, 2)), "frame not orthogonal") + 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 + need(all((vector & row).bit_count() % 2 == 0 for row in rows), + "a frame parity survives") + basis.append(vector) + weights = tuple(vector.bit_count() for vector in basis) + need(weights == 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") + return tuple(basis) + + +def relative_differences(root): + return tuple(0 if root[2 * pair] == root[2 * pair + 1] else 1 for pair in range(4)) + + +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 spin_mask(representative): + patterns = {representative, tuple(1 - bit for bit in representative)} + mask = 0 + for root in spinors: + if relative_differences(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 in_code(mask, rows): + return all((mask & row).bit_count() % 2 == 0 for row in rows) + + +def compile_scan(work): + binary = work / "scan" + subprocess.run( + ["gcc", "-O3", "-std=c11", "-pthread", "-Wall", "-Werror", + "-o", str(binary), str(HERE / "scan.c")], + check=True, cwd=work, timeout=60, + ) + return binary + + +def run_split(binary, basis, split, work): + path = work / ("basis-%d.txt" % split) + path.write_text("".join("%028x\n" % vector for vector in basis), encoding="ascii") + completed = subprocess.run( + [str(binary), str(path), str(split)], + check=True, capture_output=True, text=True, timeout=180, + ) + need(completed.stderr == "", "scan wrote to stderr") + histogram = {} + found = [] + seen = None + reported = None + weights = [] + for line in completed.stdout.splitlines(): + kind, *rest = line.split() + if kind == "SPLIT": + reported = int(rest[0]) + elif kind == "SEEN": + seen = int(rest[0]) + elif kind == "HIST": + histogram[int(rest[0])] = int(rest[1]) + elif kind == "LOW": + found.append(int(rest[0], 16)) + elif kind == "BASIS": + weights.append(int(rest[1])) + else: + raise ValueError("unexpected scan line") + need(reported == split, "scan split") + need(seen == CODEWORDS, "half-split missed a codeword") + need(tuple(weights) == BASIS_WEIGHTS, "scan read a different basis") + need(histogram == HISTOGRAM, "weight distribution changed at split " + str(split)) + need(sum(histogram.values()) == CODEWORDS, "histogram sum") + for weight, count in histogram.items(): + need(histogram[WIDTH - weight] == count, "complement asymmetry") + supports = set(found) + need(len(found) == len(supports) == SUPPORT_COUNT, "support count") + need(all(word.bit_count() == WEIGHT_BOUND for word in supports), "a lighter positive word") + need(min(weight for weight in histogram if weight) == WEIGHT_BOUND, "minimum left 16") + return supports + + +def engine_words(engine, basis, maximum, batch_bits): + listed = list(engine(basis, WIDTH, maximum, batch_bits)) + need(len(listed) == len(set(listed)), "engine repeated a word") + return set(listed) + + +def positive_words_have_weight(words, weight): + return all(word.bit_count() == weight for word in words if word) + + +def check(mode): + need(mode in ("all", "census", "engine"), "mode") + do_census = mode in ("all", "census") + do_engine = mode in ("all", "engine") + authenticate() + lines, puncture, live = pinned_model() + frames = orthogonal_frames(lines, live) + degree = [0] * WIDTH + for frame in frames: + for index in frame: + degree[index] += 1 + need(set(degree) == {DEGREE}, "frame degree") + rows = tuple(sum(1 << index for index in frame) for frame in frames) + basis = kernel(rows) + supports = partition_masks(lines, live) + need(all(in_code(mask, rows) for mask in supports), "partition block leaves a frame") + need(in_code((1 << WIDTH) - 1, rows), "all-ones leaves a frame") + moved = (supports[0] ^ (1 << (supports[0].bit_length() - 1)) + ^ (1 << (supports[1].bit_length() - 1))) + need(moved.bit_count() == WEIGHT_BOUND and moved not in supports, + "moved block collapsed onto the partition") + need(not in_code(moved, rows), "a moved block still meets every frame evenly") + if do_census: + with tempfile.TemporaryDirectory(prefix="p112-frame-") as directory: + work = Path(directory) + binary = compile_scan(work) + scanned = [] + for split in SPLIT_POINTS: + scanned.append(run_split(binary, basis, split, work)) + need(scanned[0] == scanned[1] == set(supports), "half-split changed the set") + produced = None + rejected = None + if do_engine: + engine = run_path( + str(ROOT / "research/e7-bitsliced-exhaustion/binary.py"), + run_name="p112_frame_lane_engine", + )["low_weight_words"] + produced = engine_words(engine, basis, WEIGHT_BOUND, ENGINE_BATCH) + need(produced == set(supports) | {0}, "engine dropped or added a word") + need(0 in produced and positive_words_have_weight(produced, WEIGHT_BOUND), + "engine minimum") + witness = supports[0] + need(produced - {witness} != set(supports) | {0}, + "dropping one support still compared equal") + lighter = witness ^ (1 << (witness.bit_length() - 1)) + need(lighter.bit_count() == WEIGHT_BOUND - 1, + "clearing the top bit did not reduce weight") + need(lighter not in produced and not in_code(lighter, rows), + "a weight-fifteen word was already in the code") + forged = set(produced) + forged.add(lighter) + need(not positive_words_have_weight(forged, WEIGHT_BOUND), + "weight-fifteen injection was accepted") + toy = engine_words(engine, (1, 2, 4), 1, 3) + need(toy == {0, 1, 2, 4}, "toy weight-1 set") + need(engine_words(engine, (1, 2, 4), 0, 3) == {0}, "toy bound change was ignored") + try: + list(engine((basis[0], basis[0]), WIDTH, WEIGHT_BOUND, 4)) + except ValueError: + rejected = True + else: + rejected = False + need(rejected, "a repeated generator was accepted") + digest = sha256(json.dumps(sorted(supports)).encode()).hexdigest() + need(digest == SUPPORT_SHA256, "support hash") + return { + "status": "PASS_P112_PUNCTURED_FRAME_CODE", + "width": WIDTH, + "frames": FRAME_COUNT, + "frame_size": FRAME_SIZE, + "frame_degree": DEGREE, + "rank": RANK, + "dimension": DIMENSION, + "free_coordinates": list(FREE_COORDINATES), + "puncture_indices": list(puncture), + "minimum_positive_weight": WEIGHT_BOUND, + "weight_at_most_16": SUPPORT_COUNT + 1, + "minimum_supports": SUPPORT_COUNT, + "distinct_codewords": CODEWORDS, + "splits": list(SPLIT_POINTS) if do_census else [], + "mode": mode, + "engine_batch": ENGINE_BATCH if do_engine else None, + "supports": sorted(supports), + "supports_sha256": digest, + "lines_sha256": LINE_SHA256, + "dependent_generator_rejected": rejected, + "e6_replayed": False, + "d6_replayed": False, + "intersection_engine_replayed": False, + "timing_remeasured": False, + "no_new_kappa": True, + } + + +if __name__ == "__main__": + selected = sys.argv[1] if len(sys.argv) > 1 else "all" + result = check(selected) + shown = dict(result) + shown["engine_batch"] = ( + "20" if result["engine_batch"] == ENGINE_BATCH else "not-run" + ) + shown["splits"] = ( + "18,16" if result["splits"] == [18, 16] else "not-run" + ) + print( + "PASS_P112_PUNCTURED_FRAME_CODE" + " width={width}" + " frames={frames}" + " dimension={dimension}" + " minimum={minimum_positive_weight}" + " supports={minimum_supports}" + " codewords={distinct_codewords}" + " mode={mode}" + " batches={engine_batch}" + " splits={splits}" + " e6_replayed=false" + " d6_replayed=false" + " no_new_kappa=true".format(**shown) + ) + print(json.dumps(result, indent=2, sort_keys=True))