From e72837b58f04bbbb7414402062a2f8db3e3a0b0f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 00:11:03 +0000 Subject: [PATCH] perf(research): speed up complete quinary replay by 33.75% --- research/quinary-forward-rank/README.md | 204 +++++++++++++++++++++ research/quinary-forward-rank/SOURCES.json | 54 ++++++ research/quinary-forward-rank/TASK.json | 89 +++++++++ research/quinary-forward-rank/VERIFY.json | 39 ++++ research/quinary-forward-rank/adapter.py | 143 +++++++++++++++ research/quinary-forward-rank/benchmark.py | 64 +++++++ research/quinary-forward-rank/verify.py | 124 +++++++++++++ 7 files changed, 717 insertions(+) create mode 100644 research/quinary-forward-rank/README.md create mode 100644 research/quinary-forward-rank/SOURCES.json create mode 100644 research/quinary-forward-rank/TASK.json create mode 100644 research/quinary-forward-rank/VERIFY.json create mode 100644 research/quinary-forward-rank/adapter.py create mode 100644 research/quinary-forward-rank/benchmark.py create mode 100644 research/quinary-forward-rank/verify.py diff --git a/research/quinary-forward-rank/README.md b/research/quinary-forward-rank/README.md new file mode 100644 index 0000000000..554f24adfd --- /dev/null +++ b/research/quinary-forward-rank/README.md @@ -0,0 +1,204 @@ +# Faster complete characteristic-five disjointness replay + +An optional forward-echelon evaluator reduces the median time of the complete +composed PR5221 scientific replay by **33.75%** on the recorded host. Both +scientific command bodies execute in full, with identical combined stdout, +every reached rank call and the original typed receipt retained. This is a +scoped implementation-equivalence proof and a measured runtime improvement. +The characteristic-five repair theorem remains Brian / JoyboyBrian's result. +No new mathematical repair rank, supplier or kappa is claimed. + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Change and execution boundary + +The primary verifier in [PR5221](https://github.com/CrocSwap/integer-mult-bounds/pull/5221) +computes reduced row echelon form and returns only its rank. The new evaluator +normalizes each pivot and eliminates rows below it, updating only the remaining +row suffix. Eliminating above each pivot is unnecessary for the returned rank. + +`adapter.py` authenticates all six declared source inputs before compiling any +source. In adapted mode it renames exactly one source definition from `rank` +to `frozen_rank` and supplies `forward_rank` under the original name. The +entire remainder of the primary source, including its `__main__` block, is +unchanged. The independent command is compiled and executed without edits. +Compilation uses authenticated source text directly, without importing source +bytecode. The frozen predecessor files are never modified. + +The complete composed consumer runs the primary body and independent body +sequentially in one fresh Python process. The same wrapper, authentication, +compilation, imports, fixture construction, output capture and checking are +inside both timed modes. Original mode executes the original rank definition. +Adapted mode uses the new evaluator. This measures the complete scientific +consumer, including the independent check. It does not measure the shared +package runner, CI planning, or the sum of two separately started interpreters. + +The two unchanged output lines are: + +```text +PASS_QUINARY_RESONANT_DISJOINTNESS_REPAIR +PASS_INDEPENDENT_QUINARY_TENSOR_AND_KERNEL +``` + +The combined output SHA256 is +`e2c64edfb1e54f877f32e061452239b97cd8493be02017bdafc156e901f2d0a8`. +The original typed `RESULT.json` remains checked by both source bodies. +All five Jordan rules, both literal source fixtures, endpoint witnesses, +domain controls, direct-binomial powers, similarity and kernel census remain. +Their mathematical claims retain predecessor credit and are not new results +of this package. + +## Equivalence proof + +The new function accepts rectangular integer matrices with at most 256 rows +and columns and entries of at most 64 bits, over F5. Empty matrices and +zero-column matrices have rank zero. Every reached source argument lies in +this domain. The function copies and reduces the entries before any update. + +At the start of column c, let r be the number of selected pivots. The remaining +rows have zero entries in every column before c. This invariant holds initially. +If the column has no pivot among those rows, it is zero there; advancing c +preserves the invariant. Otherwise swap a nonzero pivot to row r, multiply +that row by its inverse and eliminate its column from all rows below it. +These are invertible row operations over F5. The earlier entries of all +affected rows are zero, so updating only the suffix gives exactly the same +row operation as updating the whole row. The invariant follows for the next +column and r increases by one. + +The selected pivot rows are linearly independent, with distinct leading +columns. At termination every remaining row is zero, or every row has a pivot. +Thus the matrix rank is exactly r. Clearing entries above a pivot changes no +rank and is unnecessary for this conclusion. Both evaluators consequently +return the mathematical rank on the stated domain. Neither modifies its input. +Since no other source code consumes the intermediate echelon matrix, replacing +the rank return value preserves every downstream scientific check. + +## Evidence + +`verify.py` compares both complete output strings and observes every reached +adapted call. All **28** calls agree with the original evaluator, and each +input remains unchanged. The largest reached matrix is 254 by 254. A separate +oracle using one-entry and two-by-two minors checks every one of the **15,625** +two-by-three matrices over F5. Their rank histogram is `[1,744,14880]`. +There are another **89** boundary/rectangular cases, including negative +entries, row swaps, zero dimensions and the 256-dimensional identity. +Eleven rejection controls cover invalid fields, shapes, types and capacities, +changed source bytes and a missing rewrite anchor. Explicit guards survive +optimized Python. Each run generates a receipt from actual checks and the +SHA256 of all seven package files and six source inputs; no receipt is +handwritten or committed. + +An untimed cProfile run of the original primary reports 0.209 seconds in its +28 rank calls out of 0.242 seconds total. Profiling is excluded from timings. +The largest exact row reduction is the measured limiter. Keeping forward +elimination and the unchanged construction and independent work explains why +the whole consumer is not twice as fast. + +After adding a bounded source-file read, the five final pairs below alternate +original then adapted, each in a fresh process. +Times include full source authentication and both scientific bodies. The +host is CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. Load averages +were `(4.34,3.94,3.06)` before measurement and +`(2.1128,3.5083,3.1260)` after the final measurement. Other processes were +present; no claim of an idle host is made. There were zero command failures +or output disagreements. + +| Pair | Original seconds | Adapted seconds | +| --- | ---: | ---: | +| 1 | 0.288796625 | 0.190406375 | +| 2 | 0.283317125 | 0.187691209 | +| 3 | 0.282368625 | 0.185105083 | +| 4 | 0.282861833 | 0.184945250 | +| 5 | 0.285454292 | 0.194998125 | + +Medians are **0.283317125** and **0.187691209** seconds. Ranges are +`[0.282368625,0.288796625]` and `[0.184945250,0.194998125]` seconds. +The median reduction is 33.75%; the ranges are disjoint. This is local +evidence for this complete fixed consumer, not a portable performance guarantee +or a faster multiplication algorithm. Optimization stopped at this first +verified improvement. + +## Reproduction + +From the repository root, with the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/quinary-forward-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/quinary-forward-rank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/quinary-forward-rank +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/quinary-forward-rank --check-source-history +``` + +Expected markers are `PASS_QUINARY_FORWARD_RANK`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Any CPython 3.12 path can replace the local interpreter path. The direct +verifier also works in a Git-free export with its declared inputs. + +To repeat measurements, create an external directory, choose a fresh output +filename, and use: + +```sh +python3.12 -W error -B research/quinary-forward-rank/benchmark.py --rounds 5 --output /absolute/external/directory/measurements.json +``` + +The benchmark requires five to fifteen alternating pairs, checks exact +stdout/stderr and status, bounds every child at thirty seconds, removes its +private bytecode namespace and writes measurements exclusively outside the +checkout. Direct `adapter.py --mode original` and `--mode adapted` execute +the corresponding complete composed consumer without the conformance oracle. + +## Scope and implementation constraints + +This is an optional isolated adapter. Default adoption and historical pin +migration are not implemented. General coefficient fields, unbounded matrix +sizes, rounded arithmetic and intermediate echelon outputs are outside its +interface. The scientific predecessor law and complete multiplication theorem +are not independently reviewed here. Native maps, a physical caller, ownership, +restoration, routing, precision/tape, stock, compiler and outer admission remain +separate. Lean, Docker, heavy native builds and the selected scientific cold +replay were not run. No selected record or predecessor file changes. +Independent human and formal proof-kernel review are unclaimed. + +All new functions are under sixty lines, with bounded matrix, fixture, file and +process domains. There is no recursion or persistent cache. CPython's managed +allocation is a Power-of-Ten rule 3 deviation; the evaluator holds at most +256 by 256 entries plus one row suffix, with bounded input integer sizes. +Sources are at most one MiB each. Rule 8/9 deviations are authenticated source +compilation and the two named evaluator callbacks used by conformance. Their +targets and source hashes are fixed; all source and output checks propagate +failures. Standard-library internals allocate and dispatch dynamically. +The inherited source's fixed loops and containers remain unchanged and are +not exposed to user-selected dimensions. Warning-strict normal and optimized +registered checks provide recurring Python diagnostics. + +The first five pairs before that boundary guard also had zero errors and +identical output, with medians 0.288851667 and 0.192588875 seconds and disjoint +ranges. The final run above measures the published implementation. + +## Provenance + +Scientific base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8, selected PR6030. The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362961) +states this exact runtime scope. `TASK.json` retains the original runtime card +and refinement. `SOURCES.json` pins every live source at the base. Live open +and account PRs, handoffs and active Discussions, current-main README searches, +merged/general-form searches and the cached card scan supplied overlap +coverage. Sparse notes, arbitrary historical diffs and unpublished work are +not exhaustively covered. PR6135 concerns DisjointTensor DAG serialization, +a different compiler and consumer; this is not its follow-up. + +## Open next questions + +Can the evaluator be adopted in the default consumer while preserving +historical source pins? First specify the migration and retain both complete +scientific bodies and the typed receipt. Default integration is the remaining +blocker. No further optimization is reserved. + +## Credit + +Credit Brian / JoyboyBrian's PR5221 for the entire law, primary and independent +consumer, typed receipt, controls and source structure. Retain Ali Romman +PR4962, Nick Petalas PR5173, mikey1201 PR172, icekylinx PR144 and the complete +tensor/deletion lineage. Gaussian elimination is classical. The new contribution +is the source-bound implementation step, equivalence argument and measured +complete-consumer evidence. diff --git a/research/quinary-forward-rank/SOURCES.json b/research/quinary-forward-rank/SOURCES.json new file mode 100644 index 0000000000..d0e40da6c7 --- /dev/null +++ b/research/quinary-forward-rank/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/boolean-disjointness-repair/PROOF.txt", + "usage": "input", + "git_blob": "96b0e770da33660eff812df8b74302b15c557e59", + "sha256": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427" + }, + { + "path": "research/quinary-resonant-disjointness-repair/RESULT.json", + "usage": "input", + "git_blob": "cc5c1eaab65873a31a31e3a0cf9963e82313ee62", + "sha256": "daaab01765def2717cd24a06deaf8c741933d82abdf5a1b414ae6286f541c0d7" + }, + { + "path": "research/quinary-resonant-disjointness-repair/SOURCES.json", + "usage": "input", + "git_blob": "4cf09e79fd5316c33927024fd5e28b1e010e36b4", + "sha256": "26a46f85f6cd439bd38b3c47f3e10d5c559ca4ce7c5c50c9a940d448e535bb9b" + }, + { + "path": "research/quinary-resonant-disjointness-repair/independent.py", + "usage": "input", + "git_blob": "4f1d1900f98ff1a44c3a6b9980d669d7151e221d", + "sha256": "b1307e6c97f739c778fcff96a1e2d768aa6e6322e22c1346810f157832d7b0d4" + }, + { + "path": "research/quinary-resonant-disjointness-repair/verify.py", + "usage": "input", + "git_blob": "8bf8c2b5be11b5a2ef5542d6c7546a2c44d7a43e", + "sha256": "3110c867528e5b15bd21042d86468dc21e0af6bec50fe7febd70f40cc2e9067c" + }, + { + "path": "research/ternary-disjointness-repair/PROOF.md", + "usage": "input", + "git_blob": "680e0adb269a3cd3420c2fe2312bea99c4b76ded", + "sha256": "43d61f2c7ea623e6a39783b486c12c8edea62197a2ae2512a4e4f9596f8920e0" + } + ] +} diff --git a/research/quinary-forward-rank/TASK.json b/research/quinary-forward-rank/TASK.json new file mode 100644 index 0000000000..d111cb0848 --- /dev/null +++ b/research/quinary-forward-rank/TASK.json @@ -0,0 +1,89 @@ +{ + "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": "An opt-in forward-echelon rank evaluator for the unchanged complete PR5221 characteristic-five disjointness replay, retaining both primary and independent scientific command bodies.", + "scope_change_reason": "The runtime card is narrowed to the measured row-reduction bottleneck in one fully source-bound consumer; no mathematical theorem is re-audited.", + "bottleneck_link": "Implementation side result: less elapsed time for the same complete scientific replay, without new supplier credit or a kappa claim.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified complete-consumer improvement, with exact conformance, five alternating fresh-process pairs and unchanged scientific output.", + "outcome": "completed", + "evidence": "README.md equivalence proof; verifier checks all 28 reached rank calls, all 15625 F5 2x3 matrices, 89 boundaries and 11 rejection controls. Five alternating fresh-process pairs have zero errors, identical output and nonoverlapping ranges.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this rank-only implementation be adopted in the default consumer while preserving historical source pins?", + "why_it_matters": "Would make the faster path available without the optional adapter.", + "first_step": "Specify the source-pin migration and retain the full primary/independent workload and typed receipt.", + "blocked_by": "Default integration and historical pin migration are not supplied by this isolated package." + } + ], + "claim_type": "scoped implementation-equivalence proof and measured replay-time improvement", + "coordination": { + "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/5221", + "source_author": "JoyboyBrian", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362961" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "freshness": { + "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_at_utc": "2026-11-03T00:10:21.601392+00:00", + "selected_pr": 6030, + "decision": "Canonical main, guidance and source pins unchanged; continue verified isolated runtime result." + }, + "overlap": "Live open/account PRs, last-hour handoffs and active Discussions; cached runtime card scan; current-main formula/object and merged/general searches. PR5221 supplies this consumer. PR6135 optimizes a distinct DisjointTensor serialization consumer. Arbitrary historical diffs, sparse notes and unpublished work are not exhaustively covered.", + "overlap_coverage": { + "local_notes": 8917, + "local_head_inventory_complete": true, + "open_prs": 407, + "open_prs_fetched_at": "2026-11-03T00:01:22.430953+00:00", + "discussions": 6360, + "discussions_fetched_at": "2026-11-03T00:02:35.604126+00:00", + "manual_delta": "Open PR list, merged PR5221 search and last30 handoffs refreshed before commitment; no competing same-consumer optimization." + } +} diff --git a/research/quinary-forward-rank/VERIFY.json b/research/quinary-forward-rank/VERIFY.json new file mode 100644 index 0000000000..1535e47220 --- /dev/null +++ b/research/quinary-forward-rank/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/boolean-disjointness-repair/PROOF.txt", + "research/quinary-resonant-disjointness-repair/RESULT.json", + "research/quinary-resonant-disjointness-repair/SOURCES.json", + "research/quinary-resonant-disjointness-repair/independent.py", + "research/quinary-resonant-disjointness-repair/verify.py", + "research/ternary-disjointness-repair/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both complete scientific command bodies, all reached rank calls and inputs, exhaustive F5 minor oracle, boundary and invalidation controls, generated source/package-hash receipt" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete coverage and explicit guards with Python assertions disabled" + } + ] +} diff --git a/research/quinary-forward-rank/adapter.py b/research/quinary-forward-rank/adapter.py new file mode 100644 index 0000000000..896115298c --- /dev/null +++ b/research/quinary-forward-rank/adapter.py @@ -0,0 +1,143 @@ +"""Source-bound forward elimination for the complete PR5221 replay.""" + +import argparse +import contextlib +import hashlib +import io +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/quinary-resonant-disjointness-repair/" +INPUTS = ( + SOURCE + "verify.py", + SOURCE + "independent.py", + SOURCE + "RESULT.json", + SOURCE + "SOURCES.json", + "research/boolean-disjointness-repair/PROOF.txt", + "research/ternary-disjointness-repair/PROOF.md", +) +MAX_BYTES = 2**20 +MAX_DIMENSION = 256 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bounded(path): + with path.open("rb") as stream: + data = stream.read(MAX_BYTES + 1) + require(len(data) <= MAX_BYTES, "source too large") + return data + + +def forward_rank(matrix, p=5): + """Return F5 rank without modifying a bounded rectangular integer matrix.""" + require(type(p) is int and p == 5, "coefficient field must be F5") + require(isinstance(matrix, (list, tuple)), "matrix must be a sequence") + rows = len(matrix) + require(rows <= MAX_DIMENSION, "too many rows") + require(all(isinstance(row, (list, tuple)) for row in matrix), "invalid row") + cols = len(matrix[0]) if rows else 0 + require(cols <= MAX_DIMENSION, "too many columns") + require(all(len(row) == cols for row in matrix), "ragged matrix") + require( + all(type(x) is int and x.bit_length() <= 64 for row in matrix for x in row), + "entries must be bounded integers", + ) + a = [[x % p for x in row] for row in matrix] + rank = 0 + for col in range(cols): + pivot = next((i for i in range(rank, rows) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + inverse = pow(a[rank][col], -1, p) + require(a[rank][col] * inverse % p == 1, "pivot inverse") + a[rank][col:] = [x * inverse % p for x in a[rank][col:]] + tail = a[rank][col + 1 :] + for i in range(rank + 1, rows): + q = a[i][col] + if q: + a[i][col] = 0 + a[i][col + 1 :] = [ + (x - q * y) % p for x, y in zip(a[i][col + 1 :], tail) + ] + rank += 1 + if rank == rows: + break + return rank + + +def authenticate(): + manifest_bytes = read_bounded(PACKAGE / "SOURCES.json") + manifest = json.loads(manifest_bytes) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(rows) == len(INPUTS), "source inventory size") + require({row["path"] for row in rows} == set(INPUTS), "source inventory") + payloads = {} + for row in rows: + path = row["path"] + data = read_bounded(ROOT / path) + check_digest(data, row["sha256"]) + payloads[path] = data + return payloads + + +def check_digest(data, expected): + require(hashlib.sha256(data).hexdigest() == expected, "source bytes changed") + + +def primary_text(payloads, mode): + require(mode in ("original", "adapted"), "unknown replay mode") + source = payloads[SOURCE + "verify.py"].decode("utf-8") + needle = "def rank(a,p=5):" + require(source.count(needle) == 1, "rank definition anchor") + if mode == "adapted": + source = source.replace(needle, "def frozen_rank(a,p=5):", 1) + return source + + +def run_complete(mode, observe=False): + """Execute both full frozen commands and return their exact combined stdout.""" + payloads = authenticate() + source = primary_text(payloads, mode) + records = [] + namespace = {"__name__": "__main__", "__file__": str(ROOT / INPUTS[0])} + + def checked_rank(matrix, p=5): + before = [list(row) for row in matrix] + got = forward_rank(matrix, p) + expected = namespace["frozen_rank"](matrix, p) + require(got == expected, "reached rank disagreement") + require(matrix == before, "reached rank input mutation") + records.append((len(matrix), len(matrix[0]) if matrix else 0, got)) + return got + + namespace["rank"] = checked_rank if observe else forward_rank + require(not observe or mode == "adapted", "observation requires adapted mode") + output = io.StringIO() + with contextlib.redirect_stdout(output): + exec(compile(source, str(ROOT / INPUTS[0]), "exec"), namespace) + independent = payloads[INPUTS[1]].decode("utf-8") + second = {"__name__": "__main__", "__file__": str(ROOT / INPUTS[1])} + exec(compile(independent, str(ROOT / INPUTS[1]), "exec"), second) + text = output.getvalue() + require(len(text) <= MAX_BYTES, "replay output too large") + return text, records + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mode", choices=("original", "adapted"), required=True) + args = parser.parse_args() + output, records = run_complete(args.mode) + require(not records, "unexpected observation") + print(output, end="") + + +if __name__ == "__main__": + main() diff --git a/research/quinary-forward-rank/benchmark.py b/research/quinary-forward-rank/benchmark.py new file mode 100644 index 0000000000..80d76affea --- /dev/null +++ b/research/quinary-forward-rank/benchmark.py @@ -0,0 +1,64 @@ +"""Alternate complete original/adapted commands in fresh CPython processes.""" + +import argparse +import hashlib +import json +import os +import platform +from pathlib import Path +import statistics +import subprocess +import sys +import tempfile +import time + +from adapter import PACKAGE, ROOT, require + + +def sample(mode, temporary): + env = dict(os.environ) + env["PYTHONPYCACHEPREFIX"] = str(temporary / mode) + command = [sys.executable, "-W", "error", "-B", str(PACKAGE / "adapter.py"), + "--mode", mode] + start = time.perf_counter_ns() + result = subprocess.run(command, capture_output=True, env=env, timeout=30, check=False) + elapsed = time.perf_counter_ns() - start + require(result.returncode == 0, "replay failed: " + result.stderr.decode()) + require(not result.stderr, "unexpected replay stderr") + expected = (b"PASS_QUINARY_RESONANT_DISJOINTNESS_REPAIR\n" + b"PASS_INDEPENDENT_QUINARY_TENSOR_AND_KERNEL\n") + require(result.stdout == expected, "incomplete scientific output") + return {"mode": mode, "seconds": elapsed / 10**9, + "stdout_sha256": hashlib.sha256(result.stdout).hexdigest(), "errors": 0} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + require(5 <= args.rounds <= 15, "round count must be 5..15") + output = args.output.resolve() + require(not output.is_relative_to(ROOT), "measurements must stay outside checkout") + require(output.parent.is_dir() and not output.exists(), "exclusive output required") + samples = [] + with tempfile.TemporaryDirectory(prefix="rank-benchmark-", dir=output.parent) as name: + for _ in range(args.rounds): + for mode in ("original", "adapted"): + samples.append(sample(mode, Path(name))) + summary = {} + for mode in ("original", "adapted"): + values = [row["seconds"] for row in samples if row["mode"] == mode] + summary[mode] = {"median_seconds": statistics.median(values), + "range_seconds": [min(values), max(values)]} + report = {"python": sys.version, "platform": platform.platform(), + "cpu_count": os.cpu_count(), "load_average": os.getloadavg(), + "rounds": args.rounds, "samples": samples, "summary": summary, + "errors": sum(row["errors"] for row in samples)} + with output.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(report, indent=2, sort_keys=True) + "\n") + print(json.dumps(summary, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/quinary-forward-rank/verify.py b/research/quinary-forward-rank/verify.py new file mode 100644 index 0000000000..dc31f5e0d2 --- /dev/null +++ b/research/quinary-forward-rank/verify.py @@ -0,0 +1,124 @@ +"""Finite conformance for an implementation change, not a new repair theorem.""" + +import hashlib +import itertools +import json + +from adapter import ( + INPUTS, + PACKAGE, + SOURCE, + authenticate, + check_digest, + forward_rank, + primary_text, + require, + run_complete, +) + + +def rank_two_rows(matrix): + if not any(x % 5 for row in matrix for x in row): + return 0 + for j, k in itertools.combinations(range(3), 2): + if (matrix[0][j] * matrix[1][k] - matrix[0][k] * matrix[1][j]) % 5: + return 2 + return 1 + + +def exhaustive_small(): + histogram = [0, 0, 0] + for entries in itertools.product(range(5), repeat=6): + matrix = [list(entries[:3]), list(entries[3:])] + before = [row[:] for row in matrix] + expected = rank_two_rows(matrix) + require(forward_rank(matrix) == expected, "minor oracle disagreement") + require(matrix == before, "small input changed") + histogram[expected] += 1 + require(sum(histogram) == 5**6, "exhaustive domain") + return histogram + + +def edge_cases(payloads): + namespace = {"__name__": "source_fixture", "__file__": str(PACKAGE / "unused")} + exec(compile(primary_text(payloads, "original"), "frozen-primary", "exec"), namespace) + matrices = [[], [[]], [[], []], [[0]], [[-5]], [[-1]], [[0, 1], [1, 0]]] + for rows in range(1, 10): + for cols in range(1, 10): + matrices.append([[(i * j + i + 3 * j) % 7 - 3 for j in range(cols)] + for i in range(rows)]) + for matrix in matrices: + require(forward_rank(matrix) == namespace["rank"](matrix), "boundary rank") + require(forward_rank([[int(i == j) for j in range(256)] for i in range(256)]) + == 256, "dimension limit") + return len(matrices) + 1 + + +def controls(payloads): + rejected = [] + bad_inputs = ( + ("field", [[1]], 3), + ("field type", [[1]], True), + ("matrix type", None, 5), + ("row type", [1], 5), + ("ragged", [[1], []], 5), + ("entry type", [[True]], 5), + ("entry size", [[2**65]], 5), + ("row limit", [[0]] * 257, 5), + ("column limit", [[0] * 257], 5), + ) + for name, matrix, p in bad_inputs: + try: + forward_rank(matrix, p) + except ValueError: + rejected.append(name) + else: + raise ValueError("invalid matrix accepted: " + name) + try: + check_digest(payloads[INPUTS[0]] + b"\n", hashlib.sha256(payloads[INPUTS[0]]).hexdigest()) + except ValueError: + rejected.append("source mutation") + else: + raise ValueError("changed source accepted") + changed = dict(payloads) + changed[SOURCE + "verify.py"] = b"def other(): pass\n" + try: + primary_text(changed, "adapted") + except ValueError: + rejected.append("definition anchor") + else: + raise ValueError("missing definition accepted") + require(forward_rank([[0, 1], [1, 0]]) == 2, "row swap required") + require(forward_rank([[1, 1], [2, 2]]) == 1, "dependent row required") + return rejected + + +def main(): + payloads = authenticate() + original, empty = run_complete("original") + adapted, records = run_complete("adapted", observe=True) + require(not empty and len(records) == 28, "complete reached rank inventory") + require(original == adapted, "complete scientific output changed") + require(original.splitlines() == ["PASS_QUINARY_RESONANT_DISJOINTNESS_REPAIR", + "PASS_INDEPENDENT_QUINARY_TENSOR_AND_KERNEL"], "complete markers") + histogram = exhaustive_small() + boundaries = edge_cases(payloads) + rejected = controls(payloads) + files = sorted(p for p in PACKAGE.iterdir() if p.is_file()) + require(len(files) == 7, "package inventory") + receipt = { + "claim_type": "implementation equivalence and measured runtime improvement", + "reached_rank_calls": records, + "small_matrix_rank_histogram": histogram, + "boundary_cases": boundaries, + "rejected_controls": rejected, + "complete_output_sha256": hashlib.sha256(original.encode()).hexdigest(), + "source_sha256": {p: hashlib.sha256(b).hexdigest() for p, b in payloads.items()}, + "package_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in files}, + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_QUINARY_FORWARD_RANK") + + +if __name__ == "__main__": + main()