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