From f015b04c74801fa330f818d178e809c760fb5469 Mon Sep 17 00:00:00 2001 From: merramil Date: Tue, 13 Oct 2026 01:27:40 -0400 Subject: [PATCH] Speed up exact single-intersection Gram replay with symmetric packing --- certificates/affine-vector-screens.json | 2 +- certificates/single-intersection.json | 2 +- docs/research/single-intersection-packing.md | 97 +++++++++++ .../single-intersection-packing/NOTICE.md | 22 +++ .../single-intersection-packing/RESULT.json | 92 +++++++++++ .../VALIDATION.json | 59 +++++++ .../single-intersection-packing/baseline.py | 153 ++++++++++++++++++ .../single-intersection-packing/benchmark.py | 145 +++++++++++++++++ scripts/experiments/single_intersection.py | 18 ++- tests/test_single_intersection_benchmark.py | 53 ++++++ tests/test_single_intersection_packing.py | 78 +++++++++ 11 files changed, 718 insertions(+), 3 deletions(-) create mode 100644 docs/research/single-intersection-packing.md create mode 100644 research/single-intersection-packing/NOTICE.md create mode 100644 research/single-intersection-packing/RESULT.json create mode 100644 research/single-intersection-packing/VALIDATION.json create mode 100644 research/single-intersection-packing/baseline.py create mode 100644 research/single-intersection-packing/benchmark.py create mode 100644 tests/test_single_intersection_benchmark.py create mode 100644 tests/test_single_intersection_packing.py diff --git a/certificates/affine-vector-screens.json b/certificates/affine-vector-screens.json index 47e598ab3d..7553cd304e 100644 --- a/certificates/affine-vector-screens.json +++ b/certificates/affine-vector-screens.json @@ -146,7 +146,7 @@ "scripts/experiments/affine_vector_screens.py": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", "scripts/experiments/affine_vector_witnesses.json": "672a4318c48f5286ce088d34736c38957b7f662a5f753d440dbc638e7da5f62a", "scripts/experiments/cube_core_family.py": "e58f1f4067bda2d4838343f42ec2505316f006561f0702e869847d88b85413a8", - "scripts/experiments/single_intersection.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d" + "scripts/experiments/single_intersection.py": "6874d41b75590369182ed61e0c6da5b547e035e0e43b50ea2b39e1f3861dca6d" }, "status": "NINE SPECIFIED CENTRAL MATRICES REJECTED; NO NEW KAPPA", "upstream_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a" diff --git a/certificates/single-intersection.json b/certificates/single-intersection.json index bbd43997f7..f5fd6bbf56 100644 --- a/certificates/single-intersection.json +++ b/certificates/single-intersection.json @@ -52854,7 +52854,7 @@ "source_sha256": { "docs/research/single-intersection.md": "c3a9be97b38f4ac1e7983842d9f23656671e877ad5144f41894818f4551aa4dd", "scripts/audit_single_intersection.py": "1de7f9a62edc93c624ff2693ae9bb725cf6dc9735ff1caad56f6913aae9448ee", - "scripts/experiments/single_intersection.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d", + "scripts/experiments/single_intersection.py": "6874d41b75590369182ed61e0c6da5b547e035e0e43b50ea2b39e1f3861dca6d", "scripts/experiments/single_intersection_witnesses.json": "c2308a3d21991f5828b0519b191b470f48b2fbbcaa5af0f7aed3986cc7534185" }, "status": "BOUNDED TWO-FIELD RANK SCREEN; NO COMPETITIVE SIDE CIRCUIT OR NEW KAPPA", diff --git a/docs/research/single-intersection-packing.md b/docs/research/single-intersection-packing.md new file mode 100644 index 0000000000..cb5551bb26 --- /dev/null +++ b/docs/research/single-intersection-packing.md @@ -0,0 +1,97 @@ +# Exact packed Gram replay + +This verification tooling contribution targets `minor_rows` in +`scripts/experiments/single_intersection.py`. It changes neither the historical +single-intersection search domain nor the selected multiplication bound. + +The matrix entry is `C[S,T] = [S == T or popcount(S & T) == j]` over F2. +Distinct labels make every diagonal entry one. The intersection relation is +symmetric, so one exact popcount determines both off-diagonal entries. +Byte buffers store bit `b` at byte `b // 8`, bit `b % 8`; little-endian integer +conversion preserves the packed-row convention consumed by binary elimination. +The final partial byte has zero padding. Every matrix entry is retained. + +The baseline at commit `66849e1475c930fd7732b1a0067ffee7e1e95f60` builds each +row by summing shifted arbitrary-precision integers. Profiling all 5,257 cases +and four committed orbit witnesses took 39.151 seconds, with 30.878 seconds +inside `minor_rows` (profiling overhead included). This motivated switching +from the initial feature-construction hypothesis to matrix packing. No rank, +feature-basis independence, transposition-closure, or input rejection check +is removed. No persistent cache is introduced. + +The contribution is by merramil with substantial OpenAI Codex assistance, +under Apache-2.0. It builds on Douglas R. Colkitt's preserved historical +single-intersection audit (`d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`) and +retains that audit's mathematical scope and attribution. Assignment seed 86 +selected verification engineering; the three candidates were gather schedules, +coded-carry controls, and single-intersection replay (86 modulo 3 selects the +last). The initial open-PR snapshot had 582 entries and no title claiming this +engine. The only open issue was #650, so the scope was claimed locally. + +## Verification contract + +Tests compare complete packed rows with the predecessor's directed formula, +including permutations, negative controls, and byte-boundary sizes. The bounded +benchmark compares every entry of all four committed orbit Gram matrices +and the complete audit output. Only the changed implementation's source hash +may differ from the committed certificate. Existing malformed orbit witnesses +still fail, including with Python optimization enabled. + +The full matrices remain quadratic in space and time. This is an implementation +speedup for finite verification, not a new construction, rank theorem, expanded +search, or proof of the conditional multiplication theorem. + +## Reproduce and measured result + +From the repository root, using standard-library Python 3.11 or newer on +macOS or Linux: + +```sh +python3 -B research/single-intersection-packing/benchmark.py --rounds 3 --output /tmp/single-intersection-packing.json +``` + +Use a fresh output path. Expected final status: +`PASS_IDENTICAL_GRAM_ROWS_AND_COMPLETE_CERTIFICATES`. Timing is descriptive, +not a pass threshold. The benchmark imports the preserved, hash-pinned complete +predecessor module, compares all 100,203,737 Gram entries, then runs three +alternating baseline/packed pairs in fresh, sequential interpreters. Each +worker recomputes the complete 5,257-case certificate, including feature-basis +independence, every adjacent-image closure check, exact Gram ranks, and all +other controls. Its full serialized output must have the original certificate +SHA256 after restoring exactly the implementation-source binding. The matrix +comparison happens outside the timing workers; it does not warm their caches. + +[RESULT.json](../../research/single-intersection-packing/RESULT.json) records +every sample and source pin. On CPython 3.13.1 / macOS arm64, median full-audit +time was **13.766 to 6.597 seconds (2.087x faster)**. This trades memory for +speed: median process peak RSS increased from **49,266,688 to 68,845,568 bytes** +(about 40%). In-place buffer conversion avoids explicitly retaining two full +matrix lists, but Python allocator behavior still raises observed peak RSS. +These timings cover this historical finite audit, not supplier cold replay +or integer multiplication runtime. + +Run the focused tests with: + +```sh +python3 -B -m unittest discover -s tests -p 'test_single_intersection*.py' -v +python3 -B -O -m unittest discover -s tests -p 'test_single_intersection*.py' -v +``` + +The 16 tests include changed-source, changed-rank, changed-screen-row, +changed-other-source-binding, and wrong-matrix-entry rejection controls. +Only two generated certificate bindings change: `single-intersection.json` +and `affine-vector-screens.json`. Tests reconstruct and hash each complete +predecessor certificate after restoring that one binding. No selected-frontier +artifact or `upstream/` source changes. + +The complete `make verify-tests` run passed **557 tests in 86 isolated +interpreters and 20 patch-application checks**. Both affected certificate +producers, selected-record integrity, and `git diff --check` passed. +[VALIDATION.json](../../research/single-intersection-packing/VALIDATION.json) +records the exact commands and scope. The broad `make verify-research` target +would regenerate unrelated certificates, so only its two affected producers +were rerun. Full `make verify`, selected-supplier cold replay, Lean builds, and +remote Linux CI are outside this local validation. + +The final pre-submission overlap refresh covered 594 open PRs through #775; +none claimed this single-intersection packing change. diff --git a/research/single-intersection-packing/NOTICE.md b/research/single-intersection-packing/NOTICE.md new file mode 100644 index 0000000000..fc898fa560 --- /dev/null +++ b/research/single-intersection-packing/NOTICE.md @@ -0,0 +1,22 @@ +# Attribution and scope + +Contributor: merramil, with substantial OpenAI Codex assistance. Apache-2.0. + +`baseline.py` is an exact, unmodified copy of +`scripts/experiments/single_intersection.py` at +`66849e1475c930fd7732b1a0067ffee7e1e95f60`, SHA256 +`08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d`. +It was introduced in Douglas R. Colkitt's historical research preservation +commit `d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`. The benchmark retains it +only as a pinned comparison implementation, under the repository's Apache-2.0 +license. All original construction, rank-screen, and orbit-proof credit remains +with that work and its cited mathematical sources. + +The closest concurrent tooling PRs inspected were #707 (Bareiss determinant +prefixes for selected R420 frames) and #756 (balanced-Fano meet-in-the-middle +replay). Neither supplies code or a dependency here; this contribution packs +the historical single-intersection binary Gram matrix. + +See [the engineering note](../../docs/research/single-intersection-packing.md) +for the equivalence argument and verification scope. No new multiplication +exponent, broader negative result, or full theorem verification is claimed. diff --git a/research/single-intersection-packing/RESULT.json b/research/single-intersection-packing/RESULT.json new file mode 100644 index 0000000000..4706072df9 --- /dev/null +++ b/research/single-intersection-packing/RESULT.json @@ -0,0 +1,92 @@ +{ + "status": "PASS_IDENTICAL_GRAM_ROWS_AND_COMPLETE_CERTIFICATES", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 86, + "python": "3.13.1 (main, Dec 3 2024, 17:59:52) [Clang 16.0.0 (clang-1600.0.26.4)]", + "platform": "macOS-26.5.1-arm64-arm-64bit-Mach-O", + "machine": "arm64", + "source_pins": { + "research/single-intersection-packing/baseline.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d", + "scripts/experiments/single_intersection_witnesses.json": "c2308a3d21991f5828b0519b191b470f48b2fbbcaa5af0f7aed3986cc7534185", + "scripts/audit_single_intersection.py": "1de7f9a62edc93c624ff2693ae9bb725cf6dc9735ff1caad56f6913aae9448ee" + }, + "packed_source_sha256": "6874d41b75590369182ed61e0c6da5b547e035e0e43b50ea2b39e1f3861dca6d", + "row_comparisons": [ + { + "h": 20, + "k": 6, + "j": 2, + "rows": 1140, + "entries_compared": 1299600, + "packed_rows_sha256": "f230204454368c722bb34307e0daf1356126df03208a2531277516b4ad41fb2d" + }, + { + "h": 32, + "k": 6, + "j": 2, + "rows": 4960, + "entries_compared": 24601600, + "packed_rows_sha256": "ee09dd3c8190623f7f0e518a48fc2726ce905fb8eeb24cd0e7bddc692005e0e2" + }, + { + "h": 38, + "k": 6, + "j": 2, + "rows": 8436, + "entries_compared": 71166096, + "packed_rows_sha256": "3a53896a8f14e3384a283e0530865c190e1631d25e2f81f9c9c5ae212d914049" + }, + { + "h": 23, + "k": 7, + "j": 3, + "rows": 1771, + "entries_compared": 3136441, + "packed_rows_sha256": "9b1919d552c6fb54798470ba193a7ebe8a4d4cc2210737667dd77cb495d10957" + } + ], + "samples": [ + { + "engine": "baseline", + "audit_seconds": 14.628344791941345, + "peak_rss_bytes": 49266688, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + }, + { + "engine": "packed", + "audit_seconds": 6.6083968337625265, + "peak_rss_bytes": 66437120, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + }, + { + "engine": "packed", + "audit_seconds": 6.596809957176447, + "peak_rss_bytes": 71843840, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + }, + { + "engine": "baseline", + "audit_seconds": 13.502197874709964, + "peak_rss_bytes": 48578560, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + }, + { + "engine": "baseline", + "audit_seconds": 13.766040291637182, + "peak_rss_bytes": 51019776, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + }, + { + "engine": "packed", + "audit_seconds": 6.383586917072535, + "peak_rss_bytes": 68845568, + "certificate_sha256_with_original_source_binding": "59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8" + } + ], + "median_audit_seconds": { + "baseline": 13.766040291637182, + "packed": 6.596809957176447 + }, + "speedup": 2.0867723007029437, + "scope": "Four committed orbit witnesses and 5,257 historical cases; no new kappa." +} diff --git a/research/single-intersection-packing/VALIDATION.json b/research/single-intersection-packing/VALIDATION.json new file mode 100644 index 0000000000..106dc4a2f4 --- /dev/null +++ b/research/single-intersection-packing/VALIDATION.json @@ -0,0 +1,59 @@ +{ + "status": "PASS_SCOPED_VERIFICATION", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 86, + "checks": [ + { + "command": "PYTHONDONTWRITEBYTECODE=1 make verify-tests", + "exit_code": 0, + "tests": 557, + "isolated_modules": 86, + "patch_checks": 20, + "log_sha256": "77c358c471a9a051ab3af9c228320ecaf19574c1ee90e784803e1baaac028ba2" + }, + { + "command": "python3 -B -m unittest discover -s tests -p 'test_single_intersection*.py' -v", + "exit_code": 0, + "tests": 16 + }, + { + "command": "python3 -B -O -m unittest discover -s tests -p 'test_single_intersection*.py' -v", + "exit_code": 0, + "tests": 16 + }, + { + "command": "python3 -B scripts/audit_single_intersection.py", + "exit_code": 0, + "cases": 5257 + }, + { + "command": "python3 -B scripts/audit_affine_vectors.py", + "exit_code": 0, + "cases": 9 + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "exit_code": 0 + }, + { + "command": "python3 -B research/single-intersection-packing/benchmark.py --rounds 3 --output research/single-intersection-packing/RESULT.json", + "exit_code": 0, + "receipt": "RESULT.json", + "entries_compared": 100203737, + "fresh_process_samples": 6 + }, + { + "command": "git diff --check", + "exit_code": 0 + } + ], + "regenerated_certificates": "Only the single_intersection.py source binding changes in single-intersection.json and affine-vector-screens.json. Tests hash the complete predecessor certificate after restoring that binding.", + "not_run": [ + "Full make verify", + "Whole make verify-research target (would regenerate unrelated certificates)", + "Selected supplier cold replay", + "Lean builds", + "Remote Linux CI" + ], + "scope": "Historical finite verification tooling; no new kappa, mathematical search, or full theorem verification." +} diff --git a/research/single-intersection-packing/baseline.py b/research/single-intersection-packing/baseline.py new file mode 100644 index 0000000000..c14fdaff14 --- /dev/null +++ b/research/single-intersection-packing/baseline.py @@ -0,0 +1,153 @@ +"""Single-intersection two-field cores and exact binary minor witnesses.""" +from fractions import Fraction as Q +from math import comb +from itertools import combinations + +from certify import require +from search_network import log_integer_bounds + + +def core_parameters(h,k,j): + require(all(type(x) is int for x in (h,k,j)) and 2<=k=j else 0)+int(l==k))%2 for l in range(k+1)] + for t in range(k+1): + require(sum(a*comb(t,l) for l,a in enumerate(coefficients) if l<=t)%2 == int(t==j or t==k), + 'Binomial coefficient expansion failed') + levels=[l for l,a in enumerate(coefficients) if a] + retained=[l for l in levels if not any(t>l and comb(k-l,t-l)%2 for t in levels)] + cover={l:next(t for t in retained if t>=l and comb(k-l,t-l)%2) for l in levels} + upper=sum(comb(h,l) for l in retained) + degree=comb(k,j)*comb(h-k,k-j) if h-k>=k-j else 0 + return dict(h=h,k=k,j=j,n=n,d=d,binomial_coefficients=coefficients, + retained_levels=retained,level_cover=cover, + binary_factor_upper=upper,degree=degree, + positive_with_supplied_factor=n>6*upper*d, + positivity_exclusion_rank=(n+6*d-1)//(6*d)) + + +def rank_of_rows(rows): + basis={} + for row in rows: + require(type(row) is int and row>=0,'Invalid packed binary row') + while row: + pivot=row.bit_length()-1 + if pivot not in basis: + basis[pivot]=row;break + row^=basis[pivot] + return len(basis) + + +def minor_rows(labels,j): + require(len(labels)==len(set(labels)) and all(type(x) is int and x>0 for x in labels), + 'Distinct positive packed labels required') + return [sum(1<=parameters['n']) + + +def free_side_bounds(h,k,j,r): + p=core_parameters(h,k,j);n=p['n'];d=p['d'];m=d**3 + require(type(r) is int and 1<=r<=n,'Use a nonzero rank bound at most n') + f=1-Q(6*r*d,n) + if f<=0:return None + eta=f/(m*(2+Q(3*r,n))) + lo,hi=log_integer_bounds(m) + return dict(relative_deficit=eta,lower=eta/hi,upper=eta/((1-eta)*lo)) + + +def spectral_parity_bound(h,k,j): + """Integer Johnson spectrum gives a binary rank lower bound. + + The common rational eigenspaces need not remain eigenspaces over F2. + Only the integer characteristic polynomial is reduced modulo two. + """ + p=core_parameters(h,k,j) + require(2*k<=h,'Spectral formula here uses k<=h/2') + b=[(((-1)**(l-j)*comb(l,j)) if l>=j else 0)+int(l==k) for l in range(k+1)] + eigenvalues=[sum(b[l]*comb(k-i,l-i)*comb(h-l-i,k-l) for l in range(i,k+1)) + for i in range(k+1)] + multiplicities=[comb(h,i)-(comb(h,i-1) if i else 0) for i in range(k+1)] + require(sum(multiplicities)==p['n'],'Wrong total spectral multiplicity') + require(sum(m*e for m,e in zip(multiplicities,eigenvalues))==p['n'],'Wrong spectral trace') + require(sum(m*e*e for m,e in zip(multiplicities,eigenvalues))==p['n']*(1+p['degree']), + 'Wrong spectral squared trace') + lower=sum(m for m,e in zip(multiplicities,eigenvalues) if e%2) + return dict(eigenvalues=eigenvalues,multiplicities=multiplicities, + binary_rank_lower=lower,positive_deficit_excluded=6*lower*p['d']>=p['n']) + + +def intersecting_minor_bound(h,k,j): + """Identity minor on all labels containing one fixed (j+1)-subset.""" + p=core_parameters(h,k,j) + candidates={'fixed_common_subset':comb(h-j-1,k-j-1)} + block=2*k-j-1 + if j>0 and block<=h: + candidates['disjoint_blocks']=h//block*comb(block,k) + if j==k-1: + # Adjacent labels differ in one ground point, so their point sums + # differ nontrivially modulo h. A largest color class is independent. + candidates['sum_mod_h_color_class']=(p['n']+h-1)//h + lower=max(candidates.values()) + return dict(binary_rank_lower=lower,positive_deficit_excluded=6*lower*p['d']>=p['n'], + fixed_common_subset_size=j+1,identity_minor_lower_bounds=candidates) + + +def verify_feature_orbit(h,k,j,labels,feature_budget=40000): + """Certify the feature row span by adjacent-transposition closure. + + Every supplied label is an actual k-subset. Independent feature rows + whose span is invariant under all adjacent ground permutations span + the entire transitive orbit. The full C rank then equals their Gram rank. + """ + p=core_parameters(h,k,j) + require(labels and len(labels)==len(set(labels)),'Distinct nonempty orbit basis required') + require(all(type(S) is int and 0<=S<1<>i&1] + return sum(1<>i)^(S>>(i+1)))&1: + image=S^(3<6*r*p['d']) diff --git a/research/single-intersection-packing/benchmark.py b/research/single-intersection-packing/benchmark.py new file mode 100644 index 0000000000..e97f073bc7 --- /dev/null +++ b/research/single-intersection-packing/benchmark.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Compare every Gram entry and time complete audits in fresh interpreters.""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import platform +import resource +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT / 'scripts')) +BASE = '66849e1475c930fd7732b1a0067ffee7e1e95f60' +PINS = { + 'research/single-intersection-packing/baseline.py': + '08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d', + 'scripts/experiments/single_intersection_witnesses.json': + 'c2308a3d21991f5828b0519b191b470f48b2fbbcaa5af0f7aed3986cc7534185', + 'scripts/audit_single_intersection.py': + '1de7f9a62edc93c624ff2693ae9bb725cf6dc9735ff1caad56f6913aae9448ee', +} +SOURCE = 'scripts/experiments/single_intersection.py' +CERTIFICATE_SHA256 = '59bca430c5cda9050b346f0f89ff980c9e610a30786cd19677911a1eb433d5b8' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def load_baseline(): + for name, expected in PINS.items(): + require(digest((ROOT / name).read_bytes()) == expected, + 'Pinned source changed: ' + name) + spec = importlib.util.spec_from_file_location('orbit_baseline', HERE / 'baseline.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def sample(engine): + # Import before timing, identically in both fresh worker processes. + baseline = load_baseline() + import audit_single_intersection as audit + from prepare_layers import serializable + if engine == 'baseline': + audit.verify_feature_orbit = baseline.verify_feature_orbit + started = time.perf_counter() + result = serializable(audit.certificate()) + elapsed = time.perf_counter() - started + # Permit exactly the implementation-source binding to differ. Everything + # else, including all other source bindings and all 5,257 rows, is hashed. + require(result['source_sha256'][SOURCE] == digest((ROOT / SOURCE).read_bytes()), + 'Current implementation is not bound to the certificate') + result['source_sha256'][SOURCE] = PINS['research/single-intersection-packing/baseline.py'] + normalized = (json.dumps(result, indent=2, sort_keys=True) + '\n').encode() + require(digest(normalized) == CERTIFICATE_SHA256, + 'Full predecessor certificate changed beyond the implementation binding') + return { + 'engine': engine, + 'audit_seconds': elapsed, + 'peak_rss_bytes': resource.getrusage(resource.RUSAGE_SELF).ru_maxrss + * (1 if sys.platform == 'darwin' else 1024), + 'certificate_sha256_with_original_source_binding': digest(normalized), + } + + +def compare_rows(): + baseline = load_baseline() + from experiments.single_intersection import minor_rows + fixtures = json.loads((ROOT / 'scripts/experiments/single_intersection_witnesses.json').read_text()) + comparisons = [] + for fixture in fixtures['feature_orbits']: + labels, j = fixture['labels'], fixture['j'] + expected = baseline.minor_rows(labels, j) + actual = minor_rows(labels, j) + require(actual == expected, 'Complete packed Gram matrix differs') + width = (len(labels) + 7) // 8 + sha = hashlib.sha256() + for row in actual: + sha.update(row.to_bytes(width, 'little')) + comparisons.append({ + 'h': fixture['h'], 'k': fixture['k'], 'j': j, + 'rows': len(labels), 'entries_compared': len(labels) ** 2, + 'packed_rows_sha256': sha.hexdigest(), + }) + return comparisons + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--rounds', type=int, default=3) + parser.add_argument('--output', type=Path) + parser.add_argument('--worker', choices=('baseline', 'packed'), help=argparse.SUPPRESS) + args = parser.parse_args() + if args.rounds < 1: + parser.error('--rounds must be positive') + if args.worker: + print(json.dumps(sample(args.worker))) + return + if args.output and args.output.exists(): + parser.error('--output must be a fresh path') + rows = compare_rows() + samples = [] + for turn in range(args.rounds): + order = ('baseline', 'packed') if turn % 2 == 0 else ('packed', 'baseline') + for engine in order: + command = [sys.executable, '-B'] + if sys.flags.optimize: + command.append('-O') + command += [str(Path(__file__).resolve()), '--worker', engine] + run = subprocess.run(command, cwd=ROOT, text=True, capture_output=True, check=True) + result = json.loads(run.stdout) + samples.append(result) + print(engine, f"{result['audit_seconds']:.3f}s", flush=True) + medians = { + engine: statistics.median(s['audit_seconds'] for s in samples if s['engine'] == engine) + for engine in ('baseline', 'packed') + } + report = { + 'status': 'PASS_IDENTICAL_GRAM_ROWS_AND_COMPLETE_CERTIFICATES', + 'base_commit': BASE, 'assignment_seed': 86, + 'python': sys.version, 'platform': platform.platform(), 'machine': platform.machine(), + 'source_pins': PINS, 'packed_source_sha256': digest((ROOT / SOURCE).read_bytes()), + 'row_comparisons': rows, 'samples': samples, 'median_audit_seconds': medians, + 'speedup': medians['baseline'] / medians['packed'], + 'scope': 'Four committed orbit witnesses and 5,257 historical cases; no new kappa.', + } + if args.output: + with args.output.open('x') as stream: + stream.write(json.dumps(report, indent=2) + '\n') + print(report['status'], f"speedup={report['speedup']:.3f}x") + + +if __name__ == '__main__': + main() diff --git a/scripts/experiments/single_intersection.py b/scripts/experiments/single_intersection.py index c14fdaff14..8ebbf6fb76 100644 --- a/scripts/experiments/single_intersection.py +++ b/scripts/experiments/single_intersection.py @@ -40,9 +40,25 @@ def rank_of_rows(rows): def minor_rows(labels,j): + """Pack the full symmetric binary matrix without repeated big-int sums.""" require(len(labels)==len(set(labels)) and all(type(x) is int and x>0 for x in labels), 'Distinct positive packed labels required') - return [sum(1<> n == 0 for row in rows)) + + def test_invalid_labels_are_rejected(self): + for labels in ([1, 1], [0], [-1], [True], [1.0], [1, 2, 1]): + with self.subTest(labels=labels), self.assertRaises(ValueError): + minor_rows(labels, 0) + + def test_nonclosed_and_dependent_orbit_witnesses_are_rejected(self): + with self.assertRaisesRegex(ValueError, 'not permutation invariant'): + verify_feature_orbit(4, 2, 1, [3]) + # These four triples sum to zero in the point-incidence features. + with self.assertRaisesRegex(ValueError, 'Feature basis is dependent'): + verify_feature_orbit(5, 3, 1, [7, 11, 21, 25]) + + +if __name__ == '__main__': + unittest.main()