Faster verification: concurrent checks, make verify-parallel, faster paired-cube frames, no joint-dual re-pins

.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

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;

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

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": {

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,

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",

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"
   },

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

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):

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
         if x:
             p=x.bit_length()-1
             for k,y in list(b.items()):
                 if y>>p&1:b[k]=y^x
-            b[p]=x
+            b[p]=x;mask|=1<<p
     return tuple(b[p] for p in sorted(b,reverse=True))
 
 def perp(rows,h):
+    return _perp(tuple(rows),h)
+
+@functools.lru_cache(maxsize=500000)
+def _perp(rows,h):
     rows=basis(rows); piv={r.bit_length()-1:r for r in rows}; out=[]
     for j in range(h):
         if j in piv:continue
@@ -32,10 +37,24 @@ def perp(rows,h):
         out.append(x)
     return basis(out)
 
+@functools.lru_cache(maxsize=500000)
+def _support(A):
+    u=0
+    for x in A:u|=x
+    return u
+
+@functools.lru_cache(maxsize=500000)
+def _tops(B):
+    # min(x,x^y) == x^y exactly when x has the top bit of y set
+    return tuple((y.bit_length()-1,y) for y in B if y)
+
 @functools.lru_cache(maxsize=500000)
 def contained(A,B):
+    if _support(A)&~_support(B):return False  # XORs of rows of B cannot leave the union of their supports
+    tops=_tops(B)
     for x in A:
-        for y in B:x=min(x,x^y)
+        for t,y in tops:
+            if x>>t&1:x^=y
         if x:return False
     return True
 

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')

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')