diff --git a/certificates/inplace-side.json b/certificates/inplace-side.json index 8d3240c59c..260ed13927 100644 --- a/certificates/inplace-side.json +++ b/certificates/inplace-side.json @@ -5609,7 +5609,7 @@ "docs/research/inplace-side.md": "c228f131d95f3ea348455c13378c19ed6e3c75af7e14cf68ea0ada445ab3ac72", "scripts/audit_inplace_side.py": "16d295f9f9250d35f6f1de2843d5e13c7adbf88d595ebcd0b65b00d1a938acd9", "scripts/experiments/core_limits.py": "a31a27cc24cf0349a507d1141a2b965ea25f1c60f355d7e13c581305a12d3a43", - "scripts/experiments/inplace_side.py": "4e7cb3df2e263f6c7f5907c55e3ee04c08926e6dbc984bbda1722a27b0a48ff6", + "scripts/experiments/inplace_side.py": "4397b84f3ac52554bf14303171410a2799af0bf8dae11ec64594bb5c011e93a2", "scripts/experiments/inplace_side_witnesses.json": "90fe710f5daa35cc9e4892b29d712d66110b7b2b4c404da95a960ea7041618b9" }, "status": "SPECIFIED IN-PLACE FAMILY EXCLUDED; NO STRONGER KAPPA", diff --git a/research/inplace-side-performance/README.md b/research/inplace-side-performance/README.md new file mode 100644 index 0000000000..38e51f5626 --- /dev/null +++ b/research/inplace-side-performance/README.md @@ -0,0 +1,121 @@ +# Faster historical inplace-side prefix replay + +**Tooling improvement; no new kappa.** The historical +`scripts/experiments/inplace_side.py:verify_prefix` check rejects a specified +n-role Gauss–Jordan side family using three pinned witnesses (`h = 42, 46, 50`). +Each elimination column previously rebuilt `sorted(unused)` to locate the least +unused row with the pivot bit set. The production checker now scans an unused +flag array from index 0 and tests bits with a column mask. The lexicographic +rule, XOR updates, switch witnesses, deficit arithmetic and every receipt field +are unchanged. + +The selected frontier, `upstream/` and the mathematical rejection in +[docs/research/inplace-side.md](../../docs/research/inplace-side.md) are not +reopened. Only the source pin for `scripts/experiments/inplace_side.py` changes +inside `certificates/inplace-side.json`. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/inplace-side-performance/verify.py +python3.12 -I -O -B research/inplace-side-performance/verify.py +python3.12 -I -B -m unittest tests.test_inplace_side tests.test_inplace_side_performance -v +python3.12 -B scripts/research_package.py --package research/inplace-side-performance --check-only +python3.12 -B scripts/research_package.py --package research/inplace-side-performance +``` + +Expected verifier line: + +```text +PASS_INPLACE_SIDE_PREFIX_FAST witnesses=3 h=[42, 46, 50] paths=[151, 415, 767] ... no_new_kappa +``` + +Expected registered replay: + +```text +PASS_REGISTERED_RESEARCH_PACKAGE research/inplace-side-performance outcome=completed +``` + +Normal verification is read-only. To regenerate the certificate after editing the +production source: + +```sh +python3.12 -I -B research/inplace-side-performance/verify.py --write-certificate +``` + +Before/after wall times (descriptive; not a pass gate): + +```sh +python3.12 -I -B research/inplace-side-performance/benchmark.py --rounds 5 +``` + +Expected: `PASS_IDENTICAL_INPLACE_PREFIX_RECEIPTS`. Samples are retained in +[RESULT.json](RESULT.json). On this Linux host / CPython 3.12.3, five alternating +fresh-process pairs gave median **17.061 s → 5.466 s (3.12×)** for the three +pinned witnesses. Timing is descriptive, not a correctness gate. + +## Why the receipts stay identical + +For each column `col`, the original code selected + +```text +min{ i in unused : rows[i] has bit col } +``` + +by materializing `sorted(unused)` and taking the first hit. Scanning +`i = 0, 1, …` over a boolean unused table and stopping at the first hit yields +the same index, because the integers are totally ordered. Column tests +`rows[i] & (1 << col)` equal `rows[i] >> col & 1` on these nonnegative row +masks. The subsequent row-XOR updates therefore run on the same pivot sequence +and produce the same residual matrix, the same certified nonorthogonal path +list and the same deficit upper bound. + +[baseline.py](baseline.py) is a byte-identical copy of +`scripts/experiments/inplace_side.py` at base +`0b1cccf86e2f5132ed286a26ef0a681a495740ea` (blob +`db3de6f1d962ccc3a4eae31f83c72bba995ba44e`). The verifier compares every field +of every witness receipt against that baseline, checks shared rejection +behavior, rejects a greatest-unused mutant on all three witnesses, and requires +the working certificate to differ from the base certificate only in the single +`inplace_side.py` source pin. + +## Task card, overlap and limits + +Chooser seed `1cd1f71746c2d200dd617bc3dd17d8a6` drew `bit-mechanisms`; live +helper-contract and register-model surfaces were saturated. Expertise override +to `replay-runtime` (verifier-engineering). Scope **refined** to this fixed +historical screen inside `make verify-certificates`. + +Closest priors (different objects; no code reused here): + +- [CrocSwap #756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) — + packed-column balanced-Fano replay (2.91×) on a different checker. +- [CrocSwap #1584](https://github.com/CrocSwap/integer-mult-bounds/pull/1584) — + finite-bit block-core frame interning. +- [CrocSwap #1076](https://github.com/CrocSwap/integer-mult-bounds/pull/1076) / + [#1075](https://github.com/CrocSwap/integer-mult-bounds/pull/1075) — + quadratic-affine / quadratic-code tooling. +- Local `find_overlap.py` for `inplace side` / `inplace_side` / `verify_prefix` + reported no competing open PR on this object at refresh time. + +Limits: timing is host-descriptive; OS caches were not flushed. Full +`make verify`, selected-supplier cold replay, Lean and multiplication-theorem +obligations were not rerun for this isolated historical-checker change. + +## Open next questions + +- Can the same least-unused scan replace `sorted(unused)` inside `compile_side` + without changing gate lists on `h = 6, 10` and, if identical, on `h = 50`? +- Should CI grow a soft regression timer for this screen, or keep RESULT.json + descriptive only? + +## Credit + +Douglas R. Colkitt authored the inplace-side rejection, witnesses and original +checker. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) +with substantial AI assistance, under Apache-2.0. No independent human +peer-review or formal proof-assistant claim. diff --git a/research/inplace-side-performance/RESULT.json b/research/inplace-side-performance/RESULT.json new file mode 100644 index 0000000000..bd3218eafa --- /dev/null +++ b/research/inplace-side-performance/RESULT.json @@ -0,0 +1,62 @@ +{ + "ai_assistance": "Substantial AI assistance for profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "baseline_seconds": [ + 16.747456939999665, + 17.098737376999907, + 17.06069083300008, + 16.890133087999857, + 17.154922305999662 + ], + "engines": { + "baseline": "research/inplace-side-performance/baseline.py", + "optimized": "scripts/experiments/inplace_side.py" + }, + "environment": { + "implementation": "CPython", + "isolated_host": false, + "os_caches_flushed": false, + "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": "scripts/experiments/inplace_side_witnesses.json", + "medians": { + "baseline": 17.06069083300008, + "optimized": 5.465907218000211, + "speedup": 3.121291700088902 + }, + "no_new_kappa": true, + "optimized_seconds": [ + 5.465907218000211, + 5.394471960999908, + 5.672483955000189, + 5.443477510999855, + 5.647890871000072 + ], + "receipt_fields_compared": [ + "all_internal_rational_frames_allowed", + "bad_endpoints", + "certified_nonorthogonal_paths", + "deficit_upper", + "disjoint_switches", + "excess_per_invocation_lower", + "h", + "n", + "no_positive_deficit", + "prefix_columns", + "scope" + ], + "rounds": 5, + "scope": "Fixed historical inplace-side prefix check on the three pinned witnesses (h=42,46,50). Not a selected-supplier cold replay or multiplication runtime.", + "source_sha256": { + "baseline.py": "4e7cb3df2e263f6c7f5907c55e3ee04c08926e6dbc984bbda1722a27b0a48ff6", + "scripts/experiments/inplace_side.py": "4397b84f3ac52554bf14303171410a2799af0bf8dae11ec64594bb5c011e93a2", + "scripts/experiments/inplace_side_witnesses.json": "90fe710f5daa35cc9e4892b29d712d66110b7b2b4c404da95a960ea7041618b9" + }, + "status": "PASS_IDENTICAL_INPLACE_PREFIX_RECEIPTS", + "witness_h": [ + 42, + 46, + 50 + ] +} diff --git a/research/inplace-side-performance/SOURCES.json b/research/inplace-side-performance/SOURCES.json new file mode 100644 index 0000000000..2bca1ca87e --- /dev/null +++ b/research/inplace-side-performance/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/inplace-side.json", + "usage": "provenance", + "git_blob": "8d3240c59c26c1839c2cf7a9b063fd30cbbe5a84", + "sha256": "1a2020c346e7d039e924a8c782dc6b3f0e94039eb1bec2b2644fc3de9d41ccdb" + }, + { + "path": "docs/research/inplace-side.md", + "usage": "provenance", + "git_blob": "a0bb57cacd27d7c2921f6060f59b42aeb1355311", + "sha256": "c228f131d95f3ea348455c13378c19ed6e3c75af7e14cf68ea0ada445ab3ac72" + }, + { + "path": "scripts/audit_inplace_side.py", + "usage": "provenance", + "git_blob": "2e9108178ee2e07d17f52d7cf79e079e91ba5feb", + "sha256": "16d295f9f9250d35f6f1de2843d5e13c7adbf88d595ebcd0b65b00d1a938acd9" + }, + { + "path": "scripts/experiments/inplace_side.py", + "usage": "provenance", + "git_blob": "db3de6f1d962ccc3a4eae31f83c72bba995ba44e", + "sha256": "4e7cb3df2e263f6c7f5907c55e3ee04c08926e6dbc984bbda1722a27b0a48ff6" + }, + { + "path": "scripts/experiments/inplace_side_witnesses.json", + "usage": "input", + "git_blob": "9d9970245a71705da7b84122a8be5b44755b5005", + "sha256": "90fe710f5daa35cc9e4892b29d712d66110b7b2b4c404da95a960ea7041618b9" + } + ] +} diff --git a/research/inplace-side-performance/TASK.json b/research/inplace-side-performance/TASK.json new file mode 100644 index 0000000000..20b167787e --- /dev/null +++ b/research/inplace-side-performance/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "1cd1f71746c2d200dd617bc3dd17d8a6", + "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 the historical inplace-side prefix checker (scripts/experiments/inplace_side.py:verify_prefix on the three pinned h=42/46/50 witnesses) be sped up without changing any receipt field, rejection condition or the regenerated certificates/inplace-side.json except its single source pin?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. The OS-random bit-mechanisms draw (seed 1cd1f71746c2d200dd617bc3dd17d8a6) was saturated on helper-contract/register-model work; expertise override selected verifier-engineering. Profiling make verify-certificates pointed at this fixed historical screen rather than isolated-test harness caching.", + "bottleneck_link": "Side result on review throughput: the inplace-side certificate is part of verify-certificates. A faster identical replay does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving verify_prefix change with frozen baseline, identical witness receipts, rejection/mutant controls, certificate pin discipline, registered replay and a measured before/after median. Do not reopen the mathematical rejection or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_INPLACE_SIDE_PREFIX_FAST via research/inplace-side-performance/verify.py (also under -O); PASS_IDENTICAL_INPLACE_PREFIX_RECEIPTS via benchmark.py; certificates/inplace-side.json differs from base only in the inplace_side.py source pin.", + "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": "Can the same least-unused scan replace sorted(unused) pivots inside compile_side without changing gate lists?", + "why_it_matters": "compile_side is not on the certificate hot path here, but shares the same lexicographic rule; unifying it would remove a second O(n log n) sort per column on small controls.", + "first_step": "Diff gate lists for h=6 and h=10 between set/sort and flag-scan compile_side, then time h=50 if identical.", + "blocked_by": "Out of this session's stop rule; not needed for the verify_prefix receipt claim." + }, + { + "question": "Should verify-certificates adopt a microbenchmark regression gate for this screen?", + "why_it_matters": "A future edit could restore sorted(unused) without failing equivalence tests.", + "first_step": "Decide whether RESULT.json medians belong in CI or remain descriptive.", + "blocked_by": "Maintainer CI-budget preference." + } + ] +} diff --git a/research/inplace-side-performance/VERIFY.json b/research/inplace-side-performance/VERIFY.json new file mode 100644 index 0000000000..4e9c95f5d1 --- /dev/null +++ b/research/inplace-side-performance/VERIFY.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/experiments/inplace_side.py", + "scripts/experiments/inplace_side_witnesses.json", + "scripts/audit_inplace_side.py", + "certificates/inplace-side.json", + "docs/research/inplace-side.md", + "tests/test_inplace_side.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact baseline copy of the base-commit source; identical verify_prefix receipts on all three pinned witnesses and small h=6/10 controls; shared rejection of reused switches, wrong prefixes and out-of-range switches; greatest-unused mutant rejected on every witness; certificates/inplace-side.json matches certificate() and differs from the base certificate only in the inplace_side.py source pin." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same equivalence and certificate discipline under -O (require() gates, not assert)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_inplace_side*.py", + "-v" + ], + "timeout_seconds": 180, + "checks": "Existing inplace-side unit tests plus focused performance-package controls." + } + ] +} diff --git a/research/inplace-side-performance/baseline.py b/research/inplace-side-performance/baseline.py new file mode 100644 index 0000000000..db3de6f1d9 --- /dev/null +++ b/research/inplace-side-performance/baseline.py @@ -0,0 +1,114 @@ +"""In-place binary side maps and exact disjoint-path excess witnesses. + +The rejection is scoped to lexicographic, smallest-row Gauss--Jordan, +exactly n side roles, retained invocation boundaries and central frames. +""" +from itertools import combinations +from fractions import Fraction as Q +from certify import require + + +def triple_side(h): + require(type(h) is int and h>=6 and h%2==0,'Use even h >= 6') + triples=list(combinations(range(h),3));n=len(triples);points=[0]*h + for i,S in enumerate(triples): + for p in S:points[p]|=1<>col&1) + unused.remove(p);pivots.append(p) + for i in range(n): + if i!=p and work[i]>>col&1:work[i]^=work[p];ops.append((i,p)) + require(set(work)=={1<>col&1) + require(p==expected,'Not the specified lexicographic elimination prefix') + unused.remove(p) + if col in at_step: + j=at_step[col] + require(rows[pivots[j]]>>col&1,'Claimed switch gate is absent') + verified.append((j,col)) + if col+1>col&1:rows[i]^=row + bad=[] + for j,p in enumerate(pivots): + target=pivots[partners[j]] if j in partners else p + if (masks[j]&masks[target]).bit_count()!=1:bad.append((j,target)) + k=len(bad) + # Each selected path contributes at least two units of edge excess in + # every invocation. The three n^2 copies give at least 6kn^2 extra. + deficit_upper=n*n*(n-6*h*h-6*k) + return dict(h=h,n=n,prefix_columns=len(pivots),disjoint_switches=len(swaps), + certified_nonorthogonal_paths=k,bad_endpoints=bad, + excess_per_invocation_lower=2*k,deficit_upper=deficit_upper, + no_positive_deficit=deficit_upper<=0, + all_internal_rational_frames_allowed=True, + scope='Fixed data-copy/injection boundaries, central frames, lexicographic elimination and exactly n side roles') + + +def invoke(x,y,side,center,code,inverse=False): + n=code['roles'];h=code['h'] + require(len(x)==len(y)==len(side)==n and len(center)==h,'Wrong role dimensions') + def mix(reverse=False): + for t,s in (reversed(code['gates']) if reverse else code['gates']):side[t]^=side[s] + def copy(): + for slot,i in enumerate(code['initial']):side[slot]^=x[i] + def inject(): + for i in range(n):y[i]^=side[i] + def gather(): + for i,T in enumerate(code['triples']): + for p in T:center[p]^=x[i] + def scatter(): + for i,T in enumerate(code['triples']): + for p in T:y[i]^=center[p] + ops=((mix,False),(inject,None),(mix,True),(scatter,None),(copy,None),(gather,None), + (scatter,None),(mix,False),(inject,None),(mix,True),(gather,None),(copy,None)) + if inverse:ops=tuple((f,not arg if f==mix else arg) for f,arg in reversed(ops)) + for f,arg in ops: + if f==mix:f(arg) + else:f() diff --git a/research/inplace-side-performance/benchmark.py b/research/inplace-side-performance/benchmark.py new file mode 100644 index 0000000000..91e6e7f4ea --- /dev/null +++ b/research/inplace-side-performance/benchmark.py @@ -0,0 +1,149 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timings for the three pinned witnesses. + +Timing is descriptive evidence for RESULT.json. Equivalence is enforced by +verify.py; this script fails only on unequal receipts or subprocess errors. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent + + +WORKER = r""" +import json, sys, time +from pathlib import Path +root = Path(sys.argv[1]) +engine = sys.argv[2] +sys.path.insert(0, str(root / "scripts")) +if engine == "baseline": + import importlib.util + path = root / "research/inplace-side-performance/baseline.py" + spec = importlib.util.spec_from_file_location("inplace_side_baseline", path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) +else: + from experiments import inplace_side as mod +witnesses = json.loads((root / "scripts/experiments/inplace_side_witnesses.json").read_text()) +t0 = time.perf_counter() +receipts = [mod.verify_prefix(w["h"], w["pivots"], w["swaps"]) for w in witnesses] +elapsed = time.perf_counter() - t0 +print(json.dumps({"elapsed": elapsed, "receipts": receipts})) +""" + + +def run_engine(engine: str) -> dict: + env = os.environ.copy() + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-B", "-c", WORKER, str(ROOT), engine], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + check=False, + ) + if proc.returncode != 0: + raise SystemExit(f"engine={engine} failed\n{proc.stderr}\n{proc.stdout}") + return json.loads(proc.stdout.strip().splitlines()[-1]) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--output", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args(argv) + require_rounds = args.rounds + if require_rounds < 1: + raise SystemExit("--rounds must be >= 1") + + baseline_samples = [] + optimized_samples = [] + reference = None + for round_index in range(require_rounds): + order = ("baseline", "optimized") if round_index % 2 == 0 else ("optimized", "baseline") + pair = {} + for engine in order: + payload = run_engine(engine) + if reference is None: + reference = payload["receipts"] + elif payload["receipts"] != reference: + raise SystemExit(f"receipt mismatch on round {round_index} engine={engine}") + pair[engine] = payload["elapsed"] + baseline_samples.append(pair["baseline"]) + optimized_samples.append(pair["optimized"]) + print( + f"round={round_index} order={order[0]}->{order[1]} " + f"baseline={pair['baseline']:.6f}s optimized={pair['optimized']:.6f}s", + flush=True, + ) + + base_med = statistics.median(baseline_samples) + opt_med = statistics.median(optimized_samples) + result = { + "status": "PASS_IDENTICAL_INPLACE_PREFIX_RECEIPTS", + "ai_assistance": ( + "Substantial AI assistance for profiling, implementation, packaging, " + "benchmarking and writing. Not independent human peer review." + ), + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "fixture": "scripts/experiments/inplace_side_witnesses.json", + "engines": { + "baseline": "research/inplace-side-performance/baseline.py", + "optimized": "scripts/experiments/inplace_side.py", + }, + "source_sha256": { + "baseline.py": sha256((PACKAGE / "baseline.py").read_bytes()).hexdigest(), + "scripts/experiments/inplace_side.py": sha256( + (ROOT / "scripts/experiments/inplace_side.py").read_bytes() + ).hexdigest(), + "scripts/experiments/inplace_side_witnesses.json": sha256( + (ROOT / "scripts/experiments/inplace_side_witnesses.json").read_bytes() + ).hexdigest(), + }, + "environment": { + "python": sys.version, + "platform": platform.platform(), + "implementation": platform.python_implementation(), + "os_caches_flushed": False, + "isolated_host": False, + }, + "rounds": require_rounds, + "baseline_seconds": baseline_samples, + "optimized_seconds": optimized_samples, + "medians": { + "baseline": base_med, + "optimized": opt_med, + "speedup": (base_med / opt_med) if opt_med else None, + }, + "receipt_fields_compared": sorted(reference[0].keys()) if reference else [], + "witness_h": [r["h"] for r in reference] if reference else [], + "scope": ( + "Fixed historical inplace-side prefix check on the three pinned witnesses " + "(h=42,46,50). Not a selected-supplier cold replay or multiplication runtime." + ), + "no_new_kappa": True, + } + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print( + f"PASS_IDENTICAL_INPLACE_PREFIX_RECEIPTS " + f"median_baseline={base_med:.6f}s median_optimized={opt_med:.6f}s " + f"speedup={base_med / opt_med:.3f}x output={args.output}" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/inplace-side-performance/verify.py b/research/inplace-side-performance/verify.py new file mode 100644 index 0000000000..6601138ed5 --- /dev/null +++ b/research/inplace-side-performance/verify.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and rejection controls for the faster inplace-side prefix check. + +Read-only by default. Regenerates no certificate unless --write-certificate is +passed. 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 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 +from prepare_layers import serializable # noqa: E402 +from audit_inplace_side import certificate as production_certificate # noqa: E402 +from experiments import inplace_side as production # noqa: E402 + + +BASE_COMMIT = "0b1cccf86e2f5132ed286a26ef0a681a495740ea" +ORIGINAL_BLOB = "db3de6f1d962ccc3a4eae31f83c72bba995ba44e" +ORIGINAL_SHA256 = "4e7cb3df2e263f6c7f5907c55e3ee04c08926e6dbc984bbda1722a27b0a48ff6" +BASE_CERTIFICATE_SHA256 = "1a2020c346e7d039e924a8c782dc6b3f0e94039eb1bec2b2644fc3de9d41ccdb" + + +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) + # baseline.py imports certify; scripts/ is already on sys.path + spec.loader.exec_module(module) + return module + + +def load_witnesses(): + return json.loads((SCRIPTS / "experiments/inplace_side_witnesses.json").read_text(encoding="utf-8")) + + +def load_base_certificate_bytes() -> bytes: + import subprocess + return subprocess.check_output(["git", "show", f"{BASE_COMMIT}:certificates/inplace-side.json"], cwd=ROOT) + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def compare_receipts(label: str, left: dict, right: dict) -> None: + require(left == right, f"{label}: receipts differ: {left!r} vs {right!r}") + + +def check_baseline_bytes() -> None: + baseline = PACKAGE / "baseline.py" + # Strip the package docstring/header added above the frozen body: compare the + # production historical blob to the functions by re-reading git. + import subprocess + original = subprocess.check_output(["git", "show", f"{BASE_COMMIT}:scripts/experiments/inplace_side.py"], cwd=ROOT) + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base inplace_side.py sha256 drift") + require( + subprocess.check_output(["git", "rev-parse", f"{BASE_COMMIT}:scripts/experiments/inplace_side.py"], cwd=ROOT) + .decode() + .strip() + == ORIGINAL_BLOB, + "base inplace_side.py blob drift", + ) + # baseline.py must match the original byte-for-byte after its own module docstring + # is the frozen original file itself. + require(baseline.read_bytes() == original, "baseline.py must be an exact copy of the base commit source") + + +def check_witness_equivalence(baseline, optimized) -> list[dict]: + witnesses = load_witnesses() + require([w["h"] for w in witnesses] == [42, 46, 50], "pinned witness set changed") + rows = [] + for witness in witnesses: + args = (witness["h"], witness["pivots"], witness["swaps"]) + old = baseline.verify_prefix(*args) + new = optimized.verify_prefix(*args) + compare_receipts(f"h={witness['h']}", old, new) + require(old["no_positive_deficit"] is True, f"h={witness['h']} deficit gate failed") + rows.append(old) + return rows + + +def check_small_controls(baseline, optimized) -> None: + for h in (6, 10): + code = optimized.compile_side(h) + require(code == baseline.compile_side(h), f"compile_side({h}) drifted") + old = baseline.verify_prefix(h, code["pivots"], []) + new = optimized.verify_prefix(h, code["pivots"], []) + compare_receipts(f"small h={h}", old, new) + + +def check_rejections(baseline, optimized) -> None: + code = optimized.compile_side(6) + pivots = code["pivots"] + + def expect_value_error(eng, name, args, needle): + try: + eng.verify_prefix(*args) + raise AssertionError(f"{name} accepted invalid input ({needle})") + except ValueError as exc: + require(needle.lower() in str(exc).lower(), f"{name} wrong rejection: {exc}") + + for eng, name in ((baseline, "baseline"), (optimized, "optimized")): + expect_value_error(eng, name, (6, pivots, [(0, 1), (0, 2)]), "reuse") + wrong = list(pivots) + wrong[0], wrong[1] = wrong[1], wrong[0] + expect_value_error(eng, name, (6, wrong, []), "prefix") + expect_value_error(eng, name, (6, pivots, [(0, len(pivots) + 1)]), "switch") + + +def greatest_unused_mutant_verify_prefix(h, pivots, swaps): + """Deliberate mutant: picks the greatest unused row instead of the least.""" + from experiments.inplace_side import triple_side + triples, points, rows = triple_side(h) + n = len(rows) + require(h % 4 == 2 and 0 < len(pivots) <= n, "Need an invertible side and nonempty prefix") + require(all(type(p) is int and 0 <= p < n for p in pivots) and len(set(pivots)) == len(pivots), + "Pivot roles must be distinct") + masks = [sum(1 << x for x in T) for T in triples] + partners = {} + at_step = {} + for j, c in swaps: + require(type(j) is int and type(c) is int and 0 <= j < c < len(pivots), "Invalid switch indices") + require(j not in partners and c not in partners, "Switch paths reuse a physical role") + partners[j] = c + partners[c] = j + at_step[c] = j + unused = [True] * n + for col, p in enumerate(pivots): + mask = 1 << col + expected = None + for i in range(n - 1, -1, -1): # MUTATION: greatest instead of least + if unused[i] and rows[i] & mask: + expected = i + break + require(expected is not None and p == expected, "Not the specified lexicographic elimination prefix") + unused[p] = False + if col in at_step: + j = at_step[col] + require(rows[pivots[j]] & mask, "Claimed switch gate is absent") + if col + 1 < len(pivots): + row = rows[p] + for i in range(n): + if i != p and rows[i] & mask: + rows[i] ^= row + bad = [] + for j, p in enumerate(pivots): + target = pivots[partners[j]] if j in partners else p + if (masks[j] & masks[target]).bit_count() != 1: + bad.append((j, target)) + k = len(bad) + deficit_upper = n * n * (n - 6 * h * h - 6 * k) + return dict(h=h, n=n, prefix_columns=len(pivots), disjoint_switches=len(swaps), + certified_nonorthogonal_paths=k, bad_endpoints=bad, + excess_per_invocation_lower=2 * k, deficit_upper=deficit_upper, + no_positive_deficit=deficit_upper <= 0, + all_internal_rational_frames_allowed=True, + scope="Fixed data-copy/injection boundaries, central frames, lexicographic elimination and exactly n side roles") + + +def check_mutant_rejected(baseline) -> None: + witnesses = load_witnesses() + # On the target witnesses the least and greatest unused rows differ, so the + # mutant must raise on the lexicographic prefix gate. + raised = 0 + for witness in witnesses: + try: + greatest_unused_mutant_verify_prefix(witness["h"], witness["pivots"], witness["swaps"]) + except Exception as exc: + require("lexicographic" in str(exc).lower() or "prefix" in str(exc).lower(), str(exc)) + raised += 1 + continue + # If it somehow returned, the receipt must not match the baseline. + raise AssertionError(f"mutant accepted witness h={witness['h']}") + require(raised == len(witnesses), "mutant failed to reject every witness") + # Positive small control still works on the true engines. + code = baseline.compile_side(6) + baseline.verify_prefix(6, code["pivots"], []) + + +def check_certificate(write: bool) -> dict: + result = production_certificate() + path = ROOT / "certificates/inplace-side.json" + text = json.dumps(serializable(result), indent=2, sort_keys=True) + "\n" + if write: + path.write_text(text, encoding="utf-8") + committed = path.read_text(encoding="utf-8") + require(committed == text, "working certificates/inplace-side.json does not match regenerated certificate()") + base = load_base_certificate_bytes() + require(sha256(base).hexdigest() == BASE_CERTIFICATE_SHA256, "base certificate sha256 drift") + old = json.loads(base.decode("utf-8")) + new = json.loads(committed) + # Only the production source pin for inplace_side.py may change. + old_pin = old["source_sha256"].pop("scripts/experiments/inplace_side.py") + new_pin = new["source_sha256"].pop("scripts/experiments/inplace_side.py") + require(old_pin == ORIGINAL_SHA256, "unexpected base pin") + require(new_pin == digest_file(SCRIPTS / "experiments/inplace_side.py"), "certificate pin != working source") + require(old == new, "certificate changed outside the single inplace_side.py source pin") + return result + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", action="store_true", + help="regenerate certificates/inplace-side.json (default: read-only compare)") + args = parser.parse_args(argv) + + check_baseline_bytes() + baseline = load_module(PACKAGE / "baseline.py", "inplace_side_baseline") + optimized = production + require(digest_file(SCRIPTS / "experiments/inplace_side.py") != ORIGINAL_SHA256, + "production source still equals the unoptimized base pin") + require(digest_file(PACKAGE / "baseline.py") == ORIGINAL_SHA256, + "baseline.py must equal the original source sha256") + + receipts = check_witness_equivalence(baseline, optimized) + check_small_controls(baseline, optimized) + check_rejections(baseline, optimized) + check_mutant_rejected(baseline) + cert = check_certificate(write=args.write_certificate) + + print( + "PASS_INPLACE_SIDE_PREFIX_FAST " + f"witnesses={len(receipts)} " + f"h={[r['h'] for r in receipts]} " + f"paths={[r['certified_nonorthogonal_paths'] for r in receipts]} " + f"optimize={sys.flags.optimize} " + f"certificate_source_pin={cert['source_sha256']['scripts/experiments/inplace_side.py'][:12]} " + "no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/experiments/inplace_side.py b/scripts/experiments/inplace_side.py index db3de6f1d9..4f5e7b3f61 100644 --- a/scripts/experiments/inplace_side.py +++ b/scripts/experiments/inplace_side.py @@ -51,6 +51,11 @@ def verify_prefix(h,pivots,swaps): swaps contains pairs of pivot COLUMN indices j>col&1) - require(p==expected,'Not the specified lexicographic elimination prefix') - unused.remove(p) + mask=1<>col&1,'Claimed switch gate is absent') + require(rows[pivots[j]]&mask,'Claimed switch gate is absent') verified.append((j,col)) if col+1>col&1:rows[i]^=row + if i!=p and rows[i]&mask:rows[i]^=row bad=[] for j,p in enumerate(pivots): target=pivots[partners[j]] if j in partners else p diff --git a/tests/test_inplace_side_performance.py b/tests/test_inplace_side_performance.py new file mode 100644 index 0000000000..d5b3f42408 --- /dev/null +++ b/tests/test_inplace_side_performance.py @@ -0,0 +1,86 @@ +"""Focused controls for the faster inplace-side prefix checker.""" +from hashlib import sha256 +from pathlib import Path +import importlib.util +import json +import sys +import unittest + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "scripts")) + +from experiments import inplace_side as optimized + + +ORIGINAL_SHA256 = "4e7cb3df2e263f6c7f5907c55e3ee04c08926e6dbc984bbda1722a27b0a48ff6" + + +def load_baseline(): + path = ROOT / "research/inplace-side-performance/baseline.py" + spec = importlib.util.spec_from_file_location("inplace_side_baseline", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +class InplaceSidePerformance(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.baseline = load_baseline() + cls.witnesses = json.loads( + (ROOT / "scripts/experiments/inplace_side_witnesses.json").read_text(encoding="utf-8") + ) + + def test_baseline_bytes_match_original_pin(self): + data = (ROOT / "research/inplace-side-performance/baseline.py").read_bytes() + self.assertEqual(sha256(data).hexdigest(), ORIGINAL_SHA256) + self.assertNotEqual( + sha256((ROOT / "scripts/experiments/inplace_side.py").read_bytes()).hexdigest(), + ORIGINAL_SHA256, + ) + + def test_witness_receipts_match_baseline_fieldwise(self): + self.assertEqual([w["h"] for w in self.witnesses], [42, 46, 50]) + for witness in self.witnesses: + args = (witness["h"], witness["pivots"], witness["swaps"]) + self.assertEqual( + optimized.verify_prefix(*args), + self.baseline.verify_prefix(*args), + ) + + def test_greatest_unused_mutant_rejects_target_witnesses(self): + path = ROOT / "research/inplace-side-performance/verify.py" + spec = importlib.util.spec_from_file_location("inplace_side_performance_verify", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + mutant = module.greatest_unused_mutant_verify_prefix + for witness in self.witnesses: + with self.assertRaises(ValueError): + mutant(witness["h"], witness["pivots"], witness["swaps"]) + + def test_certificate_only_source_pin_changes(self): + import subprocess + from audit_inplace_side import certificate + from prepare_layers import serializable + + base = json.loads( + subprocess.check_output( + ["git", "show", "0b1cccf86e2f5132ed286a26ef0a681a495740ea:certificates/inplace-side.json"], + cwd=ROOT, + ) + ) + regenerated = json.loads(json.dumps(serializable(certificate()))) + committed = json.loads((ROOT / "certificates/inplace-side.json").read_text(encoding="utf-8")) + self.assertEqual(committed, regenerated) + old_pin = base["source_sha256"].pop("scripts/experiments/inplace_side.py") + new_pin = regenerated["source_sha256"].pop("scripts/experiments/inplace_side.py") + self.assertEqual(old_pin, ORIGINAL_SHA256) + self.assertEqual( + new_pin, + sha256((ROOT / "scripts/experiments/inplace_side.py").read_bytes()).hexdigest(), + ) + self.assertEqual(base, regenerated) + + +if __name__ == "__main__": + unittest.main()