From 56133ae69c9c2191d7f4964039511f4a2148ff9c Mon Sep 17 00:00:00 2001 From: eumemic Date: Thu, 8 Oct 2026 23:20:15 -0700 Subject: [PATCH 1/3] Stop pinning Makefile, README.md and NOTICE in the joint-dual freeze The joint-dual source manifest pinned the sha256 of the repository-wide Makefile, README.md and NOTICE. They are not inputs to the joint-dual computation, but nearly every contribution edits them, so `make verify-joint` failed with "AssertionError: Makefile" (or README.md) until the contributor re-pinned research/joint-dual/SOURCE.json and regenerated joint-dual-kappa.json and joint-dual-validation.json. These three files then conflicted on every rebase. Drop the three files from the pinned closure and re-pin. All other 48 pins, the kappa and the 47 strict constraints are unchanged; only the manifest digests in the two certificates change. Co-Authored-By: Claude Opus 5.5 (1M context) --- certificates/joint-dual-kappa.json | 6 +++--- certificates/joint-dual-validation.json | 2 +- research/joint-dual/SOURCE.json | 7 ++----- scripts/experiments/joint_dual_compose.py | 2 +- scripts/experiments/pin_joint_dual_sources.py | 4 +++- 5 files changed, 10 insertions(+), 11 deletions(-) diff --git a/certificates/joint-dual-kappa.json b/certificates/joint-dual-kappa.json index 13d841a8c8..dd5360ad77 100644 --- a/certificates/joint-dual-kappa.json +++ b/certificates/joint-dual-kappa.json @@ -837,12 +837,12 @@ "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669", "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc", "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13", - "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800", + "scripts/experiments/joint_dual_compose.py": "3554e957570e2d3f65c5bd7c945338c9e2fc5f3e79efa2b436a4dfc61899c394", "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", - "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", + "scripts/experiments/pin_joint_dual_sources.py": "2d1a77f81bb406866cee5fca7ce440d80bbc4ff802d360a1bebfc83d2430c1fc", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985" }, - "source_manifest_sha256": "3d8a3907630068fb76c0ed3a3e8d33245265471d1770d262b489876a65493155", + "source_manifest_sha256": "5f2c946d867abfdb6f76b1a1d3cfd95dd39146234e2ce2313649704daa5b2353", "sources": [ { "files": { diff --git a/certificates/joint-dual-validation.json b/certificates/joint-dual-validation.json index 968441593d..006b8d5c95 100644 --- a/certificates/joint-dual-validation.json +++ b/certificates/joint-dual-validation.json @@ -226,7 +226,7 @@ } }, "bit_saving": "2382370177/50000000000000", - "certificate_sha256": "16f18ad60af972ce1f9fbbbb1277a69ad838727d542889bbac6c5539d5420bf7", + "certificate_sha256": "1958458d3a288a679abc8648a4b5cf2d6deadc230319dc9a90c85fd0957f7f59", "kappa": "4764513337/100000000000000", "margins": 7, "producer_words_regenerated_and_matched": true, diff --git a/research/joint-dual/SOURCE.json b/research/joint-dual/SOURCE.json index 866dced3ac..61b0d7c5a3 100644 --- a/research/joint-dual/SOURCE.json +++ b/research/joint-dual/SOURCE.json @@ -3,9 +3,6 @@ "base_pr57_commit": "cd350f76c9bc01489ec83568bded532cb69be938", "base_pr58_commit": "bc2f7ed4c20dc18898305ab17165c0c995cbb804", "files": { - "Makefile": "24d73953fd7f6bcee49273119fa6e3bf2e4bcd7fd1b24636f5408f18d67f81f6", - "NOTICE": "f8511476690f8554d2ee37304b34dc7f58e385e4bff77555d5bd895bcda6212e", - "README.md": "82a51095522b8e69c7fe6af79a12ae907a1cb5e0ee3428bf2af2a188dd6cc4db", "certificates/joint-dual-compiler.json": "516c4d85158553dabd0a98216a064b2a7397957a9d5dd0df1d6e5aec53a4e805", "certificates/joint-dual-profiles-23.json": "159fa8fee175fc1d24f63e72d3c2f1dc9f4fcd78b938c5e7d2f735fd0fd37209", "certificates/joint-dual-profiles-25.json": "8d190ce42d097e828c5756918c52f2963df576cf4c6600b0fc7f2b7fdb6ad223", @@ -49,9 +46,9 @@ "scripts/experiments/binary_frame_profiles.cpp": "8e2e391d3ee57cbb1372c68e4aa031e1b861321536eabd642ada54e12e678669", "scripts/experiments/binary_frame_replay.py": "392e78e62d7685c99a5888a7da743ea6c3dcad631af4a743c91e0c09348442bc", "scripts/experiments/joint_dual_compiler.py": "853d3fc4a740c5b74c23b3a6af5d4dc9b41fb38e9b55678539a7e0ee71947c13", - "scripts/experiments/joint_dual_compose.py": "741900aa6f69c0e3458700f3b534334269004ad80c50405ecfeda18e6d3f2800", + "scripts/experiments/joint_dual_compose.py": "3554e957570e2d3f65c5bd7c945338c9e2fc5f3e79efa2b436a4dfc61899c394", "scripts/experiments/joint_dual_reclaim_compiler.py": "9984aaccf880e4840402322d76678bfddb33ce7e494af78430a43429f51b85fd", - "scripts/experiments/pin_joint_dual_sources.py": "4d31cc0e38b7902709ca5f8f714cba109760d2592346dd7f8dc0b900a2d9fe00", + "scripts/experiments/pin_joint_dual_sources.py": "2d1a77f81bb406866cee5fca7ce440d80bbc4ff802d360a1bebfc83d2430c1fc", "scripts/experiments/verify_joint_dual.py": "7a31bba1e9c0ded32ae285df2ca9bc91ef20c330f6789fdba361876f3c7a1985", "tests/test_joint_reclaim.py": "e2cfc99a52283c4912f970f83c7da5481ba9840d5f999f7e0e5468e8e8862a41" }, diff --git a/scripts/experiments/joint_dual_compose.py b/scripts/experiments/joint_dual_compose.py index 1db1f1f606..ae8fdf1248 100644 --- a/scripts/experiments/joint_dual_compose.py +++ b/scripts/experiments/joint_dual_compose.py @@ -60,7 +60,7 @@ def check_sources(): required.update(f'certificates/joint-dual-{kind}-{h}.{extension}' for h in (23,25) for kind, extension in (('word','json.gz'),('profiles','json'),('transitions','json'))) required.update(('certificates/joint-dual-compiler.json', 'certificates/skip-frame-kappa.json', - 'scripts/experiments/pin_joint_dual_sources.py', 'Makefile', 'README.md', 'NOTICE')) + 'scripts/experiments/pin_joint_dual_sources.py')) comparison = ROOT/'references/frame-compiler/pr58' required.add('references/frame-compiler/pr58/SOURCE.json') required.update('references/frame-compiler/pr58/'+name diff --git a/scripts/experiments/pin_joint_dual_sources.py b/scripts/experiments/pin_joint_dual_sources.py index 94ec6bd77b..1538f2fc15 100644 --- a/scripts/experiments/pin_joint_dual_sources.py +++ b/scripts/experiments/pin_joint_dual_sources.py @@ -12,7 +12,9 @@ def run(): names = {'scripts/experiments/'+name for name in NAMES} - names.update(('Makefile', 'README.md', 'NOTICE', 'research/joint-dual/README.md', + # Repository-wide Makefile, README.md and NOTICE are not inputs; pinning them + # broke this check whenever any contribution edited them. + names.update(('research/joint-dual/README.md', 'research/joint-dual/PROOF.md', 'certificates/joint-dual-compiler.json', 'certificates/skip-frame-kappa.json', 'tests/test_joint_reclaim.py')) for h in (23,25): From d67773363075cc787b6f6ffa07191475c7c3fbec Mon Sep 17 00:00:00 2001 From: eumemic Date: Thu, 8 Oct 2026 23:20:15 -0700 Subject: [PATCH 2/3] Run independent checks concurrently and add make verify-parallel - verify-research: the 28 historical audits each write only their own certificate, so scripts/run_parallel.py runs them concurrently, slowest first (JOBS limits the processes; JOBS=1 runs them in order). - verify-tests: run_isolated_tests.py keeps one interpreter per test module and runs the modules concurrently; they write only temporary files. - make verify-parallel: runs every `make verify` group concurrently, each in a fresh git snapshot of the working tree (as CI does), and fails if a group changes a committed file. - formal-historical-verify: the Python circuit check runs alongside the Lean build. - CI: a new push to a pull request cancels the run for its previous commit. Co-Authored-By: Claude Opus 5.5 (1M context) --- .github/workflows/verify.yml | 5 ++ CONTRIBUTING.md | 9 ++- Makefile | 48 +++++------- scripts/run_isolated_tests.py | 16 ++-- scripts/run_parallel.py | 64 +++++++++++++++ scripts/verify_parallel.py | 143 ++++++++++++++++++++++++++++++++++ 6 files changed, 246 insertions(+), 39 deletions(-) create mode 100644 scripts/run_parallel.py create mode 100644 scripts/verify_parallel.py diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 6b1b33f5a5..6dc8e7c0d0 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -8,6 +8,11 @@ on: permissions: contents: read +# A new push to a pull request cancels the run for its previous commit. +concurrency: + group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && github.event.pull_request.number || github.run_id }} + cancel-in-progress: true + jobs: verify: runs-on: ubuntu-24.04 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8ec9f289e9..9ebd1fc531 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -19,9 +19,16 @@ change stays within the parameter ceiling or changes one of its hypotheses. Keep `upstream/` unchanged. Edit the generators under `scripts/`, then run: ```sh -make verify +make verify-parallel ``` +This runs the groups of `make verify` concurrently, each in a fresh snapshot of +your working tree as CI does, and fails if a group changes a committed file. +Logs go to `build/verify-parallel/`. It starts one group per CPU and per 2 GiB +of memory (all groups at once peak near 13 GB); to change that, run +`python3 scripts/verify_parallel.py -j N`. `make verify` runs the same groups +one after another in place. + Include regenerated certificates and patches in the same change. Run the selected incremental target, `make paired-cube-verify`, as well as the checks affected by your changes. The current proof is supplied as LaTeX source; diff --git a/Makefile b/Makefile index 6656308b6b..540bcf1452 100644 --- a/Makefile +++ b/Makefile @@ -9,9 +9,13 @@ community-audit-check: community-followup-check: python3 scripts/audit_followup_candidate.py --candidate-root . --check docs/research/community-followup-arithmetic.json -.PHONY: verify-community verify-producers verify-certificates verify-ternary verify-tests +.PHONY: verify-community verify-producers verify-certificates verify-ternary verify-tests verify-parallel # CI runs these in separate checkouts. Keep local verification sequential: # different groups regenerate certificates that another group may read. +# verify-parallel runs the groups concurrently, each in its own snapshot. +verify-parallel: + MAKE="$(MAKE)" python3 scripts/verify_parallel.py + verify: $(MAKE) verify-community $(MAKE) verify-producers @@ -291,13 +295,20 @@ climbed-48-verify: climbed-48-producer climbed-48-check .PHONY: formal-verify formal-historical-verify formal-gaussian-verify formal-verify: formal-historical-verify formal-gaussian-verify +.PHONY: formal-historical-lean formal-historical-circuit +# The Python circuit check is independent of Lean, so it runs alongside the build. formal-historical-verify: + $(MAKE) -j2 formal-historical-lean formal-historical-circuit + +formal-historical-lean: cd formal/lean && lake build python3 scripts/check_lean_axioms.py --project formal/lean --audit formal/lean/AuditAll.lean python3 formal/lean/sources.py python3 formal/open-prs/drift_A.py python3 formal/open-prs/drift_B.py --selftest python3 formal/open-prs/drift_C.py + +formal-historical-circuit: mkdir -p build/formal python3 formal/circuit/export_paired.py build/formal/paired50.json python3 -I formal/circuit/check_paired.py build/formal/paired50.json @@ -308,35 +319,14 @@ formal-gaussian-verify: .PHONY: verify-research # Historical finite searches; no current witness or production certificates change. +# Each audit writes only its own certificate, so they run concurrently, slowest first. +RESEARCH_AUDITS := quadratic_affine positive_side mixed_point parity_side bit_compression \ + early_sharing stage_pair inplace_side single_intersection affine_vectors complex_centers \ + stronger_screens disjoint_tensor block_core shared_core split_centers cyclic_topology \ + joint_return block_carry rank_product_core subset_cores fano_permutation signed_sparse \ + prime_subset_limits fano_completion core_limits cube_cores general_guard verify-research: - python3 scripts/audit_bit_compression.py - python3 scripts/audit_mixed_point.py - python3 scripts/audit_early_sharing.py - python3 scripts/audit_split_centers.py - python3 scripts/audit_stage_pair.py - python3 scripts/audit_block_carry.py - python3 scripts/audit_joint_return.py - python3 scripts/audit_cyclic_topology.py - python3 scripts/audit_fano_completion.py - python3 scripts/audit_fano_permutation.py - python3 scripts/audit_rank_product_core.py - python3 scripts/audit_stronger_screens.py - python3 scripts/audit_subset_cores.py - python3 scripts/audit_cube_cores.py - python3 scripts/audit_single_intersection.py - python3 scripts/audit_shared_core.py - python3 scripts/audit_general_guard.py - python3 scripts/audit_disjoint_tensor.py - python3 scripts/audit_core_limits.py - python3 scripts/audit_affine_vectors.py - python3 scripts/audit_block_core.py - python3 scripts/audit_complex_centers.py - python3 scripts/audit_inplace_side.py - python3 scripts/audit_quadratic_affine.py - python3 scripts/audit_signed_sparse.py - python3 scripts/audit_positive_side.py - python3 scripts/audit_parity_side.py - python3 scripts/audit_prime_subset_limits.py + python3 scripts/run_parallel.py $(RESEARCH_AUDITS:%=scripts/audit_%.py) .PHONY: skip-frame-verify skip-frame-verify: python3 scripts/experiments/verify_skip_frame.py diff --git a/scripts/run_isolated_tests.py b/scripts/run_isolated_tests.py index bb4ecc7cd3..1ff900aa09 100644 --- a/scripts/run_isolated_tests.py +++ b/scripts/run_isolated_tests.py @@ -4,22 +4,20 @@ Independent contributed research packages reuse names such as verify, skip_graph and data_recovery. A shared unittest process can silently bind a later package to an earlier package's module. Preserve full test discovery -within each file, but do not share those imports between files. +within each file, but do not share those imports between files. Modules run +concurrently (JOBS; see run_parallel.py); each writes only temporary files. """ from pathlib import Path -import subprocess import sys +from run_parallel import run_all + ROOT = Path(__file__).resolve().parents[1] files = sorted((ROOT/'tests').glob('test*.py')) if not files: raise RuntimeError('No test modules discovered') -failed = [] -for path in files: - print('Checking '+path.name, flush=True) - result = subprocess.run([sys.executable, '-m', 'unittest', 'discover', '-s', str(ROOT/'tests'), '-p', path.name, '-v'], cwd=ROOT) - if result.returncode: - failed.append(path.name) +failed = run_all([(path.name, [sys.executable, '-m', 'unittest', 'discover', '-s', str(ROOT/'tests'), + '-p', path.name, '-v']) for path in files], cwd=ROOT) if failed: - raise SystemExit('Failed modules: '+', '.join(failed)) + raise SystemExit('Failed modules: '+', '.join(sorted(failed))) print(f'PASS all {len(files)} test modules in isolated interpreters') diff --git a/scripts/run_parallel.py b/scripts/run_parallel.py new file mode 100644 index 0000000000..ecbafe5aa3 --- /dev/null +++ b/scripts/run_parallel.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +"""Run independent Python scripts concurrently, one fresh interpreter each. + +Each script's combined output is printed as one block when it finishes, so +concurrent logs stay readable. Only list scripts that do not read a file that +another listed script writes. JOBS limits the number of concurrent processes +(default: one per CPU and per 3 GiB of memory); JOBS=1 runs them in order. +""" +from concurrent.futures import ThreadPoolExecutor, as_completed +import os +import subprocess +import sys +import time + + +def available_cpus(): + if hasattr(os, 'sched_getaffinity'): + return len(os.sched_getaffinity(0)) + return os.cpu_count() or 1 + + +def memory_gib(): + """Physical memory in GiB, or None where the platform does not report it.""" + try: + return os.sysconf('SC_PAGE_SIZE')*os.sysconf('SC_PHYS_PAGES')/2**30 + except (AttributeError, ValueError, OSError): + return None + + +def jobs(): + """JOBS if set, else one process per CPU and per 3 GiB (the largest audits use 3 GiB).""" + if os.environ.get('JOBS'): + return max(1, int(os.environ['JOBS'])) + memory = memory_gib() + return max(1, min(available_cpus(), int(memory//3) if memory else available_cpus())) + + +def run_all(commands, cwd=None): + """Run (label, argv) pairs concurrently and return the failed labels.""" + def run(label, argv): + start = time.monotonic() + result = subprocess.run(argv, cwd=cwd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, + text=True, errors='replace') + return label, result.returncode, result.stdout, time.monotonic()-start + failed = [] + with ThreadPoolExecutor(max_workers=jobs()) as pool: + futures = [pool.submit(run, label, argv) for label, argv in commands] + for future in as_completed(futures): + label, code, output, seconds = future.result() + print(f'{"FAIL" if code else "Checked"} {label} ({seconds:.1f}s)', flush=True) + print(output, end='' if output.endswith('\n') else '\n', flush=True) + if code: + failed.append(label) + return failed + + +if __name__ == '__main__': + scripts = sys.argv[1:] + if not scripts: + raise SystemExit('usage: run_parallel.py SCRIPT.py [SCRIPT.py ...]') + failed = run_all([(script, [sys.executable, script]) for script in scripts]) + if failed: + raise SystemExit('Failed: '+', '.join(failed)) + print(f'PASS all {len(scripts)} scripts') diff --git a/scripts/verify_parallel.py b/scripts/verify_parallel.py new file mode 100644 index 0000000000..e15caa4f83 --- /dev/null +++ b/scripts/verify_parallel.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Run the `make verify` groups concurrently, each in its own snapshot. + +Some groups regenerate certificates that other groups read, so the groups +cannot share a working tree. As in CI, each group runs in a separate copy: +a one-commit git snapshot of the current working tree (tracked files with +uncommitted edits, plus untracked files that are not ignored). A group passes +when `make verify-` succeeds and leaves its snapshot unchanged, the +check CI makes with `git diff --exit-code`. Logs go to build/verify-parallel/. +""" +import argparse +import json +import os +from pathlib import Path +import re +import shutil +import signal +import subprocess +import tempfile +import time + +from run_parallel import available_cpus, memory_gib + +ROOT = Path(__file__).resolve().parents[1] +LOGS = ROOT/'build'/'verify-parallel' +GIT = ['git', '-c', 'core.autocrlf=false', '-c', 'commit.gpgsign=false', + '-c', 'user.name=verify-parallel', '-c', 'user.email=verify-parallel@localhost'] + + +def makefile_groups(): + """The groups that `make verify` runs, in order.""" + rule = re.search(r'^verify:\n((?:\t.*\n)+)', (ROOT/'Makefile').read_text(), re.M) + return re.findall(r'\$\(MAKE\) verify-(\S+)', rule.group(1)) + + +def git(*args, cwd): + return subprocess.run([*GIT, *args], cwd=cwd, check=True, capture_output=True, text=True).stdout + + +def snapshot(template): + """Copy every non-ignored working-tree file into a new one-commit repository.""" + names = git('ls-files', '-z', '--cached', '--others', '--exclude-standard', cwd=ROOT).split('\0') + for name in filter(None, names): + source = ROOT/name + if source.is_file() or source.is_symlink(): + (template/name).parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(source, template/name, follow_symlinks=False) + git('init', '-q', cwd=template) + git('add', '-A', cwd=template) + git('commit', '-q', '--no-verify', '-m', 'verify-parallel snapshot', cwd=template) + if git('status', '--porcelain', cwd=template): + raise SystemExit('The snapshot is not clean; check line-ending attributes') + return len(names) + + +def default_jobs(): + """One group per CPU and per 2 GiB of memory; all 14 groups at once peak near 13 GB.""" + memory = memory_gib() + return max(1, min(available_cpus(), int(memory//2) if memory else available_cpus())) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument('groups', nargs='*', help='groups to run (default: every group of `make verify`)') + parser.add_argument('-j', '--jobs', type=int, default=default_jobs(), + help='groups to run at once (default: %(default)s, from CPUs and memory)') + parser.add_argument('--keep', action='store_true', help='keep every snapshot, not only failed ones') + args = parser.parse_args() + groups = args.groups or makefile_groups() + LOGS.mkdir(parents=True, exist_ok=True) + durations_path = LOGS/'durations.json' + durations = json.loads(durations_path.read_text()) if durations_path.exists() else {} + # Longest first, using the previous run's times. + queue = sorted(groups, key=lambda g: -durations.get(g, 0)) + env = {k: v for k, v in os.environ.items() if k not in ('MAKEFLAGS', 'MFLAGS', 'MAKELEVEL')} + # Groups that run their own scripts concurrently use four processes, as on a + # CI runner; all of them at once would add about 10 GB of peak memory. + env.setdefault('JOBS', '4') + make = os.environ.get('MAKE', 'make') + work = Path(tempfile.mkdtemp(prefix='verify-parallel-')) + start = time.monotonic() + running, results, kept = {}, {}, [] + try: + count = snapshot(work/'template') + print(f'Snapshot of {count} files; running {len(groups)} groups, {args.jobs} at a time; ' + 'logs in build/verify-parallel/', flush=True) + while queue or running: + while queue and len(running) < args.jobs: + group = queue.pop(0) + tree = work/group + git('clone', '-q', str(work/'template'), str(tree), cwd=work) + log = open(LOGS/f'{group}.log', 'w') + process = subprocess.Popen([make, f'verify-{group}'], cwd=tree, env=env, stdout=log, + stderr=subprocess.STDOUT, start_new_session=True) + running[group] = (process, log, time.monotonic()) + time.sleep(0.5) + for group, (process, log, began) in list(running.items()): + if process.poll() is None: + continue + del running[group] + tree = work/group + changed = git('status', '--porcelain', '--untracked-files=no', cwd=tree) if not process.returncode else '' + if changed: + log.write('\nRegenerated files differ from the snapshot:\n'+changed) + log.close() + seconds = time.monotonic()-began + ok = not process.returncode and not changed + results[group] = (ok, seconds) + durations[group] = round(seconds) + status = 'PASS' if ok else ('FAIL (files changed)' if changed else 'FAIL') + print(f'[{len(results)}/{len(groups)}] {status} {group} in {seconds/60:.1f} min', flush=True) + if ok and not args.keep: + shutil.rmtree(tree) + else: + kept.append(tree) + except BaseException: + for process, _, _ in running.values(): + try: + os.killpg(process.pid, signal.SIGTERM) + except ProcessLookupError: + pass + process.wait() + shutil.rmtree(work, ignore_errors=True) + raise + finally: + durations_path.write_text(json.dumps(durations, indent=1, sort_keys=True)+'\n') + shutil.rmtree(work/'template') + if not kept: + work.rmdir() + failed = sorted(g for g, (ok, _) in results.items() if not ok) + for group in failed: + tail = (LOGS/f'{group}.log').read_text(errors='replace').splitlines()[-30:] + print(f'\n--- {group}: last lines of build/verify-parallel/{group}.log', *tail, sep='\n') + if kept: + print(f'\nKept snapshots under {work}') + total = (time.monotonic()-start)/60 + if failed: + raise SystemExit(f'FAILED {len(failed)} of {len(groups)} groups in {total:.1f} min: '+', '.join(failed)) + print(f'PASS all {len(groups)} groups in {total:.1f} min') + + +if __name__ == '__main__': + main() From f571bcbd6e06618aeae0b8279da48060032dc74b Mon Sep 17 00:00:00 2001 From: eumemic Date: Fri, 9 Oct 2026 00:31:38 -0700 Subject: [PATCH 3/3] Speed up the paired-cube frame algebra with identical results make paired-cube-verify drops from 27.7 s to 14.3 s, and paired_cube_producer.py from 24.6 s to 11.2 s. The regenerated graph, frames, selection and report are byte-identical; the network certificate changes only in the pinned sha256 of frames.py. - basis(): reduce a new row only by the pivots set in it. The rows stay reduced, so the order does not matter and the output is unchanged. - contained(): min(x, x^y) equals x^y exactly when x has the top bit of y, so test that bit directly; first reject when span(A) leaves the union of the supports of B. - perp(): memoize; it is called 130k times with 43.5k distinct arguments. - New caches are bounded like the existing contained() cache. Co-Authored-By: Claude Opus 5.5 (1M context) --- certificates/paired-cube-network.json | 2 +- scripts/paired_cube/frames.py | 29 ++++++++++++++++++++++----- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/certificates/paired-cube-network.json b/certificates/paired-cube-network.json index 11afbc33aa..09e784c5d5 100644 --- a/certificates/paired-cube-network.json +++ b/certificates/paired-cube-network.json @@ -321,7 +321,7 @@ "references/partial-gauge/pr97/SOURCE.json": "68fb539abcd6df21d142e4e204b6e9482eb7f9cd3907650f54bd058070266596", "scripts/paired_cube/README.md": "bf2adf1d1c5a412730be66e019bd73a08826ef8dcd6ffc833b9d1656b755dfb2", "scripts/paired_cube/__init__.py": "b5fb17c79fd41a75c0648e7a5f99076f9f42a619857d5e34e71699bf00ef0c91", - "scripts/paired_cube/frames.py": "7d897418dbfee47de0723ea4983098a982610ccba45e1bac9000a79626d8421c", + "scripts/paired_cube/frames.py": "2a3592c2ed86616088561de9b6896f6e77f9252cbd2fe93c20239da3dcd57018", "scripts/paired_cube/gauges.py": "8a501c66e1330f054e0e11a35e9321d2deea7b51cd03ca56b6a41765e43fe061", "scripts/paired_cube/graph.py": "c757d47997f2fa42a95c16f6e6855cf8b125216ae3335b3891e305cf1da82855", "scripts/paired_cube/modules.py": "18a1ad8af0a7832b7c5c4791f5b95f76386cfa7e82ad52bfd2758c081ada68c4", diff --git a/scripts/paired_cube/frames.py b/scripts/paired_cube/frames.py index 2621ef817b..87de6d8bbf 100644 --- a/scripts/paired_cube/frames.py +++ b/scripts/paired_cube/frames.py @@ -11,18 +11,23 @@ import json, math, sys, functools def basis(rows): - b={} + b={};mask=0 # pivot bits; b stays reduced, so x needs only the pivots set in it, in any order for x in rows: - for p,y in sorted(b.items(),reverse=True): - if x>>p&1:x^=y + m=x&mask + while m: + p=m.bit_length()-1;x^=b[p];m^=1<

>p&1:b[k]=y^x - b[p]=x + b[p]=x;mask|=1<

>t&1:x^=y if x:return False return True