diff --git a/research/shared-point-digest/NOTICE.md b/research/shared-point-digest/NOTICE.md new file mode 100644 index 0000000000..d749102f92 --- /dev/null +++ b/research/shared-point-digest/NOTICE.md @@ -0,0 +1,19 @@ +# Notice + +This package accelerates the historical shared-point verify digest in +`scripts/shared_point_circuit.py:SharedPointCircuit.verify` while preserving +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; explicit open question this package answers), + and #1874 (hosted-audit digest path). + +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-digest/README.md b/research/shared-point-digest/README.md new file mode 100644 index 0000000000..0a0f404914 --- /dev/null +++ b/research/shared-point-digest/README.md @@ -0,0 +1,102 @@ +# Faster exact shared-point verify digests with identical receipts + +**Tooling improvement; no new kappa.** At base +`0b1cccf86e2f5132ed286a26ef0a681a495740ea`, `SharedPointCircuit.verify` builds +`circuit_sha256` with per-active-node and per-partial-output +`json.dumps(..., separators=(',',':'))` updates. Profiling on the historical +full-size circuit (`h=46`, 501510 active nodes, 45540 partial outputs) shows +about half of verify wall time in that JSON encoder path. Open +[CrocSwap/integer-mult-bounds#1984](https://github.com/CrocSwap/integer-mult-bounds/pull/1984) +left this object as an explicit next question after shipping mixed-point +`scalar_check` digests. + +This change writes the same UTF-8 digest lines with an equivalent hand-rolled +formatter (`[node,null,null]`, `[node,[a,b],[common,local]]`, +`[common,[t0,t1,t2],node]`), keeps every support and topology assertion, and +leaves `circuit_sha256` unchanged. 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-digest/verify.py +python3.12 -I -O -B research/shared-point-digest/verify.py +python3.12 -B scripts/research_package.py --package research/shared-point-digest +python3.12 -I -B research/shared-point-digest/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_SHARED_POINT_DIGEST verify_cases=5 encoding_cases=8 certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/shared-point-digest outcome=completed +PASS_IDENTICAL_SHARED_POINT_DIGEST_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).verify` +(construction excluded; nested `ExclusionCircuit.verify` included) gave median +wall time **2.212 → 1.070 seconds (2.07×)**. 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). + +## Equivalence + +For each active node the historical encoder emitted + +- `json.dumps((node, None, None), separators=(',',':'))+'\n'` → `[node,null,null]\n` +- `json.dumps((node, (a,b), (common,local)), separators=(',',':'))+'\n'` → `[node,[a,b],[common,local]]\n` + +and for each partial output + +- `json.dumps((common, (t0,t1,t2), node), separators=(',',':'))+'\n'` → `[common,[t0,t1,t2],node]\n` + +with default JSON integer formatting (no whitespace). The hand-rolled writer +emits those exact byte strings. A `None` vs `null` spelling mutant and a flat +`[node,a,b,common,local]` mutant differ and are rejected by the package +controls. Support and topology checks remain the historical `assert` gates. + +## 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 + digest 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 `ExclusionCircuit.verify`'s leave-two-out expected-support + genexpr worth a separate identical-receipt rewrite? + **Why it matters:** Its single `json.dumps` is not hot; the support sum is. + **First step:** Profile `ExclusionCircuit(45).verify` alone and prototype a + closed-form support mask if one matches the historical expected bits. + **Blocked by:** Out of this session’s stop rule. + +## 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) +(mixed-point `scalar_check`; this package answers its SharedPoint open question), +[CrocSwap/integer-mult-bounds#1874](https://github.com/CrocSwap/integer-mult-bounds/pull/1874). +No competing open PR on the `SharedPointCircuit.verify` digest 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. diff --git a/research/shared-point-digest/RESULT.json b/research/shared-point-digest/RESULT.json new file mode 100644 index 0000000000..b8a02768fc --- /dev/null +++ b/research/shared-point-digest/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).verify only (construction excluded); includes nested ExclusionCircuit.verify", + "median_baseline_seconds": 2.212151175000031, + "median_optimized_seconds": 1.0697961950000945, + "median_ratio": 2.0678248673335724, + "no_new_kappa": true, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 2.2307621030000746, + "optimized_seconds": 1.0840965989999631, + "ratio": 2.0577152488605406, + "round": 0 + }, + { + "baseline_seconds": 2.531811613000059, + "optimized_seconds": 1.049210721999998, + "ratio": 2.4130630386372127, + "round": 1 + }, + { + "baseline_seconds": 2.1824195049999844, + "optimized_seconds": 0.999130652999952, + "ratio": 2.1843184356791916, + "round": 2 + }, + { + "baseline_seconds": 2.212151175000031, + "optimized_seconds": 1.0697961950000945, + "ratio": 2.0678248673335724, + "round": 3 + }, + { + "baseline_seconds": 2.1475713770000766, + "optimized_seconds": 1.0859181539999554, + "ratio": 1.97765491726015, + "round": 4 + } + ], + "source_sha256": { + "baseline": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba", + "production": "f5abbf6d61f3c10349416a3e1a1ed038bbd1279ed223367f2df549de46dd7ea5" + }, + "status": "PASS_IDENTICAL_SHARED_POINT_DIGEST_RECEIPTS" +} diff --git a/research/shared-point-digest/SOURCES.json b/research/shared-point-digest/SOURCES.json new file mode 100644 index 0000000000..9a95ed4f32 --- /dev/null +++ b/research/shared-point-digest/SOURCES.json @@ -0,0 +1,66 @@ +{ + "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": "docs/research/bit-compression-audit.md", + "usage": "provenance", + "git_blob": "644c6587e436e3577e121dab27bfb817a6e92249", + "sha256": "d97764832d3ea1fe813623431b42383e3ffd713d83863de275425853fd85469d" + }, + { + "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" + }, + { + "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-digest/TASK.json b/research/shared-point-digest/TASK.json new file mode 100644 index 0000000000..38d6f55683 --- /dev/null +++ b/research/shared-point-digest/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "7c2a91e04f8b3d65a1e0c9d2478f5b36", + "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 emit the same circuit_sha256 digest lines (and the same support/topology assertion checks) without per-node json.dumps, so full-size shared-point and bit-compression verify receipts 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 #1984 left SharedPointCircuit.verify / ExclusionCircuit.verify digests as an explicit next question. Profiling named SharedPointCircuit.verify's per-node json.dumps stream (about half of h=46 verify time) as the bottleneck; ExclusionCircuit.verify's single json.dumps is not hot.", + "bottleneck_link": "Side result on review throughput: shared-point verify and bit-compression certificates call SharedPointCircuit.verify. A faster identical digest does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving SharedPointCircuit.verify digest change with frozen baseline, identical receipts on the historical h=46 circuit, registered replay and a measured before/after median. Do not reopen the mathematical screens, rewrite ExclusionCircuit support enumeration, or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_SHARED_POINT_DIGEST via research/shared-point-digest/verify.py (also under -O); PASS_IDENTICAL_SHARED_POINT_DIGEST_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 digest 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 ExclusionCircuit.verify's leave-two-out expected-support genexpr worth a separate identical-receipt rewrite?", + "why_it_matters": "Profiling shows that single json.dumps is negligible there; the hot path is the per-output support sum genexpr, a different object from digest formatting.", + "first_step": "Profile ExclusionCircuit(45).verify alone and prototype a closed-form support mask if one matches the historical expected bits.", + "blocked_by": "Out of this session's stop rule; SharedPointCircuit.verify digests were the measured bottleneck." + } + ] +} diff --git a/research/shared-point-digest/VERIFY.json b/research/shared-point-digest/VERIFY.json new file mode 100644 index 0000000000..ead3cbd423 --- /dev/null +++ b/research/shared-point-digest/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 receipts on h in {6,8,10,12,46}; encoding foil rejects wrong null and flat encodings; 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 digest equivalence under -O. Historical support checks use assert and are stripped under -O; circuit_sha256 identity remains the gate." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_shared_point_digest.py", + "-v" + ], + "timeout_seconds": 120, + "checks": "Focused shared-point digest package controls." + } + ] +} diff --git a/research/shared-point-digest/baseline.py b/research/shared-point-digest/baseline.py new file mode 100644 index 0000000000..8347a0bda6 --- /dev/null +++ b/research/shared-point-digest/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_DIGEST_RECEIPTS", + fixture=( + "SharedPointCircuit(46).verify only (construction excluded); " + "includes nested ExclusionCircuit.verify" + ), + 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_DIGEST_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-digest/verify.py b/research/shared-point-digest/verify.py new file mode 100644 index 0000000000..07db45f5b0 --- /dev/null +++ b/research/shared-point-digest/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and mutation controls for shared-point verify digests. + +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 = "f5abbf6d61f3c10349416a3e1a1ed038bbd1279ed223367f2df549de46dd7ea5" + + +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_encoding_foil() -> dict: + """Hand-rolled lines must match json.dumps text, and mutants must differ.""" + node_samples = [ + (1, None, None), + (5, (1, 2), (0, 3)), + (999999, (0, 1), (2, 4)), + (42, None, None), + (7, (100, 200), (3, 9)), + ] + for node, edge, prov in node_samples: + old = json.dumps((node, edge, prov), separators=(",", ":")) + "\n" + if edge is None: + new = f"[{node},null,null]\n" + else: + a, b = edge + common, local = prov + new = f"[{node},[{a},{b}],[{common},{local}]]\n" + require(old == new, f"node encoding mismatch for {(node, edge, prov)}") + output_samples = [ + (0, (0, 1, 2), 22), + (5, (1, 3, 5), 100), + (45, (0, 22, 45), 531870), + ] + for common, target, node in output_samples: + old = json.dumps((common, target, node), separators=(",", ":")) + "\n" + t0, t1, t2 = target + new = f"[{common},[{t0},{t1},{t2}],{node}]\n" + require(old == new, f"output encoding mismatch for {(common, target, node)}") + # Mutant foils: Python None spelling and a dropped nested bracket. + bad_none = "[0,None,None]\n" + good_none = json.dumps((0, None, None), separators=(",", ":")) + "\n" + require(bad_none != good_none, "mutant None spelling must differ from json null") + bad_flat = "[5,1,2,0,3]\n" + good_nested = json.dumps((5, (1, 2), (0, 3)), separators=(",", ":")) + "\n" + require(bad_flat != good_nested, "mutant flat triple must differ from nested encoding") + return { + "node_encoding_cases": len(node_samples), + "output_encoding_cases": len(output_samples), + "none_mutant": "rejected", + "flat_mutant": "rejected", + } + + +def check_verify_equivalence(baseline, optimized) -> dict: + records = [] + for h in (6, 8, 10, 12, 46): + circuit = optimized.SharedPointCircuit(h) + old = baseline.SharedPointCircuit.verify(circuit) + new = circuit.verify() + require(old == new, f"verify mismatch on h={h}") + records.append( + dict( + h=h, + roles=new["roles"], + additions=new["additions"], + partial_outputs=new["partial_outputs"], + merged_additions=new["merged_additions"], + circuit_sha256=new["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") + return {"verify_cases": len(records), "records": records} + + +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] + # Drop one child from the recorded core intersection; both engines must reject. + 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_digest_baseline") + encoding = check_encoding_foil() + verifies = check_verify_equivalence(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_DIGEST", + f"verify_cases={verifies['verify_cases']}", + f"encoding_cases={encoding['node_encoding_cases'] + encoding['output_encoding_cases']}", + "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..32bdbb7e0e 100644 --- a/scripts/shared_point_circuit.py +++ b/scripts/shared_point_circuit.py @@ -9,7 +9,6 @@ from functools import lru_cache from hashlib import sha256 from itertools import combinations -import json from exclusion_circuit import ExclusionCircuit @@ -87,24 +86,52 @@ def contained(self,a,b): self.support_in(a,common)&~self.support_in(b,common)) def verify(self): + """Exact support nesting and a byte-stable circuit digest. + + Tooling note (shared-point / bit-compression replay): node and partial- + output digest lines are written with the same UTF-8 text that + ``json.dumps(..., separators=(',',':'))`` produced historically, but + without building JSON encoder objects per row. Support checks and + ``circuit_sha256`` are unchanged. See ``research/shared-point-digest/``. + """ self.local.verify() digest=sha256() + update=digest.update + encode=str.encode + args=self.args + provenance=self.provenance + support_in=self.support_in + local_support=self.local.support + core=self.core + union=self.union for node in sorted(self.active): - if self.args[node]: - a,b=self.args[node];common,local=self.provenance[node] + edge=args[node] + if edge: + a,b=edge;common,local=provenance[node] assert a