diff --git a/research/dirty-phase-row-products/README.md b/research/dirty-phase-row-products/README.md new file mode 100644 index 0000000000..ef6c416054 --- /dev/null +++ b/research/dirty-phase-row-products/README.md @@ -0,0 +1,173 @@ +# Fewer integer products in the complete dirty-phase replay + +This implementation was produced by Nick Petalas. It removes **255,310 +scalar products** from the complete scientific replay of Philipp / mightyOil's +[PR1294](https://github.com/CrocSwap/integer-mult-bounds/pull/1294). +Five alternating fresh-process pairs show a **17.87% local median wall-time +reduction**, with identical complete scientific stdout and zero failures. +Claim type: scoped implementation-preservation proof, exact finite conformance +and local performance evidence. No new mathematical identity or kappa is claimed. + +The opt-in adapter changes only `check_dense.multiply` in a private module. +The original symbolic checker, substitution loops, counterexamples, source +files, scientific receipts and six package tests remain intact. The +predecessor mathematics is the preserved workload, not new verification credit. + +## Implementation and proof + +For nonempty rectangular integer matrices A of size m by n and B of size n +by p, the original kernel evaluates every term in + + C[i,j] = sum_k A[i,k] B[k,j]. + +The new kernel allocates a zero m-by-p result, then visits each row i and +inner index k. If A[i,k] is nonzero, it adds A[i,k] times row k of B to +result row i. After processing inner indices less than k, the accumulator +is the corresponding partial sum. Terms with A[i,k]=0 contribute integer +zero. Induction on k proves equality of the complete matrices. Exact integer +addition permits the changed accumulation order. Both inputs remain unchanged +and each result row is fresh. The empty-output-row boundary is also preserved. + +The scalar-product count changes from m*n*p to p times the number of nonzero +entries of A. This is classical row expansion. Custom scalar objects, +floating-point arithmetic and malformed matrices are outside the contract. + +`adapter.py` authenticates all fourteen declared predecessor files by SHA256 +and Git-blob hash before compiling any predecessor module. It executes those +authenticated source bytes directly, without predecessor bytecode-cache reads +or scientific-result caching. Changed dependencies reject before scientific +execution. Each invocation loads fresh private modules and compares both +complete generated receipts with their authenticated originals. + +## Evidence + +The complete dense consumer reaches **16,294** multiplication calls across +26 shapes with dimensions at most eleven. The checking adapter compares every +new result against the original kernel and checks both inputs after both +calls. The old kernel enumerates 562,574 scalar products; the new kernel +enumerates 307,264. Their difference is exactly 255,310. These counts include +all direct matrices, normal-form substitutions and four invariant-removal +counterexamples of that consumer. + +Separate conformance covers all 6,561 pairs of two-by-two matrices with entries +in {-1,0,1}, 64 rectangular fixtures and the empty-output boundary, for **6,626** +cases. Sixteen source controls reject corruption of each of fourteen actual +inputs, a missing source and an unknown entry. Four arithmetic faults fail +explicit kernel fixtures; four additional well-shaped faulty kernels fail the +actual complete dense consumer. All six retained package tests run unchanged, +including relocation, source/receipt/order faults and exclusive output creation. +No assertion is needed for acceptance. + +Complete scientific JSON before its trailing newline has SHA256 +`7ab04e8ef093875f43f3d1240eb6bcf224c7d11f069eb7e40bfdc469e6cc9df1`. +The checking adapter also generates a digest of every reached input/output +triple and a shape histogram. Standalone verification prints a generated +receipt bound to every regular package file. No receipt is handwritten. + +## Complete scientific caller timing + +The timed boundary starts before launching a fresh CPython process and ends +after successful exit and captured output. Each process includes source +authentication, both module loads, the complete universal polynomial body, +the complete dense body, both expected-receipt comparisons and complete JSON +serialization. The six retained tests, new conformance tests, metadata checks, +shell startup and CI planning run separately. This does not claim a 17.87% +reduction of the whole generic registered-package job or a changed default +predecessor command. + +| Pair | Original kernel, seconds | Row expansion, seconds | +| --- | ---: | ---: | +| 1 | 0.075181084 | 0.060592416 | +| 2 | 0.074843250 | 0.061917208 | +| 3 | 0.074595417 | 0.062196792 | +| 4 | 0.075584708 | 0.061222917 | +| 5 | 0.074929500 | 0.061536584 | +| Median | 0.074929500 | 0.061536584 | + +The ranges are 0.074595417 to 0.075584708 seconds before and 0.060592416 to +0.062196792 seconds after. Every pair improves; the ranges are separated. +All ten outputs are byte-identical, with stdout SHA256 +`292f0080f85366a0fc96108216970c365fb6c0fd52913133c962eff14902b2ea`, +including the final newline. + +The machine runs macOS 27.0.1 arm64 and CPython 3.12.15, with eighteen logical +cores and entry load averages 2.10, 2.22 and 2.37. Other research processes were +present. Both sides use identical options and warm filesystem caches; module +state is fresh. An earlier five-pair pilot with the same kernel is excluded +from this final table. An untimed profile places 0.073 of 0.133 profiled seconds +in the original dense multiply. Python loops and integer arithmetic limit this +single-process caller. The measured reduction is smaller than that profiled +share; the profile itself is not a wall-time sample. + +`benchmark.py` reproduces the five-pair procedure and emits every duration, +failure count, complete-output digest, source hashes, program hashes and +environment. Timing is opt-in, with no CI threshold. + +## Reproduce + +From the contribution checkout root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dirty-phase-row-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/dirty-phase-row-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dirty-phase-row-products +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dirty-phase-row-products --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dirty-phase-row-products/benchmark.py +``` + +Another CPython 3.12 path may replace the local path. Expected markers are +`PASS_DIRTY_PHASE_ROW_PRODUCTS`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. Direct checks write only stdout. Retained file +fault tests use system temporary storage; set `TMPDIR` to a private external +directory when collecting evidence. Exported replay needs this package and +all fourteen declared inputs at their relative paths, but no Git or network. + +## Scope, sources and credit + +The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8, selected conditional PR6030. The replay-runtime card is refined +to this measured integer kernel. Current main, open and recent-account PRs, +merged object/general-kernel searches, active Discussions and local reservations +were checked before the +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363383). +Sparse historical notes and unpublished work remain coverage limits. + +Credit Philipp / mightyOil PR1294 for both complete scientific consumers, +identities, receipts, tests and original implementation; Charles Bethin PR1278 +for the interval proof and phase formulas; Hanson Sun PR1244/1085, Chafik +Boukhalfa PR628/905, Gareth Davidson PR877 and their retained lineage. Their +source and credit lines are unchanged. The new contribution is this concrete +implementation, preservation proof, conformance and complete-caller measurement. +Distributivity and sparse multiplication are classical. New work is Apache-2.0. + +Physical caller, rounded leaves, precision/tape, stock, compiler, supplier +admission and the complete multiplication theorem remain outside this result. +No selected cold replay, native suite, Lean or Docker run is needed or claimed. +The selected frontier and its five assumptions are unchanged. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +Should a maintained scientific replay adopt this integer kernel? Begin with +one named caller's profile, exact matrix contract and complete conformance. +This isolated package supplies no default adoption or selected-caller gain. +The structured first step and blocker are in `TASK.json`. + +## Verifier constraints + +New functions are below sixty lines. Fixed fixture domains bound every loop. +Caller dimensions are at most eleven; independent rectangular fixtures have +dimensions at most four. Fourteen source files are limited to one MiB each. +Five benchmark pairs have a thirty-second subprocess timeout. Registered +commands each have a 120-second outer bound. The unchanged retained six-test +suite invokes finite children without individual timeouts; the registered +runner's process-group deadline bounds that inherited path. + +Power of Ten rule 3 deviation: CPython allocates managed integers and containers. +Fixed domains and source sizes bound live collections; no fixed-allocation +runtime is claimed. Rule 8/9 deviation: authenticated compilation, `runpy` for +the local adapter, private replacement and the fixed unittest loader use dynamic +execution/dispatch. Targets are three named predecessor modules, this adapter +and the explicitly enumerated fault kernels. No source text is rewritten. +Warning-strict ordinary/optimized checks and source compilation supply +diagnostics. No standalone Python linter is installed in this environment. diff --git a/research/dirty-phase-row-products/SOURCES.json b/research/dirty-phase-row-products/SOURCES.json new file mode 100644 index 0000000000..b9938aa4c4 --- /dev/null +++ b/research/dirty-phase-row-products/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/universal-dirty-phase-identities/CERTIFICATE.json", + "usage": "input", + "git_blob": "40983343f6839cd98f60878ba5ebdbaaa74a23c2", + "sha256": "d7af9d33856ec45d4163bae1493abff2503664b58876210047491c5ba2c383af" + }, + { + "path": "research/universal-dirty-phase-identities/DENSE-CHECK.json", + "usage": "input", + "git_blob": "5c6d7295d199e72eaafbe8592d041218b5e67597", + "sha256": "43f23f4ba8cce04488662d0c0bc6595b688073420fbb89ad67c40a33670fff9d" + }, + { + "path": "research/universal-dirty-phase-identities/README.md", + "usage": "input", + "git_blob": "fdebc9c89099f0f59b2b1cc4353bc33786529011", + "sha256": "3620ec8ae93b66af22d9dff045a339ff75160b4e6c334518a01768dd69e6a0ea" + }, + { + "path": "research/universal-dirty-phase-identities/SOURCES.json", + "usage": "input", + "git_blob": "0d90ca139d061b286af584fbec5c5b8c3c629a9e", + "sha256": "167117bffb8c7587ee0bc676e37b45b9b345a00ae24502ad3a66ee664867d548" + }, + { + "path": "research/universal-dirty-phase-identities/TASK.json", + "usage": "input", + "git_blob": "a678d0ad03bc8dbe98c0abb89dc7d80117f89203", + "sha256": "94a9e1bb53d005c413564a91eeb42ce3bd611d4011ee2a6669f4945ab0c9677d" + }, + { + "path": "research/universal-dirty-phase-identities/VALIDATION.json", + "usage": "input", + "git_blob": "5abd00051e8d8d6b3dd513cd3238d36936f1502f", + "sha256": "493dafa182db67f1955d86a414a3090b4f9593da03a098c35f80898bf22ba04c" + }, + { + "path": "research/universal-dirty-phase-identities/VERIFY.json", + "usage": "input", + "git_blob": "58792a2654becf30f6fe2ab0bb75e2673db9f5ca", + "sha256": "d74193b96e897c9f231a0133b9d6ecec4f4e32d8bf138e18b13a9cba7a853011" + }, + { + "path": "research/universal-dirty-phase-identities/check_dense.py", + "usage": "input", + "git_blob": "cf04137c1bcf9a5a0c8df55174c2937d4fc2f177", + "sha256": "69629276352e02f335ea71af0c83608821d2c7ced315e4f4b522b48ebbb93740" + }, + { + "path": "research/universal-dirty-phase-identities/test_package.py", + "usage": "input", + "git_blob": "cc708f022848e27e37ed0cc59e449f93c693607c", + "sha256": "5116b9d96a9eccdc08c3e5db27207b2fedd0dfec8a4a77f4ea1e7d2b5d0c29a2" + }, + { + "path": "research/universal-dirty-phase-identities/vendor/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/universal-dirty-phase-identities/vendor/PR1278-NOTICE.md", + "usage": "input", + "git_blob": "b543c9e72463cb495ed380d5ded4c4235571483a", + "sha256": "e5d70a6492de305c914b1bd96b84506f6124c5fbfc3d09434ab241d1f4e2b438" + }, + { + "path": "research/universal-dirty-phase-identities/vendor/PR1278-PROOF.md", + "usage": "input", + "git_blob": "de9c8fca358c225e2ef30180c553717208015252", + "sha256": "17d346b53eb71780410e1ec5e87d56bc444215a540e98c84283f12553c0c81e9" + }, + { + "path": "research/universal-dirty-phase-identities/vendor/PR1278-README.md", + "usage": "input", + "git_blob": "01538b770abfbbca1ac753d9123aa8d0b5003e2a", + "sha256": "a05c0daa6ca62a8b619cfd8fbe38c1663b58ba7c258f9a40bdbb79b488fcf1fc" + }, + { + "path": "research/universal-dirty-phase-identities/verify.py", + "usage": "input", + "git_blob": "ac671f6a2ea28745b7dac50aa68cbf564b290b25", + "sha256": "3b440adcaa258585b064aeb05ce02ba171acc88c0021ed1ab0a245ccf6eeb15b" + } + ] +} diff --git a/research/dirty-phase-row-products/TASK.json b/research/dirty-phase-row-products/TASK.json new file mode 100644 index 0000000000..5cf775748b --- /dev/null +++ b/research/dirty-phase-row-products/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Remove zero-left-factor scalar products from the complete PR1294 scientific caller while preserving exact source-bound outputs and every retained package test.", + "scope_change_reason": "The generic replay-runtime card is refined to one measured dense integer multiplication consumer. This is implementation work, not a scientific audit.", + "bottleneck_link": "Shorter complete scientific replays reduce repeated checking costs without changing their evidence or the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified implementation improvement; do not optimize additional kernels.", + "outcome": "completed", + "evidence": "README.md; adapter.py; verify.py; benchmark.py. The standalone verifier generates a hash-bound receipt on stdout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Should an actual maintained replay adopt this integer multiplication kernel?", + "why_it_matters": "The opt-in implementation does not change the existing registered predecessor commands.", + "first_step": "Profile a named maintained consumer, verify its exact integer matrix contract and compare its complete command with this implementation.", + "blocked_by": "A separate adoption decision and caller-specific conformance are required." + } + ], + "ci_status": "pending" +} diff --git a/research/dirty-phase-row-products/VERIFY.json b/research/dirty-phase-row-products/VERIFY.json new file mode 100644 index 0000000000..982bf94448 --- /dev/null +++ b/research/dirty-phase-row-products/VERIFY.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-dirty-phase-identities/CERTIFICATE.json", + "research/universal-dirty-phase-identities/DENSE-CHECK.json", + "research/universal-dirty-phase-identities/README.md", + "research/universal-dirty-phase-identities/SOURCES.json", + "research/universal-dirty-phase-identities/TASK.json", + "research/universal-dirty-phase-identities/VALIDATION.json", + "research/universal-dirty-phase-identities/VERIFY.json", + "research/universal-dirty-phase-identities/check_dense.py", + "research/universal-dirty-phase-identities/test_package.py", + "research/universal-dirty-phase-identities/vendor/LICENSE", + "research/universal-dirty-phase-identities/vendor/PR1278-NOTICE.md", + "research/universal-dirty-phase-identities/vendor/PR1278-PROOF.md", + "research/universal-dirty-phase-identities/vendor/PR1278-README.md", + "research/universal-dirty-phase-identities/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 16294 reached products; complete primary/dense receipts; finite rectangular integer conformance; actual source and arithmetic corruptions; all six retained package tests." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete conformance and rejection checks with assertions disabled." + } + ] +} diff --git a/research/dirty-phase-row-products/adapter.py b/research/dirty-phase-row-products/adapter.py new file mode 100644 index 0000000000..ea8ca704e3 --- /dev/null +++ b/research/dirty-phase-row-products/adapter.py @@ -0,0 +1,102 @@ +"""Source-bound integer row products, produced by Nick Petalas. Apache-2.0.""" + +import argparse +import hashlib +import json +from pathlib import Path +from types import ModuleType + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/universal-dirty-phase-identities/" +MAX_BYTES = 1_048_576 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def bounded_read(path): + with path.open("rb") as stream: + raw = stream.read(MAX_BYTES + 1) + require(len(raw) <= MAX_BYTES, "input exceeds one MiB") + return raw + + +def source_bytes(root=ROOT): + manifest = json.loads(bounded_read(HERE / "SOURCES.json")) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(rows) == 14, "expected fourteen source inputs") + result = {} + for row in rows: + name = row["path"] + require(name.startswith(SOURCE) and ".." not in Path(name).parts, + "unexpected source path") + path = root / name + require(not path.is_symlink(), "source must be a regular file") + raw = bounded_read(path) + require(hashlib.sha256(raw).hexdigest() == row["sha256"], + "source SHA256 mismatch: " + name) + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == row["git_blob"], + "source Git blob mismatch: " + name) + require(name not in result, "duplicate source") + result[name] = raw + return result + + +def load_module(name, sources, root=ROOT): + require(name in ("verify", "check_dense", "test_package"), "unknown entry") + path = SOURCE + name + ".py" + module = ModuleType("retained_phase_" + name) + module.__file__ = str(root / path) + # Execute precisely the authenticated source bytes, bypassing .pyc reads. + exec(compile(sources[path], module.__file__, "exec"), module.__dict__) + return module + + +def multiply(a, b): + """Multiply the trusted nonempty rectangular integer matrices of the caller.""" + out = [[0] * len(b[0]) for _ in a] + for i, row in enumerate(a): + target = out[i] + for k, coefficient in enumerate(row): + if coefficient: + for j, value in enumerate(b[k]): + target[j] += coefficient * value + return out + + +def scientific(baseline=False, observer=None): + sources = source_bytes() + primary = load_module("verify", sources) + dense = load_module("check_dense", sources) + original = dense.multiply + if observer is not None: + dense.multiply = observer(original) + elif not baseline: + dense.multiply = multiply + results = [] + for module, receipt in ((primary, "CERTIFICATE.json"), + (dense, "DENSE-CHECK.json")): + result = module.run() + expected = json.loads(sources[SOURCE + receipt]) + require(canonical(result) == canonical(expected), "scientific receipt mismatch") + results.append(result) + return results + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--baseline", action="store_true") + args = parser.parse_args() + print(canonical(scientific(args.baseline)).decode()) + + +if __name__ == "__main__": + main() diff --git a/research/dirty-phase-row-products/benchmark.py b/research/dirty-phase-row-products/benchmark.py new file mode 100644 index 0000000000..68e4515b79 --- /dev/null +++ b/research/dirty-phase-row-products/benchmark.py @@ -0,0 +1,48 @@ +"""Fresh-process complete-caller timing, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import json +from pathlib import Path +import platform +import runpy +import statistics +import subprocess +import sys +import time +from types import SimpleNamespace + +adapter = SimpleNamespace(**runpy.run_path(str(Path(__file__).with_name("adapter.py")))) + + +def main(): + rows = [] + expected = adapter.canonical(adapter.scientific(baseline=True)) + b"\n" + for index in range(5): + row = {"pair": index + 1} + for name in ("baseline", "candidate"): + argv = [sys.executable, "-I", "-B", str(adapter.HERE / "adapter.py")] + if name == "baseline": + argv.append("--baseline") + start = time.perf_counter_ns() + process = subprocess.run(argv, capture_output=True, timeout=30) + elapsed = time.perf_counter_ns() - start + adapter.require(process.returncode == 0, process.stderr.decode(errors="replace")) + adapter.require(process.stdout == expected, "timed scientific output differs") + row[name + "_ns"] = elapsed + rows.append(row) + result = {"pairs": rows, "failures": 0, + "python": sys.version, "platform": platform.platform(), + "scientific_stdout_sha256": hashlib.sha256(expected).hexdigest(), + "source_sha256": {name: hashlib.sha256(raw).hexdigest() + for name, raw in adapter.source_bytes().items()}, + "program_sha256": {name: hashlib.sha256(adapter.bounded_read(adapter.HERE / name)).hexdigest() + for name in ("adapter.py", "benchmark.py")}} + for name in ("baseline", "candidate"): + samples = [row[name + "_ns"] for row in rows] + result[name] = {"median_ns": statistics.median(samples), + "min_ns": min(samples), "max_ns": max(samples)} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/dirty-phase-row-products/verify.py b/research/dirty-phase-row-products/verify.py new file mode 100644 index 0000000000..8ea7ec7dfa --- /dev/null +++ b/research/dirty-phase-row-products/verify.py @@ -0,0 +1,162 @@ +"""Complete consumer conformance, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import io +import itertools +import json +from pathlib import Path +import runpy +import shutil +import tempfile +from types import SimpleNamespace +import unittest + +adapter = SimpleNamespace(**runpy.run_path(str(Path(__file__).with_name("adapter.py")))) + + +def snapshot(matrix): + return tuple(map(tuple, matrix)) + + +def reached_conformance(): + counts = {"calls": 0, "old_products": 0, "new_products": 0} + shapes = {} + trace = hashlib.sha256() + + def observe(original): + def checked(a, b): + before = snapshot(a), snapshot(b) + expected = original(a, b) + actual = adapter.multiply(a, b) + adapter.require(actual == expected, "reached product mismatch") + adapter.require(before == (snapshot(a), snapshot(b)), "input was modified") + shape = (len(a), len(b), len(b[0])) + adapter.require(all(1 <= n <= 11 for n in shape), "unexpected caller size") + key = "x".join(map(str, shape)) + shapes[key] = shapes.get(key, 0) + 1 + counts["calls"] += 1 + counts["old_products"] += len(a) * len(b) * len(b[0]) + counts["new_products"] += sum(bool(x) for row in a for x in row) * len(b[0]) + trace.update(adapter.canonical([a, b, actual])) + return actual + return checked + + result = adapter.scientific(observer=observe) + adapter.require(counts == {"calls": 16294, "old_products": 562574, + "new_products": 307264}, "reached coverage changed") + return {**counts, "shapes": shapes, "trace_sha256": trace.hexdigest(), + "scientific_sha256": hashlib.sha256(adapter.canonical(result)).hexdigest()} + + +def finite_conformance(): + source = adapter.source_bytes() + reference = adapter.load_module("check_dense", source).multiply + matrices = [list(map(list, (values[:2], values[2:]))) + for values in itertools.product((-1, 0, 1), repeat=4)] + count = 0 + for a in matrices: + for b in matrices: + before = snapshot(a), snapshot(b) + adapter.require(adapter.multiply(a, b) == reference(a, b), "finite mismatch") + adapter.require(before == (snapshot(a), snapshot(b)), "finite input changed") + count += 1 + for rows, inner, columns in itertools.product(range(1, 5), repeat=3): + a = [[(i + 2 * k) % 5 - 2 for k in range(inner)] for i in range(rows)] + b = [[(3 * k - j) % 7 - 3 for j in range(columns)] for k in range(inner)] + adapter.require(adapter.multiply(a, b) == reference(a, b), "rectangular mismatch") + count += 1 + adapter.require(adapter.multiply([], [[1]]) == [], "empty-output boundary") + return count + 1 + + +def rejection_controls(): + rejected = 0 + sources = adapter.source_bytes() + with tempfile.TemporaryDirectory(prefix="dirty-phase-source-") as name: + root = Path(name) + shutil.copytree(adapter.ROOT / adapter.SOURCE, root / adapter.SOURCE, + ignore=shutil.ignore_patterns("__pycache__")) + for relative, original in sources.items(): + path = root / relative + path.write_bytes(original + b"\nchanged\n") + try: + adapter.source_bytes(root) + except ValueError as error: + adapter.require("mismatch" in str(error), "wrong source rejection") + rejected += 1 + else: + raise ValueError("changed source accepted") + path.write_bytes(original) + (root / (adapter.SOURCE + "verify.py")).unlink() + try: + adapter.source_bytes(root) + except FileNotFoundError: + rejected += 1 + else: + raise ValueError("missing source accepted") + try: + adapter.load_module("unknown", sources) + except ValueError: + rejected += 1 + else: + raise ValueError("unknown entry accepted") + return rejected + + +def kernel_controls(): + # Each real arithmetic fault must disagree on a concrete supported input. + fixtures = [([[-2]], [[3]]), ([[0, 1]], [[5], [7]]), + ([[1, 2]], [[3, 4], [5, 6]]), ([[1]], [[-1]])] + wrong = [lambda a, b: [[0]], + lambda a, b: [[a[0][0] * b[0][0]]], + lambda a, b: [[sum(a[0][k] * b[j][k] for k in range(2)) + for j in range(2)]], + lambda a, b: [[abs(a[0][0] * b[0][0])]]] + for fault, (a, b) in zip(wrong, fixtures, strict=True): + adapter.require(fault(a, b) != adapter.multiply(a, b), "kernel fault hidden") + complete_faults = [ + lambda a, b: [[0 for _ in row] for row in adapter.multiply(a, b)], + lambda a, b: [[-x for x in row] for row in adapter.multiply(a, b)], + lambda a, b: adapter.multiply([[max(x, 0) for x in row] for row in a], b), + lambda a, b: [row[::-1] for row in adapter.multiply(a, b)], + ] + for fault in complete_faults: + try: + adapter.scientific(observer=lambda original: fault) + except ValueError as error: + adapter.require("dense normal-form disagreement" in str(error), + "wrong complete-consumer rejection") + else: + raise ValueError("faulty complete consumer accepted") + return len(wrong) + len(complete_faults) + + +def retained_tests(): + sources = adapter.source_bytes() + module = adapter.load_module("test_package", sources) + suite = unittest.defaultTestLoader.loadTestsFromModule(module) + stream = io.StringIO() + result = unittest.TextTestRunner(stream=stream, verbosity=2).run(suite) + adapter.require(result.wasSuccessful() and result.testsRun == 6, + "retained package tests failed:\n" + stream.getvalue()) + return result.testsRun + + +def main(): + reached = reached_conformance() + baseline = adapter.scientific(baseline=True) + candidate = adapter.scientific() + adapter.require(adapter.canonical(baseline) == adapter.canonical(candidate), + "complete scientific output differs") + result = {"status": "PASS_DIRTY_PHASE_ROW_PRODUCTS", "reached": reached, + "finite_cases": finite_conformance(), + "source_rejections": rejection_controls(), + "kernel_rejections": kernel_controls(), "retained_tests": retained_tests()} + paths = sorted(adapter.HERE.iterdir()) + result["package_sha256"] = {p.name: hashlib.sha256(adapter.bounded_read(p)).hexdigest() + for p in paths if p.is_file()} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()