diff --git a/research/shared-point-frame-contains/NOTICE.md b/research/shared-point-frame-contains/NOTICE.md new file mode 100644 index 0000000000..040e88e622 --- /dev/null +++ b/research/shared-point-frame-contains/NOTICE.md @@ -0,0 +1,22 @@ +# Notice + +This package accelerates the historical shared-point frame nesting check in +`scripts/shared_point_circuit.py:SharedPointCircuit.verify_frames` (and the +`support_in` / `contained` helpers it uses) while preserving nesting predicates +and receipt fields. + +Predecessor credit: + +- Douglas R. Colkitt — shared-point circuits, exclusion circuits, bit-compression + screens and the historical certificates. +- Closest tooling priors on *related* shared-point surfaces: + CrocSwap/integer-mult-bounds PRs #1994 (verify digests; merged) and open #2054 + (`__init__` merge construction). This package leaves both alone and targets + the residual `verify_frames` / `support_in` LRU thrash. +- Quality-bar priors on *different* objects: #756 (balanced-Fano packed replay), + #1793 (inplace-side prefix), #1861 (parity-side basis/contains), #2117 + (DisjointTensor.frame_data). + +Prepared by Wentao Li with substantial AI assistance under Apache-2.0. +This is not independent human peer review and is not a formal proof of the +multiplication theorem. diff --git a/research/shared-point-frame-contains/README.md b/research/shared-point-frame-contains/README.md new file mode 100644 index 0000000000..c5a0e3da53 --- /dev/null +++ b/research/shared-point-frame-contains/README.md @@ -0,0 +1,96 @@ +# Faster exact shared-point frame nesting + +**Folded into open [CrocSwap/integer-mult-bounds#2054](https://github.com/CrocSwap/integer-mult-bounds/pull/2054)** (same `scripts/shared_point_circuit.py` as `__init__`). Do not open a second upstream PR. + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` (after merged +[CrocSwap/integer-mult-bounds#1994](https://github.com/CrocSwap/integer-mult-bounds/pull/1994) +verify digests), `SharedPointCircuit.support_in` uses +`@lru_cache(maxsize=16384)`. Profiling +`SharedPointCircuit(46).verify_frames` with a precompiled program shows +`contained` / `support_in` dominate the timed window, with far more than +16384 distinct `(node, common)` pairs — the small LRU thrashes. Open +[#2054](https://github.com/CrocSwap/integer-mult-bounds/pull/2054) speeds +`__init__` merge construction on the same file; this package leaves that +surface alone. + +This change memoizes `support_in` in a per-instance dense table indexed by +`node * h + common`, unpacks leaf and two-point pairs without a generator or +`sorted` call, and runs the `verify_frames` nesting walk through local +closures that share that table. Nesting predicates, `circuit_sha256`, and the +`verify_frames` receipt fields stay identical. The bit-compression certificate +does not list `scripts/shared_point_circuit.py` in `source_sha256`. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/shared-point-frame-contains/verify.py +python3.12 -I -O -B research/shared-point-frame-contains/verify.py +python3.12 -B scripts/research_package.py --package research/shared-point-frame-contains +python3.12 -I -B research/shared-point-frame-contains/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_SHARED_POINT_FRAME_CONTAINS cases=5 json_files=… certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/shared-point-frame-contains outcome=completed +PASS_IDENTICAL_SHARED_POINT_FRAME_CONTAINS_RECEIPTS +``` + +On Linux / CPython 3.12.3 (Linux-6.12.94+-x86_64-with-glibc2.39), five +alternating fresh-process pairs timing only +`SharedPointCircuit(46).verify_frames(code)` (construction and compile +excluded) gave median wall time **2.888 → 1.729 seconds (1.67×)**. Timing is +host-descriptive and is not a correctness gate; see `RESULT.json`. + +Default verify is read-only. Full `make verify`, selected cold replay, Lean, and +multiplication-theorem obligations were not rerun for this isolated +historical-checker change. + +## Equivalence argument + +- Dense-table hits return the same bitmask previously returned by the LRU path. +- Leaf triples still select the unique pair complementary to `common`; the + branchless unpack yields the same ordered pair as + `tuple(x for x in triple if x != common)`. +- Two-point stars still OR the same `pair_ids[common][pair]` bits over + `union & ~core`. +- `verify_frames` still compiles (or accepts) the same program, walks the same + forward and reverse role slots, and applies the same + `contained(prev, node)` / `contained(node, prev)` predicates. +- `SharedPointCircuit.verify` digests from #1994 are untouched in structure; + they continue to call `support_in` and receive identical masks. + +## Coverage preserved + +- `verify.py` compares baseline vs optimized `verify` and `verify_frames` + receipts on `h ∈ {6,8,10,12,46}`, plus pointwise `support_in` on sampled + active nodes. +- Corrupting a node's recorded core intersection still raises `AssertionError` + in both engines (skipped under `-O` because historical checks use `assert`). +- Package JSON manifests are scanned for duplicate keys. +- Existing `tests/test_shared_point_network.py` and `tests/test_bit_compression.py` + remain valid consumers; focused + `tests/test_shared_point_frame_contains.py` covers the package controls. + +## Open next questions + +1. **Question:** Should `research/bit-compression-provenance` refresh its live + `scripts/shared_point_circuit.py` SHA-256 pin after this rewrite? + **Why it matters:** That package binds working-tree bytes; a later provenance + replay would otherwise see a hash mismatch. + **First step:** Dedicated pin-only follow-up after confirming receipt identity. + +2. **Question:** After open #2054 merges, does folding its `__init__` rewrite + onto this frame-contains cache keep `circuit_sha256` and frame receipts + identical on one host? + **Why it matters:** Both edit the same production file; a clean fold preserves + combined review-throughput gain without dueling pins. + **First step:** Rebase onto the merged #2054 tip and rerun verify + benchmark. + +## Credit + +Prepared by Wentao Li with substantial AI assistance. See `NOTICE.md`. diff --git a/research/shared-point-frame-contains/RESULT.json b/research/shared-point-frame-contains/RESULT.json new file mode 100644 index 0000000000..072d5a0c14 --- /dev/null +++ b/research/shared-point-frame-contains/RESULT.json @@ -0,0 +1,48 @@ +{ + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "fixture": "SharedPointCircuit(46).verify_frames(code) only (construction and compile excluded)", + "machine": "x86_64", + "median_baseline_seconds": 2.8884478999998464, + "median_optimized_seconds": 1.7294277519999923, + "median_ratio": 1.6701755228916086, + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "rounds": 5, + "samples": [ + { + "baseline_seconds": 2.859907246000148, + "optimized_seconds": 1.7422272750000047, + "ratio": 1.6415236330174776, + "round": 0 + }, + { + "baseline_seconds": 2.8022404520002056, + "optimized_seconds": 1.7294277519999923, + "ratio": 1.6203281396170275, + "round": 1 + }, + { + "baseline_seconds": 2.8884478999998464, + "optimized_seconds": 1.7094040510000923, + "ratio": 1.6897397068352276, + "round": 2 + }, + { + "baseline_seconds": 2.918537890999687, + "optimized_seconds": 1.7926036090002526, + "ratio": 1.6280999750008178, + "round": 3 + }, + { + "baseline_seconds": 2.903088261999983, + "optimized_seconds": 1.7288781760003076, + "ratio": 1.6791745666638958, + "round": 4 + } + ], + "source_pins": { + "research/shared-point-frame-contains/baseline.py": "f5abbf6d61f3c10349416a3e1a1ed038bbd1279ed223367f2df549de46dd7ea5", + "scripts/shared_point_circuit.py": "360d9bffc0f55315fe294789b72c71c79e0991524555b3a5f42a2ca504d7da95" + }, + "status": "PASS_IDENTICAL_SHARED_POINT_FRAME_CONTAINS_RECEIPTS" +} diff --git a/research/shared-point-frame-contains/SOURCES.json b/research/shared-point-frame-contains/SOURCES.json new file mode 100644 index 0000000000..25b5297a02 --- /dev/null +++ b/research/shared-point-frame-contains/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "certificates/bit-compression-audit.json", + "usage": "provenance", + "git_blob": "2c8b221ad7935d49d2479fd44762cf8299066d19", + "sha256": "53effc15424ca20be4e92e8d7b66599b513f208cce1863176fdd1347a46faf90" + }, + { + "path": "docs/research/bit-compression-audit.md", + "usage": "provenance", + "git_blob": "644c6587e436e3577e121dab27bfb817a6e92249", + "sha256": "d97764832d3ea1fe813623431b42383e3ffd713d83863de275425853fd85469d" + }, + { + "path": "scripts/shared_point_circuit.py", + "usage": "provenance", + "git_blob": "32bdbb7e0e7fc4658b7885bc3755d7813a3eba0d", + "sha256": "f5abbf6d61f3c10349416a3e1a1ed038bbd1279ed223367f2df549de46dd7ea5" + }, + { + "path": "scripts/exclusion_circuit.py", + "usage": "provenance", + "git_blob": "b0e2f3e03d7de791ca936dfd92cee2134c7dd4f5", + "sha256": "f9fbcd6e85e442cbd0926ac0887414e20735b2dc923d2d5822c803ceb46726d3" + }, + { + "path": "scripts/shared_point_network.py", + "usage": "provenance", + "git_blob": "0ec7e75046fe714968c49178cd7f83e80e9f9d94", + "sha256": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697" + }, + { + "path": "scripts/audit_bit_compression.py", + "usage": "provenance", + "git_blob": "bc2521f862b1710b4afb060f07bcbeb595f78bce", + "sha256": "f0ed48592a885b54669d3f9086530fc84c467c39fd9281b357ba7550549aaa25" + }, + { + "path": "tests/test_shared_point_network.py", + "usage": "provenance", + "git_blob": "bbf18de66f35c36c91701ff1975cdc1c7aacdcee", + "sha256": "94704721cdf97c8173f4dd5448aa4e82b83b705c3ecfe9769d38aaef4e74975f" + }, + { + "path": "tests/test_bit_compression.py", + "usage": "provenance", + "git_blob": "a021dbf98d06b794e16538bf8c0c6536903086c7", + "sha256": "865e6f32fbf36b9c1571e4654f87e5ce2116f568494383cf1b64954180ef4bc8" + } + ] +} diff --git a/research/shared-point-frame-contains/TASK.json b/research/shared-point-frame-contains/TASK.json new file mode 100644 index 0000000000..34a531f773 --- /dev/null +++ b/research/shared-point-frame-contains/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "c8e1a04f7b29d65e3a90c1482f6d7b51", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Can scripts/shared_point_circuit.py:SharedPointCircuit.verify_frames (and its support_in / contained helpers) keep identical nesting receipts on the historical h=46 circuit after replacing the thrashing lru_cache(maxsize=16384) with a per-instance dense table and local hot-path closures, without touching SharedPointCircuit.__init__, verify digests, or ExclusionCircuit.compile?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after merged #1994 (verify digests) and open #2054 (__init__ merge construction) left verify_frames / support_in as the residual hot path in bit-compression frame checks. Profiling on SharedPointCircuit(46).verify_frames with a precompiled program showed contained/support_in dominating, with CacheInfo misses far above the 16384 LRU cap.", + "bottleneck_link": "Side result on review throughput: audit_bit_compression calls SharedPointCircuit.verify_frames on full-size circuits. Faster identical nesting does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving SharedPointCircuit.verify_frames / support_in change with frozen baseline, identical frame receipts on the historical h=46 circuit, registered replay and a measured before/after median at or above the ~1.5\u00d7 tooling bar. Do not reopen #1994 digests, #2054 __init__, ExclusionCircuit.compile, or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_SHARED_POINT_FRAME_CONTAINS via research/shared-point-frame-contains/verify.py (also under -O); PASS_IDENTICAL_SHARED_POINT_FRAME_CONTAINS_RECEIPTS via benchmark.py; bit-compression certificate does not pin scripts/shared_point_circuit.py in source_sha256. Folded into open CrocSwap #2054 with SharedPointCircuit.__init__ (same production file).", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Should research/bit-compression-provenance refresh its live scripts/shared_point_circuit.py SHA-256 pin after this equivalence-preserving frame-contains rewrite?", + "why_it_matters": "That provenance package binds working-tree bytes of shared_point_circuit.py; leaving the old pin keeps this tooling PR focused, but a later full provenance replay on main would see a hash mismatch until refreshed.", + "first_step": "Open a dedicated provenance follow-up that only rewrites the shared_point_circuit.py entry in SOURCES.json after confirming verify and verify_frames identity.", + "blocked_by": "Pin repair is outside this tooling change." + }, + { + "question": "After open #2054 merges, does folding its __init__ rewrite onto this verify_frames cache still keep circuit_sha256 and frame receipts identical on one host?", + "why_it_matters": "Both edit scripts/shared_point_circuit.py; a clean fold avoids dueling source pins and preserves the combined review-throughput gain.", + "first_step": "Rebase this package onto the merged #2054 tip and rerun verify.py plus benchmark.py.", + "blocked_by": "Open PR #2054 has not merged." + } + ] +} diff --git a/research/shared-point-frame-contains/VERIFY.json b/research/shared-point-frame-contains/VERIFY.json new file mode 100644 index 0000000000..f2bd000d81 --- /dev/null +++ b/research/shared-point-frame-contains/VERIFY.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/shared_point_circuit.py", + "scripts/exclusion_circuit.py", + "scripts/shared_point_network.py", + "scripts/audit_bit_compression.py", + "certificates/bit-compression-audit.json", + "docs/research/bit-compression-audit.md", + "tests/test_shared_point_network.py", + "tests/test_bit_compression.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact baseline copy of the base-commit shared_point_circuit.py; identical SharedPointCircuit.verify and verify_frames receipts on h in {6,8,10,12,46}; support_in bitmask identity; corrupted-core nesting rejection; duplicate JSON-key scan; bit-compression certificate does not pin shared_point_circuit.py." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same receipt equivalence under -O. Historical nesting checks use assert and are stripped under -O; fieldwise receipt identity remains the gate." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_shared_point_frame_contains.py", + "-v" + ], + "timeout_seconds": 180, + "checks": "Focused shared-point frame-contains package controls." + } + ] +} diff --git a/research/shared-point-frame-contains/baseline.py b/research/shared-point-frame-contains/baseline.py new file mode 100644 index 0000000000..32bdbb7e0e --- /dev/null +++ b/research/shared-point-frame-contains/baseline.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Merge equal sums across the common-point circuits, with exact certificates. + +Supports are represented by their provenance in the small pair circuit, not +by half a million dense global bit vectors. A sum that occurs in two distinct +common-point groups must be a pair-star; its fixed pair and union of vertices +identify its support exactly. +""" +from functools import lru_cache +from hashlib import sha256 +from itertools import combinations + +from exclusion_circuit import ExclusionCircuit + + +class SharedPointCircuit: + def __init__(self,h,circuit=None): + assert h>=6 and h!=9, 'The ambient form I-J/9 must be nondegenerate' + self.h=h + self.local=circuit or ExclusionCircuit(h-1) + assert self.local.n==h-1, 'Pair circuit has the wrong ground size' + self.inputs=list(combinations(range(h),3)) + self.variables={t:i+1 for i,t in enumerate(self.inputs)} + self.args=[None]*(len(self.inputs)+1) + self.core=[0]+[sum(1<=2 and key in lookup: + mapping[node]=lookup[key];self.merged+=1 + continue + new=len(self.args);mapping[node]=new + self.args.append((a,b));self.core.append(core);self.union.append(union) + self.provenance.append((common,node)) + if core.bit_count()>=2:lookup[key]=new + for pair,node in sorted(self.local.outputs.items()): + t=tuple(sorted((common,*(self.points[common][x] for x in pair)))) + self.outputs[common,t]=mapping[node] + self.active=set();stack=list(self.outputs.values()) + while stack: + n=stack.pop() + if n in self.active:continue + self.active.add(n) + if self.args[n]:stack.extend(self.args[n]) + self.additions=sum(self.args[n] is not None for n in self.active) + + @lru_cache(maxsize=16384) + def support_in(self,node,common): + """Exact pair-input support in coordinates with this common point.""" + assert self.core[node]&(1< dict: + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), mode], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + check=False, + ) + require(proc.returncode == 0, f"worker {mode} failed: {proc.stderr[-2000:]}") + line = proc.stdout.strip().splitlines()[-1] + return json.loads(line) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--out", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args() + require(args.rounds >= 1, "rounds") + + samples = [] + for i in range(args.rounds): + order = ("optimized", "baseline") if i % 2 == 0 else ("baseline", "optimized") + pair = {} + for mode in order: + pair[mode] = run_worker(mode) + require( + pair["baseline"]["record"] == pair["optimized"]["record"], + f"receipt mismatch on round {i}", + ) + samples.append( + dict( + round=i, + baseline_seconds=pair["baseline"]["seconds"], + optimized_seconds=pair["optimized"]["seconds"], + ratio=pair["baseline"]["seconds"] / pair["optimized"]["seconds"], + ) + ) + print( + f"round {i}: baseline={pair['baseline']['seconds']:.3f}s " + f"optimized={pair['optimized']['seconds']:.3f}s " + f"ratio={samples[-1]['ratio']:.3f}", + flush=True, + ) + + base_med = statistics.median(s["baseline_seconds"] for s in samples) + opt_med = statistics.median(s["optimized_seconds"] for s in samples) + result = dict( + status="PASS_IDENTICAL_SHARED_POINT_FRAME_CONTAINS_RECEIPTS", + fixture=( + "SharedPointCircuit(46).verify_frames(code) only " + "(construction and compile excluded)" + ), + rounds=args.rounds, + median_baseline_seconds=base_med, + median_optimized_seconds=opt_med, + median_ratio=base_med / opt_med, + samples=samples, + python=sys.version, + platform=platform.platform(), + machine=platform.machine(), + source_pins={ + "research/shared-point-frame-contains/baseline.py": sha256( + (PACKAGE / "baseline.py").read_bytes() + ).hexdigest(), + "scripts/shared_point_circuit.py": sha256( + (ROOT / "scripts" / "shared_point_circuit.py").read_bytes() + ).hexdigest(), + }, + base_commit="0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + ) + args.out.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print( + result["status"], + f"median_baseline={base_med:.3f}s", + f"median_optimized={opt_med:.3f}s", + f"median_ratio={result['median_ratio']:.3f}", + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/shared-point-frame-contains/verify.py b/research/shared-point-frame-contains/verify.py new file mode 100644 index 0000000000..209e2e6805 --- /dev/null +++ b/research/shared-point-frame-contains/verify.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and mutation controls for shared-point frame contains. + +Read-only by default. Regenerates no certificate. Timing is not a pass gate; +see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +SCRIPTS = ROOT / "scripts" +sys.path.insert(0, str(SCRIPTS)) + +from certify import require # noqa: E402 +import shared_point_circuit as production # noqa: E402 + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "32bdbb7e0e7fc4658b7885bc3755d7813a3eba0d" +ORIGINAL_SHA256 = "f5abbf6d61f3c10349416a3e1a1ed038bbd1279ed223367f2df549de46dd7ea5" +OPTIMIZED_SHA256 = "360d9bffc0f55315fe294789b72c71c79e0991524555b3a5f42a2ca504d7da95" + + +def load_module(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"missing module {path}") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def git_show(path: str) -> bytes: + return subprocess.check_output(["git", "show", f"{BASE_COMMIT}:{path}"], cwd=ROOT) + + +def check_baseline_bytes() -> None: + baseline = PACKAGE / "baseline.py" + original = git_show("scripts/shared_point_circuit.py") + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base shared_point_circuit.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:scripts/shared_point_circuit.py"], cwd=ROOT + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base shared_point_circuit.py blob drift") + require(baseline.read_bytes() == original, "baseline.py must be an exact copy of the base commit source") + require( + digest_file(SCRIPTS / "shared_point_circuit.py") == OPTIMIZED_SHA256, + "production shared_point_circuit.py does not match the claimed optimized digest", + ) + + +def check_no_duplicate_json_keys() -> dict: + """Reject accidental duplicate keys in package JSON manifests.""" + + def object_pairs(pairs): + seen = set() + out = {} + for key, value in pairs: + require(key not in seen, f"duplicate JSON key {key!r}") + seen.add(key) + out[key] = value + return out + + scanned = 0 + for path in sorted(PACKAGE.glob("*.json")): + text = path.read_text(encoding="utf-8") + json.loads(text, object_pairs_hook=object_pairs) + scanned += 1 + return {"json_files_scanned": scanned} + + +def check_verify_and_frames(baseline, optimized) -> dict: + records = [] + for h in (6, 8, 10, 12, 46): + circuit = optimized.SharedPointCircuit(h) + old_verify = baseline.SharedPointCircuit.verify(circuit) + new_verify = circuit.verify() + require(old_verify == new_verify, f"verify mismatch on h={h}") + code = circuit.compile() + old_frames = baseline.SharedPointCircuit.verify_frames(circuit, code) + new_frames = circuit.verify_frames(code) + require(old_frames == new_frames, f"verify_frames mismatch on h={h}") + # Pointwise support_in identity on a sample of active nodes × commons. + checked = 0 + for node in list(circuit.active)[:200]: + bits = circuit.core[node] + while bits: + bit = bits & -bits + bits -= bit + common = bit.bit_length() - 1 + old = baseline.SharedPointCircuit.support_in(circuit, node, common) + new = circuit.support_in(node, common) + require(old == new, f"support_in mismatch h={h} node={node} common={common}") + checked += 1 + records.append( + dict( + h=h, + roles=new_verify["roles"], + additions=new_verify["additions"], + partial_outputs=new_verify["partial_outputs"], + merged_additions=new_verify["merged_additions"], + circuit_sha256=new_verify["circuit_sha256"], + frame_roles=new_frames["roles"], + support_in_checks=checked, + ) + ) + require(records[-1]["additions"] == 486330, "unexpected full-size additions") + require(records[-1]["roles"] == 531870, "unexpected full-size roles") + require(records[-1]["merged_additions"] == 45706, "unexpected full-size merges") + require(records[-1]["frame_roles"] == 531870, "unexpected full-size frame roles") + return {"cases": len(records), "records": records} + + +def check_nesting_rejection(baseline, optimized) -> dict: + circuit = optimized.SharedPointCircuit(8) + code = circuit.compile() + node = next(n for n in circuit.active if circuit.args[n]) + a, _b = circuit.args[node] + # Drop one child from the recorded core intersection; both engines must reject. + circuit.core[node] = circuit.core[a] + # Invalidate dense cache if the optimized engine already filled it. + circuit.__dict__.pop("_support_in_cache", None) + with _expect_assertion(): + optimized.SharedPointCircuit.verify_frames(circuit, code) + with _expect_assertion(): + baseline.SharedPointCircuit.verify_frames(circuit, code) + return {"nesting_rejection": "preserved"} + + +class _expect_assertion: + def __enter__(self): + return self + + def __exit__(self, exc_type, exc, tb): + require(exc_type is AssertionError, "expected AssertionError from corrupted core") + return True + + +def check_certificate_not_pinning_source() -> dict: + bit = json.loads((ROOT / "certificates/bit-compression-audit.json").read_text()) + pins = bit.get("source_sha256", {}) + require( + "scripts/shared_point_circuit.py" not in pins, + "unexpected certificate pin of shared_point_circuit.py", + ) + return {"bit_compression_certificate_pins_shared_point": False} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--write-certificate", action="store_true", help="unused; kept for API parity") + args = parser.parse_args() + require(not args.write_certificate, "this package does not rewrite certificates") + + check_baseline_bytes() + keys = check_no_duplicate_json_keys() + baseline = load_module(PACKAGE / "baseline.py", "shared_point_frame_contains_baseline") + cases = check_verify_and_frames(baseline, production) + if __debug__: + rejection = check_nesting_rejection(baseline, production) + else: + # Historical nesting checks use assert, stripped under -O. + rejection = {"nesting_rejection": "skipped_under_-O"} + pins = check_certificate_not_pinning_source() + print( + "PASS_SHARED_POINT_FRAME_CONTAINS", + f"cases={cases['cases']}", + f"json_files={keys['json_files_scanned']}", + "certs=0", + "no_new_kappa", + ) + print( + "controls", + rejection["nesting_rejection"], + "certificate_pin=" + str(pins["bit_compression_certificate_pins_shared_point"]), + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/shared-point-init/NOTICE.md b/research/shared-point-init/NOTICE.md new file mode 100644 index 0000000000..08d2575665 --- /dev/null +++ b/research/shared-point-init/NOTICE.md @@ -0,0 +1,21 @@ +# Notice + +This package accelerates the historical shared-point merge construction in +`scripts/shared_point_circuit.py:SharedPointCircuit.__init__` while preserving +node allocation order, merge counts, support checks and `circuit_sha256`. + +Predecessor credit: + +- Douglas R. Colkitt — shared-point circuits, exclusion circuits, bit-compression + screens and the historical certificates. +- Closest tooling priors on *different* objects: CrocSwap/integer-mult-bounds + PRs #756 (balanced-Fano packed replay), #1793 (inplace-side prefix), #1861 + (parity-side basis/contains), #1922 (joint-frame cleared product), #1984 + (mixed-point scalar digests), #1994 (shared-point verify digests), #2039 + (partial-swap verify digests; explicit open question this package answers on + the canonical constructor), #1874 (hosted-audit digest path), and #2001 + (ExclusionCircuit / DisjointTensor support masks — not touched here). + +Prepared by Wentao Li with substantial AI assistance under Apache-2.0. +This is not independent human peer review and is not a formal proof of the +multiplication theorem. diff --git a/research/shared-point-init/README.md b/research/shared-point-init/README.md new file mode 100644 index 0000000000..8b5046caf3 --- /dev/null +++ b/research/shared-point-init/README.md @@ -0,0 +1,121 @@ +# Faster exact shared-point merge construction with identical receipts + +**Tooling improvement; no new kappa.** At base +`0b1cccf86e2f5132ed286a26ef0a681a495740ea`, `SharedPointCircuit.__init__` +builds the common-point merge DAG by, for each of `h` commons, sorting the +local active set, unpacking child mappings through a per-node generator, and +looking up merge keys with repeated attribute access. Profiling on the +historical full-size circuit (`h=46`) shows construction wall time dominated by +that merge/lookup loop. Open +[CrocSwap/integer-mult-bounds#2039](https://github.com/CrocSwap/integer-mult-bounds/pull/2039) +noted construction cost on the partial-swap producer fork; this package +rewrites the canonical `scripts/shared_point_circuit.py` constructor (the +partial-swap `__init__` copy remains a separate follow-up). + +This change pre-sorts `local.active` and `local.outputs` once, unpacks children +directly, binds hot lists/dicts locally, and keeps the historical node-allocation +order. Every structural field (`args`, `core`, `union`, `provenance`, `outputs`, +`active`, `merged_additions`, `additions`) and every verify receipt +(`circuit_sha256`, roles, flags) stays identical. The bit-compression +certificate does not list `scripts/shared_point_circuit.py` in `source_sha256`. +Production `verify` keeps the merged hand-rolled digests from +[CrocSwap/integer-mult-bounds#1994](https://github.com/CrocSwap/integer-mult-bounds/pull/1994); +this package only rewrites `__init__` merge/lookup construction. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/shared-point-init/verify.py +python3.12 -I -O -B research/shared-point-init/verify.py +python3.12 -B scripts/research_package.py --package research/shared-point-init +python3.12 -I -B research/shared-point-init/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_SHARED_POINT_INIT verify_cases=5 mutant=rejected certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/shared-point-init outcome=completed +PASS_IDENTICAL_SHARED_POINT_INIT_RECEIPTS +``` + +Default verify is read-only. Full `make verify`, selected cold replay, Lean, and +multiplication-theorem obligations were not rerun for this isolated +historical-checker change. + +## Result + +On Linux / CPython 3.12.3 (Linux-6.12.94+-x86_64-with-glibc2.39), five +alternating fresh-process pairs timing only `SharedPointCircuit(46)` construction +(verify excluded from the timer; nested `ExclusionCircuit(45)` construction +included) gave median wall time **0.649 → 0.438 seconds (1.48×)**. Timing is +host-descriptive and is not a correctness gate; all samples and environment pins +are in [RESULT.json](RESULT.json). Every verify receipt matches the baseline +checker fieldwise (`roles`, `additions`, `merged_additions`, `circuit_sha256`, +flags), and the constructed DAG matches fieldwise. + +## Equivalence + +The historical constructor walks `sorted(self.local.active)` and +`sorted(self.local.outputs.items())` inside each common-point group, allocates a +new node unless `(core, union)` already appears in the cross-common lookup when +`core.bit_count() >= 2`, and records `(common, local_node)` provenance in +allocation order. This rewrite: + +- sorts those two collections once before the common-point loop; +- replaces `a,b=(mapping[x] for x in self.local.args[node])` with direct indexing; +- uses one `bit_count` and `lookup.get` per internal node; +- binds `args`/`core`/`union`/`provenance` append methods locally; + +and does not change when a merge hits, which node id is allocated, or which +output key is written. A reverse-common-order mutant that walks commons +descending changes `args` / provenance numbering and is rejected by the package +controls. + +## Open next questions + +1. **Question:** Should `research/bit-compression-provenance` refresh its live + `scripts/shared_point_circuit.py` SHA-256 pin after this equivalence-preserving + constructor rewrite? + **Why it matters:** That provenance package binds working-tree bytes; leaving + the old pin keeps this tooling PR focused. + **First step:** Dedicated provenance follow-up that only rewrites that one + `SOURCES.json` entry after confirming `circuit_sha256` identity. + **Blocked by:** Pin repair is outside this tooling change. + +2. **Question:** Is the same merge/lookup construction rewrite worth applying to + `scripts/partial_swap/shared.py:SharedPointCircuit.__init__`? + **Why it matters:** #2039 named that fork; large skip-strip builds still spend + substantial wall time on its constructor. + **First step:** Port after #2039 lands (or in a follow-up that updates the three + `partial_swap` `source_sha256` certificate pins) and remeasure. + **Blocked by:** Avoid concurrent pin conflict with open #2039 on that file. + +## Overlap and credit + +Closest priors (different objects): +[CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756), +[CrocSwap/integer-mult-bounds#1793](https://github.com/CrocSwap/integer-mult-bounds/pull/1793), +[CrocSwap/integer-mult-bounds#1861](https://github.com/CrocSwap/integer-mult-bounds/pull/1861), +[CrocSwap/integer-mult-bounds#1922](https://github.com/CrocSwap/integer-mult-bounds/pull/1922), +[CrocSwap/integer-mult-bounds#1984](https://github.com/CrocSwap/integer-mult-bounds/pull/1984), +[CrocSwap/integer-mult-bounds#1994](https://github.com/CrocSwap/integer-mult-bounds/pull/1994) +(verify digests on this file; this package changes only `__init__`), +[CrocSwap/integer-mult-bounds#2039](https://github.com/CrocSwap/integer-mult-bounds/pull/2039) +(partial-swap verify digests; open question this package answers on the canonical +constructor), +[CrocSwap/integer-mult-bounds#1874](https://github.com/CrocSwap/integer-mult-bounds/pull/1874), +[CrocSwap/integer-mult-bounds#2001](https://github.com/CrocSwap/integer-mult-bounds/pull/2001) +(ExclusionCircuit / DisjointTensor support masks — not touched). +No competing open PR on the canonical `SharedPointCircuit.__init__` merge object +at refresh. + +Douglas R. Colkitt authored the shared-point / exclusion circuits and +bit-compression screens. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. + +Also folded here: `research/shared-point-frame-contains/` (dense `support_in` cache for `verify_frames`, same production file). diff --git a/research/shared-point-init/RESULT.json b/research/shared-point-init/RESULT.json new file mode 100644 index 0000000000..00485fcd9f --- /dev/null +++ b/research/shared-point-init/RESULT.json @@ -0,0 +1,50 @@ +{ + "environment": { + "executable": "/usr/bin/python3.12", + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]" + }, + "fixture": "SharedPointCircuit(46).__init__ only (verify excluded from timer); includes nested ExclusionCircuit(45) construction", + "median_baseline_seconds": 0.6492301979960757, + "median_optimized_seconds": 0.4380384289979702, + "median_ratio": 1.4821306876686935, + "no_new_kappa": true, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 0.6713115739985369, + "optimized_seconds": 0.4732170880015474, + "ratio": 1.4186122839172322, + "round": 0 + }, + { + "baseline_seconds": 0.6492301979960757, + "optimized_seconds": 0.4380384289979702, + "ratio": 1.4821306876686935, + "round": 1 + }, + { + "baseline_seconds": 0.6343938869977137, + "optimized_seconds": 0.41117952200147556, + "ratio": 1.542863525668083, + "round": 2 + }, + { + "baseline_seconds": 0.6534998969946173, + "optimized_seconds": 0.4400633569966885, + "ratio": 1.485013206858609, + "round": 3 + }, + { + "baseline_seconds": 0.6418241709980066, + "optimized_seconds": 0.4299524600064615, + "ratio": 1.492779390047823, + "round": 4 + } + ], + "source_sha256": { + "baseline": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba", + "production": "360d9bffc0f55315fe294789b72c71c79e0991524555b3a5f42a2ca504d7da95" + }, + "status": "PASS_IDENTICAL_SHARED_POINT_INIT_RECEIPTS" +} diff --git a/research/shared-point-init/SOURCES.json b/research/shared-point-init/SOURCES.json new file mode 100644 index 0000000000..fb38e545f7 --- /dev/null +++ b/research/shared-point-init/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "certificates/bit-compression-audit.json", + "usage": "provenance", + "git_blob": "2c8b221ad7935d49d2479fd44762cf8299066d19", + "sha256": "53effc15424ca20be4e92e8d7b66599b513f208cce1863176fdd1347a46faf90" + }, + { + "path": "scripts/shared_point_circuit.py", + "usage": "provenance", + "git_blob": "8347a0bda63fbfb51b86c6c6d10a7bf541816308", + "sha256": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba" + }, + { + "path": "scripts/exclusion_circuit.py", + "usage": "provenance", + "git_blob": "aaa99986c4b81c5d4fbe016fd216a4818940bb95", + "sha256": "b253f9d7318becda1c1f3b24e2287ed44a9c27fcea00cf9d531afb950d0457a0" + }, + { + "path": "scripts/shared_point_network.py", + "usage": "provenance", + "git_blob": "0ec7e75046fe714968c49178cd7f83e80e9f9d94", + "sha256": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697" + }, + { + "path": "scripts/audit_bit_compression.py", + "usage": "provenance", + "git_blob": "bc2521f862b1710b4afb060f07bcbeb595f78bce", + "sha256": "f0ed48592a885b54669d3f9086530fc84c467c39fd9281b357ba7550549aaa25" + } + ] +} diff --git a/research/shared-point-init/TASK.json b/research/shared-point-init/TASK.json new file mode 100644 index 0000000000..daea7099af --- /dev/null +++ b/research/shared-point-init/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "a41f8c2e9b07d35e6c80a1f2947d5e68", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Can scripts/shared_point_circuit.py:SharedPointCircuit.__init__ emit the same merge/lookup DAG (same args/core/union/provenance/outputs/active/merged_additions and the same circuit_sha256) with a tighter construction loop, so full-size shared-point builds stay fieldwise identical?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after open tooling PR #2039 left SharedPointCircuit.__init__ merge/lookup construction as an explicit next question (stated on the partial-swap fork; this package applies the same construction object on the canonical shared_point_circuit.py producer, which still had the historical loop). Profiling named the per-common-point merge loop (repeated sorted(active), per-node generator unpacks, repeated attribute lookups) as the construction bottleneck; verify digests are a different object already claimed by #1994/#2039.", + "bottleneck_link": "Side result on review throughput: shared-point and bit-compression certificates construct SharedPointCircuit(46) before verify. A faster identical constructor does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving SharedPointCircuit.__init__ change with frozen baseline, identical structure and receipts on the historical h=46 circuit, registered replay and a measured before/after median. Do not reopen verify digests, ExclusionCircuit/DisjointTensor support masks (#2001), or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_SHARED_POINT_INIT via research/shared-point-init/verify.py (also under -O); PASS_IDENTICAL_SHARED_POINT_INIT_RECEIPTS via benchmark.py; bit-compression certificate does not pin scripts/shared_point_circuit.py in source_sha256.", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Should research/bit-compression-provenance refresh its live scripts/shared_point_circuit.py SHA-256 pin after this equivalence-preserving constructor rewrite?", + "why_it_matters": "That provenance package binds working-tree bytes of shared_point_circuit.py; leaving the old pin keeps this tooling PR focused, but a later full provenance replay on main would see a hash mismatch until refreshed.", + "first_step": "Open a dedicated provenance follow-up that only rewrites the shared_point_circuit.py entry in SOURCES.json after confirming circuit_sha256 identity.", + "blocked_by": "Pin repair is outside this tooling change." + }, + { + "question": "Is the same merge/lookup construction rewrite worth applying to scripts/partial_swap/shared.py:SharedPointCircuit.__init__ (the fork named in #2039's open question)?", + "why_it_matters": "The partial-swap producer copy still uses the historical loop; large skip-strip builds spend substantial wall time constructing that DAG.", + "first_step": "After #2039's verify-digest change lands or in a follow-up that updates the three partial_swap source_sha256 certificate pins, port this constructor rewrite and remeasure.", + "blocked_by": "Open #2039 already edits that file's verify path and its certificate pin; this package stays on the canonical producer to avoid a pin conflict." + } + ] +} diff --git a/research/shared-point-init/VERIFY.json b/research/shared-point-init/VERIFY.json new file mode 100644 index 0000000000..91edc741d7 --- /dev/null +++ b/research/shared-point-init/VERIFY.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/shared_point_circuit.py", + "scripts/exclusion_circuit.py", + "scripts/shared_point_network.py", + "scripts/audit_bit_compression.py", + "certificates/bit-compression-audit.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact baseline copy of the base-commit shared_point_circuit.py; identical SharedPointCircuit construction structure and verify receipts on h in {6,8,10,12,46}; reverse-common reorder mutant changes node allocation; support-core rejection preserved; bit-compression certificate does not pin shared_point_circuit.py." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same construction equivalence under -O. Historical support checks use assert and are stripped under -O; circuit_sha256 identity and structure equality remain the gates." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_shared_point_init.py", + "-v" + ], + "timeout_seconds": 120, + "checks": "Focused shared-point init package controls." + } + ] +} diff --git a/research/shared-point-init/baseline.py b/research/shared-point-init/baseline.py new file mode 100644 index 0000000000..8347a0bda6 --- /dev/null +++ b/research/shared-point-init/baseline.py @@ -0,0 +1,149 @@ +#!/usr/bin/env python3 +"""Merge equal sums across the common-point circuits, with exact certificates. + +Supports are represented by their provenance in the small pair circuit, not +by half a million dense global bit vectors. A sum that occurs in two distinct +common-point groups must be a pair-star; its fixed pair and union of vertices +identify its support exactly. +""" +from functools import lru_cache +from hashlib import sha256 +from itertools import combinations +import json + +from exclusion_circuit import ExclusionCircuit + + +class SharedPointCircuit: + def __init__(self,h,circuit=None): + assert h>=6 and h!=9, 'The ambient form I-J/9 must be nondegenerate' + self.h=h + self.local=circuit or ExclusionCircuit(h-1) + assert self.local.n==h-1, 'Pair circuit has the wrong ground size' + self.inputs=list(combinations(range(h),3)) + self.variables={t:i+1 for i,t in enumerate(self.inputs)} + self.args=[None]*(len(self.inputs)+1) + self.core=[0]+[sum(1<=2 and key in lookup: + mapping[node]=lookup[key];self.merged+=1 + continue + new=len(self.args);mapping[node]=new + self.args.append((a,b));self.core.append(core);self.union.append(union) + self.provenance.append((common,node)) + if core.bit_count()>=2:lookup[key]=new + for pair,node in sorted(self.local.outputs.items()): + t=tuple(sorted((common,*(self.points[common][x] for x in pair)))) + self.outputs[common,t]=mapping[node] + self.active=set();stack=list(self.outputs.values()) + while stack: + n=stack.pop() + if n in self.active:continue + self.active.add(n) + if self.args[n]:stack.extend(self.args[n]) + self.additions=sum(self.args[n] is not None for n in self.active) + + @lru_cache(maxsize=16384) + def support_in(self,node,common): + """Exact pair-input support in coordinates with this common point.""" + assert self.core[node]&(1< dict: + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), mode], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + check=False, + ) + require(proc.returncode == 0, f"worker {mode} failed: {proc.stderr[-2000:]}") + line = proc.stdout.strip().splitlines()[-1] + return json.loads(line) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--out", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args() + require(args.rounds >= 1, "rounds") + + samples = [] + for i in range(args.rounds): + order = ("optimized", "baseline") if i % 2 == 0 else ("baseline", "optimized") + pair = {} + for mode in order: + pair[mode] = run_worker(mode) + require( + pair["baseline"]["record"] == pair["optimized"]["record"], + f"receipt mismatch on round {i}", + ) + samples.append( + dict( + round=i, + baseline_seconds=pair["baseline"]["seconds"], + optimized_seconds=pair["optimized"]["seconds"], + ratio=pair["baseline"]["seconds"] / pair["optimized"]["seconds"], + ) + ) + print( + f"round {i}: baseline={pair['baseline']['seconds']:.3f}s " + f"optimized={pair['optimized']['seconds']:.3f}s " + f"ratio={samples[-1]['ratio']:.3f}", + flush=True, + ) + + base_med = statistics.median(s["baseline_seconds"] for s in samples) + opt_med = statistics.median(s["optimized_seconds"] for s in samples) + result = dict( + status="PASS_IDENTICAL_SHARED_POINT_INIT_RECEIPTS", + fixture=( + "SharedPointCircuit(46).__init__ only (verify excluded from timer); " + "includes nested ExclusionCircuit(45) construction" + ), + rounds=args.rounds, + median_baseline_seconds=base_med, + median_optimized_seconds=opt_med, + median_ratio=base_med / opt_med, + samples=samples, + environment=dict( + python=sys.version, + platform=platform.platform(), + executable=sys.executable, + ), + source_sha256=dict( + baseline=sha256((PACKAGE / "baseline.py").read_bytes()).hexdigest(), + production=sha256((ROOT / "scripts/shared_point_circuit.py").read_bytes()).hexdigest(), + ), + no_new_kappa=True, + ) + args.out.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print( + "PASS_IDENTICAL_SHARED_POINT_INIT_RECEIPTS", + f"median {base_med:.3f} -> {opt_med:.3f} s ({base_med / opt_med:.2f}x)", + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/shared-point-init/verify.py b/research/shared-point-init/verify.py new file mode 100644 index 0000000000..fcded43d90 --- /dev/null +++ b/research/shared-point-init/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and mutation controls for shared-point merge construction. + +Read-only by default. Regenerates no certificate. Timing is not a pass gate; +see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +SCRIPTS = ROOT / "scripts" +sys.path.insert(0, str(SCRIPTS)) + +from certify import require # noqa: E402 +import shared_point_circuit as production # noqa: E402 + +BASE_COMMIT = "0b1cccf86e2f5132ed286a26ef0a681a495740ea" +ORIGINAL_BLOB = "8347a0bda63fbfb51b86c6c6d10a7bf541816308" +ORIGINAL_SHA256 = "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba" +OPTIMIZED_SHA256 = "360d9bffc0f55315fe294789b72c71c79e0991524555b3a5f42a2ca504d7da95" +FULL_SIZE_SHA256 = "b0402f9eaaf138129939521c2a2ef1c3e8230b730de0a7bdea3596eb415dd173" + + +def load_module(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"missing module {path}") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def git_show(path: str) -> bytes: + return subprocess.check_output(["git", "show", f"{BASE_COMMIT}:{path}"], cwd=ROOT) + + +def check_baseline_bytes() -> None: + baseline = PACKAGE / "baseline.py" + original = git_show("scripts/shared_point_circuit.py") + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base shared_point_circuit.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:scripts/shared_point_circuit.py"], cwd=ROOT + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base shared_point_circuit.py blob drift") + require(baseline.read_bytes() == original, "baseline.py must be an exact copy of the base commit source") + require( + digest_file(SCRIPTS / "shared_point_circuit.py") == OPTIMIZED_SHA256, + "production shared_point_circuit.py does not match the claimed optimized digest", + ) + + +def circuit_structure(circuit) -> dict: + return dict( + args=circuit.args, + core=circuit.core, + union=circuit.union, + provenance=circuit.provenance, + outputs=dict(sorted(circuit.outputs.items())), + active=sorted(circuit.active), + additions=circuit.additions, + merged=circuit.merged, + pair_ids=circuit.pair_ids, + variables=circuit.variables, + points=circuit.points, + ) + + +def check_construction_equivalence(baseline, optimized) -> dict: + records = [] + for h in (6, 8, 10, 12, 46): + old = baseline.SharedPointCircuit(h) + new = optimized.SharedPointCircuit(h) + require(circuit_structure(old) == circuit_structure(new), f"structure mismatch on h={h}") + old_receipt = old.verify() + new_receipt = new.verify() + require(old_receipt == new_receipt, f"verify mismatch on h={h}") + require( + baseline.SharedPointCircuit.verify(new) == new_receipt, + f"cross-engine verify mismatch on h={h}", + ) + records.append( + dict( + h=h, + roles=new_receipt["roles"], + additions=new_receipt["additions"], + partial_outputs=new_receipt["partial_outputs"], + merged_additions=new_receipt["merged_additions"], + circuit_sha256=new_receipt["circuit_sha256"], + ) + ) + require(records[-1]["additions"] == 486330, "unexpected full-size additions") + require(records[-1]["roles"] == 531870, "unexpected full-size roles") + require(records[-1]["merged_additions"] == 45706, "unexpected full-size merges") + require( + records[-1]["circuit_sha256"] == FULL_SIZE_SHA256, + "unexpected full-size circuit_sha256", + ) + return {"verify_cases": len(records), "records": records} + + +def check_reorder_mutant_rejected(baseline, optimized) -> dict: + """A mutant that walks commons in reverse must change node allocation order.""" + from itertools import combinations + + circuit = optimized.SharedPointCircuit(8) + local = circuit.local + active_sorted = sorted(local.active) + h = 8 + inputs = list(combinations(range(h), 3)) + variables = {t: i + 1 for i, t in enumerate(inputs)} + args = [None] * (len(inputs) + 1) + core = [0] + [sum(1 << i for i in t) for t in inputs] + union = list(core) + provenance = [None] * len(args) + points = [[j for j in range(h) if j != i] for i in range(h)] + lookup = {} + merged = 0 + # Historical contract: commons ascend. Reverse order preserves per-common + # topology but changes when cross-common merges are discovered. + for common in range(h - 1, -1, -1): + mapping = {} + pts = points[common] + for node in active_sorted: + if local.args[node] is None: + a, b = local.inputs[node - 1] + t = tuple(sorted((common, pts[a], pts[b]))) + mapping[node] = variables[t] + continue + a, b = (mapping[x] for x in local.args[node]) + cval = core[a] & core[b] + uval = union[a] | union[b] + key = (cval, uval) + if cval.bit_count() >= 2 and key in lookup: + mapping[node] = lookup[key] + merged += 1 + continue + new = len(args) + mapping[node] = new + args.append((a, b)) + core.append(cval) + union.append(uval) + provenance.append((common, node)) + if cval.bit_count() >= 2: + lookup[key] = new + require(args != circuit.args, "reverse-common mutant must change args allocation") + require(provenance != circuit.provenance, "reverse-common mutant must change provenance order") + require(merged > 0, "mutant should still perform some merges") + return {"reorder_mutant": "rejected"} + + +def check_support_rejection(baseline, optimized) -> dict: + circuit = optimized.SharedPointCircuit(8) + node = next(n for n in circuit.active if circuit.args[n]) + a, _b = circuit.args[node] + circuit.core[node] = circuit.core[a] + with _expect_assertion(): + optimized.SharedPointCircuit.verify(circuit) + with _expect_assertion(): + baseline.SharedPointCircuit.verify(circuit) + return {"support_rejection": "preserved"} + + +class _expect_assertion: + def __enter__(self): + return self + + def __exit__(self, exc_type, exc, tb): + require(exc_type is AssertionError, "expected AssertionError from corrupted core") + return True + + +def check_certificate_not_pinning_source() -> dict: + bit = json.loads((ROOT / "certificates/bit-compression-audit.json").read_text()) + pins = bit.get("source_sha256", {}) + require( + "scripts/shared_point_circuit.py" not in pins, + "unexpected certificate pin of shared_point_circuit.py", + ) + return {"bit_compression_certificate_pins_shared_point": False} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--write-certificate", action="store_true", help="unused; kept for API parity") + args = parser.parse_args() + require(not args.write_certificate, "this package does not rewrite certificates") + + check_baseline_bytes() + baseline = load_module(PACKAGE / "baseline.py", "shared_point_init_baseline") + verifies = check_construction_equivalence(baseline, production) + mutant = check_reorder_mutant_rejected(baseline, production) + if __debug__: + rejection = check_support_rejection(baseline, production) + else: + # Historical SharedPointCircuit.verify uses assert, stripped under -O. + rejection = {"support_rejection": "skipped_under_-O"} + pins = check_certificate_not_pinning_source() + print( + "PASS_SHARED_POINT_INIT", + f"verify_cases={verifies['verify_cases']}", + f"mutant={mutant['reorder_mutant']}", + "certs=0", + "no_new_kappa", + ) + print( + "controls", + rejection["support_rejection"], + "certificate_pin=" + str(pins["bit_compression_certificate_pins_shared_point"]), + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/scripts/shared_point_circuit.py b/scripts/shared_point_circuit.py index 8347a0bda6..d086427188 100644 --- a/scripts/shared_point_circuit.py +++ b/scripts/shared_point_circuit.py @@ -6,105 +6,192 @@ common-point groups must be a pair-star; its fixed pair and union of vertices identify its support exactly. """ -from functools import lru_cache from hashlib import sha256 from itertools import combinations -import json from exclusion_circuit import ExclusionCircuit class SharedPointCircuit: def __init__(self,h,circuit=None): + """Merge equal pair-star sums across common-point groups. + + Tooling note (shared-point / bit-compression replay): the merge/lookup + loop keeps the historical node-allocation order and output keys, but + pre-sorts the local active set and output items once, unpacks child + mappings without a per-node generator, and binds hot attributes locally. + ``merged_additions``, topology and ``circuit_sha256`` are unchanged. + See ``research/shared-point-init/``. + """ assert h>=6 and h!=9, 'The ambient form I-J/9 must be nondegenerate' self.h=h self.local=circuit or ExclusionCircuit(h-1) assert self.local.n==h-1, 'Pair circuit has the wrong ground size' self.inputs=list(combinations(range(h),3)) self.variables={t:i+1 for i,t in enumerate(self.inputs)} - self.args=[None]*(len(self.inputs)+1) + nin=len(self.inputs) + self.args=[None]*(nin+1) self.core=[0]+[sum(1<=2 and key in lookup: - mapping[node]=lookup[key];self.merged+=1 + pts=self.points[common] + bit=1<=2:lookup[key]=new - for pair,node in sorted(self.local.outputs.items()): - t=tuple(sorted((common,*(self.points[common][x] for x in pair)))) - self.outputs[common,t]=mapping[node] - self.active=set();stack=list(self.outputs.values()) + a=mapping[ab[0]];b=mapping[ab[1]] + cval=core[a]&core[b];uval=union[a]|union[b] + assert cval&bit + if cval.bit_count()>=2: + key=(cval,uval) + hit=lookup.get(key) + if hit is not None: + mapping[node]=hit;self.merged+=1 + continue + new=len(args);mapping[node]=new + append_args((a,b));append_core(cval);append_union(uval) + append_prov((common,node));lookup[key]=new + else: + new=len(args);mapping[node]=new + append_args((a,b));append_core(cval);append_union(uval) + append_prov((common,node)) + outs=self.outputs + for pair,node in outputs_items: + outs[common,tuple(sorted((common,*(pts[x] for x in pair))))]=mapping[node] + self.active=set();stack=list(self.outputs.values());active=self.active while stack: n=stack.pop() - if n in self.active:continue - self.active.add(n) - if self.args[n]:stack.extend(self.args[n]) - self.additions=sum(self.args[n] is not None for n in self.active) + if n in active:continue + active.add(n) + edge=args[n] + if edge:stack.extend(edge) + self.additions=sum(args[n] is not None for n in active) - @lru_cache(maxsize=16384) def support_in(self,node,common): - """Exact pair-input support in coordinates with this common point.""" - assert self.core[node]&(1<