From dc7d0f681a7b326b475863074c825f9824d21a80 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 22:25:47 +0000 Subject: [PATCH] feat(research): skip settled columns in encoded Gaussian inverse --- .../gaussian-inverse-settled-columns/PROOF.md | 111 ++++++++++++++ .../README.md | 135 +++++++++++++++++ .../SOURCES.json | 48 ++++++ .../TASK.json | 80 ++++++++++ .../VERIFY.json | 40 +++++ .../benchmark.py | 57 +++++++ .../checks.py | 99 ++++++++++++ .../inverse.py | 81 ++++++++++ .../physical.py | 143 ++++++++++++++++++ .../verify.py | 34 +++++ 10 files changed, 828 insertions(+) create mode 100644 research/gaussian-inverse-settled-columns/PROOF.md create mode 100644 research/gaussian-inverse-settled-columns/README.md create mode 100644 research/gaussian-inverse-settled-columns/SOURCES.json create mode 100644 research/gaussian-inverse-settled-columns/TASK.json create mode 100644 research/gaussian-inverse-settled-columns/VERIFY.json create mode 100644 research/gaussian-inverse-settled-columns/benchmark.py create mode 100644 research/gaussian-inverse-settled-columns/checks.py create mode 100644 research/gaussian-inverse-settled-columns/inverse.py create mode 100644 research/gaussian-inverse-settled-columns/physical.py create mode 100644 research/gaussian-inverse-settled-columns/verify.py diff --git a/research/gaussian-inverse-settled-columns/PROOF.md b/research/gaussian-inverse-settled-columns/PROOF.md new file mode 100644 index 0000000000..8632696887 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/PROOF.md @@ -0,0 +1,111 @@ +# Exact inverse refinement and its resource boundary + +This scoped proof and implementation were produced by Nick Petalas. +The Gauss-Jordan algorithm and its identity-column invariant are classical. +Jose Manuel / jmbarrancoml, PR3851, supplies the exact encoded implementation +to which this refinement applies. Its Gaussian construction is a cited +premise, not a result audited here. New work is Apache-2.0. + +## Contract + +Take a positive-dimensional square exact rational `Matrix` accepted by the +retained no-pivot inverse. Each successive pivot must be positive. Matrix +entries are canonical reduced rational records. Numerical payloads and +indices use the retained encoded tape operations; fixture construction and +final checking are separate host boundaries. Sufficient scratch leases for +the stated extra counts are required; a pool sized only for the original +peak is not promised to suffice. + +The candidate starts from the same `[A | I]`, uses the same normalization +and elimination arithmetic, checks each pivot at the same point, and copies +the same final right block. It changes only the column iterator in the two +row-operation loops from `[0,2n)` to `[k,2n)` at pivot `k`. + +## Equality of states and accepted domain + +Before pivot `k`, the first `k` columns of the augmented matrix equal the +first `k` columns of `I`. This holds vacuously at zero. In particular every +entry `(k,j)` with `j=k`, in identical order. Column `k` +becomes the `k`th identity column. Induction proves both the invariant and +bit-identical augmented matrix contents after every completed pivot. + +The next pivot is therefore identical, including its sign and reduced +representation. A nonpositive pivot rejects in both implementations. A +nonsquare matrix rejects before augmentation in both. The iterator's +extra order guard always holds, since `0<=k0`, because +eliminating one pivot changes `c` to `nc/(n+c)>0`. The already processed +rows have the same nonzero coefficient on every unprocessed column; +their common coefficient begins positive and updates by multiplication +by `n/(n+c)>0`. Thus every off-diagonal factor is nonzero and `m_k=n-1`. +Every pivot is positive. This proves attainment in every dimension. + +For `n=4`, this is the literal fixture `4I+J`. The physical checker measures +236 versus 212 matrix reads and 80 writes on each side. Its separate +rational trace derives the 24 omitted reads rather than assuming density. + +## Costs not hidden by the read count + +The suffix iterator additionally owns a cursor and a length while the +retained iterator owns its own index and remaining counter. These are +encoded `O(log n)`-bit counts, closed after each finite traversal. The +candidate does not claim a universal reduction in every tape operation, +wall time or scratch capacity. + +For the complete `4I+J` fixture, including input construction, decoding, +and final pool cleanup, the retained pool's own meters report + +```text + baseline candidate +record reads 947301 922401 +record writes 187399 182739 +unit head moves 869032 846336 +peak pool leases 34 36 +``` + +These are actual finite pooled-record-tape counters. They are not a +complete machine instruction count or a supplier invoice. In particular +the two extra peak leases are paid explicitly. Both runs execute under +`sealed_constructors` and disallow host payload decoding during inversion. +All returned source records agree and all pool tapes are blank at return. + +Cold-process measurements include source hash authentication, extraction, +imports, input construction, inversion, output consumption and cleanup. +They do not establish a runtime improvement. The written theorem is the +all-dimension semantics and matrix-read refinement; finite checks alone +do not prove it universally. Native all-column validity, numerical +Gaussian admission, production pages and a complete multiplication caller +remain outside this result. diff --git a/research/gaussian-inverse-settled-columns/README.md b/research/gaussian-inverse-settled-columns/README.md new file mode 100644 index 0000000000..5baf03c1d2 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/README.md @@ -0,0 +1,135 @@ +# Skip settled columns in encoded Gaussian inverse setup + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped semantics/resource proof with exact finite corroboration. +The exact positive-pivot inverse of Jose Manuel's +[PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851) +can omit reads of its completed identity columns. At pivot k, with m_k +nonzero off-diagonal elimination factors, the exact saving is + +```text +sum k(1+m_k) matrix reads, +between n(n-1)/2 and n^2(n-1)/2, both sharp. +``` + +The candidate performs identical rational arithmetic and matrix writes, +returns identical encoded output and preserves the positive-pivot numerical +domain. It requires additional scratch. [PROOF.md](PROOF.md) gives the +all-dimension invariant, sharp examples and resource boundary. No new kappa +or selected-frontier change is claimed. + +For the literal physical 4-by-4 matrix `4I+J`, where J is all ones: + +| Measured complete finite workload | Retained inverse | Candidate | +| --- | ---: | ---: | +| Matrix reads during inversion | 236 | 212 | +| Matrix writes during inversion | 80 | 80 | +| Pooled tape reads | 947301 | 922401 | +| Pooled tape writes | 187399 | 182739 | +| Pooled unit head moves | 869032 | 846336 | +| Peak pool leases | 34 | 36 | + +The pooled counters include input construction, output decoding and final +cleanup. They include the suffix iterator's extra scratch operations. They +are finite record-tape counters, not a complete machine instruction count +or recursive supplier invoice. A pool sized only for the original peak +need not suffice. The first checked improvement is shipped without further +optimization. + +## Evidence and reproduction + +The new checker executes ten paired physical fixtures, checks every output +against a separate rational trace and both inverse products, and confirms +the exact read reduction and unchanged writes. Eight executions reject +nonsquare, singular, zero-pivot and negative-pivot inputs with the same +messages and cleanup. Another 81 rational matrices corroborate the identity +invariant. All checks use explicit exceptions and survive optimized Python. +The inversion itself runs under sealed constructors and a host-decoding ban. + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-inverse-settled-columns/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-inverse-settled-columns/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-inverse-settled-columns +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-inverse-settled-columns --check-source-history --check-modes +``` + +Other hosts may substitute their CPython 3.12 path. The direct checker writes +no files and prints a generated receipt bound to every package file. It +authenticates all five live inputs before importing the retained physical +runtime. An official package export includes those inputs and supports a +Git-free replay; full history is needed only for the repository provenance +checks. No predecessor scientific verifier is imported or replayed. + +## Cold runtime limit + +Run the separate benchmark with + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-inverse-settled-columns/benchmark.py --pairs 9 +``` + +Nine alternating fresh-process pairs on macOS arm64, CPython 3.12.15, +give medians 0.928621375 seconds retained and 0.922816875 seconds candidate. +Their ranges are 0.917676334 to 1.030556625 seconds and 0.909664875 to +0.998733333 seconds. All eighteen complete output byte strings agree and +there are zero errors. This comparison is inconclusive: the median gap is +smaller than the observed variation. No wall-time speedup is claimed. + +The timed region includes authentication, nested export extraction, imports, +fixture construction, inversion, literal output checking and cleanup. A +separate profile of the same 4-by-4 workload places the retained inversion +at 0.703 of 1.532 profiled seconds; `Matrix.get` accounts for 0.189 seconds. Authentication and +extraction dominate this tiny cold workload. The host has eighteen logical +CPUs, and other processes were active. Alternating sides limits drift but +does not remove contention. Neither side uses result caching or a changed +fixture. Timing is not a CI acceptance threshold. + +## Open next questions + +The structured questions and blockers are in [TASK.json](TASK.json). + +1. Can one exact streamed row update reduce complete tape work without + increasing peak scratch? First specify every borrowed record, scan and + cleanup operation. No such primitive or cost proof is supplied here. +2. Does this inverse improve a complete reached Gaussian preparation? + First compare an actual preparation page, its full output bytes, + ownership and pooled meters. Production pages and a full caller + benchmark were not run. + +## Credit, scope and implementation limits + +Jose Manuel / jmbarrancoml retains PR3851's physical Gaussian setup, +positive-pivot rational inverse, encoded tape operations and word-product +lineage. Chafik Boukhalfa, RaD/hipotures, Mason Hale, Dugongue and the +retained arithmetic, Gaussian and multiplication contributors retain their +source credit. Existing files and attribution are unchanged. Gauss-Jordan +elimination and its identity-column argument are classical; the new result +is their checked physical read-count refinement in this exact implementation. + +The canonical base is `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority +revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279747) +and [TASK.json](TASK.json) record the original question and bounded overlap +coverage. Direct live PR/Discussion and main-tree searches supplement the +helper's incomplete sparse local coverage. Unpublished work and arbitrary +historical code diffs are outside that search. + +The source Gaussian theorem is cited rather than audited. Native all-column, +numerical Gaussian admission, production preparation, precision/tape/stock, +complete caller and all five selected framework assumptions remain open. +No selected scientific cold replay, Lean or Docker run was performed. +Independent human and formal proof-kernel review are unclaimed. + +Power of Ten inspection covers the five new Python files. Functions are +under sixty lines; numerical loops are bounded by matrix dimension and +fixtures by width four. The 81-matrix host domain and at most fifteen +benchmark pairs are explicit. Subprocesses have sixty-second timeouts. +Source files are capped at 128 MiB and the manifest at 64 KiB and sixteen +rows. Recursion and runtime code generation are absent from new code. +Managed Python allocation is a rule-3 deviation; inherited tape buffers +also allocate dynamically, so no fixed-storage implementation is claimed. +The two engine choices, source loader, fixture constructor and temporary +instrumentation are bounded indirect calls, a rule-9 deviation. Strict +warnings and normal/optimized replays are the available local diagnostics. diff --git a/research/gaussian-inverse-settled-columns/SOURCES.json b/research/gaussian-inverse-settled-columns/SOURCES.json new file mode 100644 index 0000000000..eb87ec1e28 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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/physical-gaussian-core/gaussian_matrix.py", + "usage": "input", + "git_blob": "fc41183a42f5e1af5ea2294c295a0519abbcdb6c", + "sha256": "5bb982c6f36083b646bd5a5ab2ea4059c203fa0cc824e9f28132c0f323824bac" + }, + { + "path": "research/physical-gaussian-core/gaussian_rationals.py", + "usage": "input", + "git_blob": "053404d91c1bef0d4bb0f6647491847bf5879aaf", + "sha256": "6f9a380c8c7b4233c3bc338a6206d65cc85bee2e4f5625c2a212065f04f4b73d" + }, + { + "path": "research/physical-gaussian-core/gaussian_sources.py", + "usage": "input", + "git_blob": "ce521f91997775e189f984ba7dd68a15bf9ecd9b", + "sha256": "c5889a97a11a9c6c6c44deb8a2042498ddc3f55703de15269132b8f198e24b15" + }, + { + "path": "research/physical-gaussian-core/inputs/branchfree-source.tar", + "usage": "input", + "git_blob": "48dc77f5145d649bfed6745e38ab18b11772d597", + "sha256": "e6cdacd59a067189a99bfe03f4448913bb8d518ed4a9b1d981a68c5c666529c7" + }, + { + "path": "research/physical-gaussian-core/inputs/word-export.tar", + "usage": "input", + "git_blob": "885794cf3328941209034ee2d946ed76dbea8ce3", + "sha256": "d428e8b6aef4d348fa2e922ca64c4cfd634bbb2f0c150033273e65fcf4600b49" + } + ] +} diff --git a/research/gaussian-inverse-settled-columns/TASK.json b/research/gaussian-inverse-settled-columns/TASK.json new file mode 100644 index 0000000000..51e5b732e6 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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": "Skip settled leading identity columns in the exact encoded Gaussian inverse; prove the read-count saving and test the complete finite physical boundary.", + "scope_change_reason": "This is an encoded preparation component used by Gaussian replays. Cold runtime measurements are reported even when inconclusive; the proved improvement is matrix-read count.", + "bottleneck_link": "Fewer exact setup scans can reduce preparation work for physical Gaussian experiments. This component does not alter the recursive paid invoice or supply a new kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact read-count improvement, with the full scratch tradeoff and measured cold-command limits; do not extend the optimizer.", + "outcome": "completed", + "evidence": "Written all-dimension read-count refinement; ten paired physical fixtures, 81 rational matrices and eight rejecting executions. Dense dimension four saves 24 of 236 matrix reads and reduces each pooled-tape meter at a two-lease peak cost. Cold runtime comparison is inconclusive.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a row-streaming inverse reduce complete tape work without increasing peak scratch?", + "why_it_matters": "The present suffix cursor saves reads but uses two extra peak leases.", + "first_step": "Specify one exact batched row update and charge every stream scan and cleanup.", + "blocked_by": "No such physical update or complete cost proof is supplied." + }, + { + "question": "Does replacing the setup inverse improve a complete Gaussian preparation on a reached caller?", + "why_it_matters": "Source authentication dominates the cold tiny inversion command; a component improvement is not an end-to-end speedup.", + "first_step": "Pin one actual preparation page and compare complete bytes, ownership and pooled meters.", + "blocked_by": "No production-size preparation or full caller benchmark was run." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279747", + "source_predecessor": { + "pr": 3851, + "author": "jmbarrancoml", + "role": "Exact encoded positive-pivot inverse and physical Gaussian setup; cited construction, not audited." + }, + "freshness": { + "canonical_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "priority_revision": 8, + "selected_kappa": "0.003125804", + "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "overlap_limits": "Cached snapshot covers 338 open PRs and 5959 Discussion records; sparse local coverage is incomplete. Direct live PR/Discussion and main README searches supplement it. Unpublished work and arbitrary historical diffs are not covered." + } +} diff --git a/research/gaussian-inverse-settled-columns/VERIFY.json b/research/gaussian-inverse-settled-columns/VERIFY.json new file mode 100644 index 0000000000..678803d35a --- /dev/null +++ b/research/gaussian-inverse-settled-columns/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-gaussian-core/gaussian_matrix.py", + "research/physical-gaussian-core/gaussian_rationals.py", + "research/physical-gaussian-core/gaussian_sources.py", + "research/physical-gaussian-core/inputs/branchfree-source.tar", + "research/physical-gaussian-core/inputs/word-export.tar" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Ten paired encoded inverse fixtures, 81 exact rational matrices, literal two-sided inverse identities, source preservation, scratch cleanup, exact saved reads, full pooled meters and eight same-domain rejection executions." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical explicit conformance and rejection checks with assertions disabled." + } + ] +} diff --git a/research/gaussian-inverse-settled-columns/benchmark.py b/research/gaussian-inverse-settled-columns/benchmark.py new file mode 100644 index 0000000000..a9319f2e72 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/benchmark.py @@ -0,0 +1,57 @@ +"""Alternate complete cold commands; timings are evidence, not CI thresholds.""" +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent + + +def measure(engine, fixture): + command = [sys.executable, "-I", "-W", "error", "-B", str(HERE / "verify.py"), + "--workload", "--engine", engine, "--fixture", fixture] + started = time.perf_counter_ns() + result = subprocess.run(command, capture_output=True, check=True, timeout=60) + elapsed = time.perf_counter_ns() - started + if result.stderr: + raise ValueError("unexpected benchmark diagnostics") + output = json.loads(result.stdout) + if len(output["output"]) != int(fixture[-1]) or output["counts"] != {"get": 0, "set": 0}: + raise ValueError("incomplete or instrumented benchmark workload") + return elapsed, sha256(result.stdout).hexdigest() + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--fixture", choices=("dense3", "dense4"), default="dense4") + parser.add_argument("--pairs", type=int, choices=range(5, 16), default=9) + args = parser.parse_args() + rows = [] + for pair in range(args.pairs): + order = ("baseline", "candidate") if pair % 2 == 0 else ("candidate", "baseline") + for engine in order: + elapsed, digest = measure(engine, args.fixture) + rows.append({"pair": pair, "engine": engine, "elapsed_ns": elapsed, "stdout_sha256": digest}) + if len({row["stdout_sha256"] for row in rows}) != 1: + raise ValueError("benchmark output disagreement") + summary = {} + for engine in ("baseline", "candidate"): + samples = [row["elapsed_ns"] for row in rows if row["engine"] == engine] + summary[engine] = {"median_ns": statistics.median(samples), "min_ns": min(samples), + "max_ns": max(samples), "runs": len(samples)} + paths = sorted(HERE.glob("*.py")) + [HERE / "SOURCES.json"] + source_hashes = {p.name: sha256(p.read_bytes()).hexdigest() for p in paths} + print(json.dumps({"fixture": args.fixture, "rows": rows, "summary": summary, + "errors": 0, "outputs_equal": True, "python": sys.version, + "platform": platform.platform(), "cpu_count": os.cpu_count(), + "source_hashes": source_hashes}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/gaussian-inverse-settled-columns/checks.py b/research/gaussian-inverse-settled-columns/checks.py new file mode 100644 index 0000000000..4ddc69e8c3 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/checks.py @@ -0,0 +1,99 @@ +"""New inverse conformance, exact read accounting, and domain controls.""" +from fractions import Fraction as Q +from itertools import product +from physical import fixture, require, run_case + + +def saved_reads(matrix): + """A separate rational trace counts nonzero elimination factors.""" + n = len(matrix) + a = [[Q(v) for v in row] + [Q(int(i == j)) for j in range(n)] + for i, row in enumerate(matrix)] + savings = 0 + for k in range(n): + pivot = a[k][k] + require(pivot > 0, "positive trace pivot") + a[k] = [v / pivot for v in a[k]] + factors = [a[i][k] for i in range(n) if i != k] + savings += k * (1 + sum(v != 0 for v in factors)) + for i in range(n): + if i == k: + continue + factor = a[i][k] + a[i] = [x - factor * y for x, y in zip(a[i], a[k])] + require(all(a[i][j] == int(i == j) for i in range(n) for j in range(k + 1)), + "completed identity-column invariant") + return savings, [row[n:] for row in a] + + +def host_corroboration(): + cases = 0 + for entries in product(range(-1, 2), repeat=4): + matrix = [[Q(4 + entries[0]), Q(entries[1])], + [Q(entries[2]), Q(4 + entries[3])]] + savings, inverse = saved_reads(matrix) + require(savings in (1, 2), "two-row exact savings range") + identity(matrix, inverse) + cases += 1 + return cases + + +def identity(matrix, inverse): + n = len(matrix) + require(len(inverse) == n and all(len(row) == n for row in inverse), "full output shape") + for i in range(n): + for j in range(n): + require(sum(matrix[i][k] * inverse[k][j] for k in range(n)) == int(i == j), + "literal right inverse identity") + require(sum(inverse[i][k] * matrix[k][j] for k in range(n)) == int(i == j), + "literal left inverse identity") + + +def physical_corroboration(): + matrices = [[[Q(int(i == j)) for j in range(n)] for i in range(n)] for n in range(1, 5)] + matrices += [fixture(name) for name in ("dense3", "dense4", "rational3")] + matrices += [[[Q(1, 3), Q(0)], [Q(0), Q(7, 5)]], + [[Q(1), Q(0), Q(0)], [Q(-2), Q(1), Q(0)], [Q(3), Q(4), Q(1)]], + [[Q(2), Q(3)], [Q(1), Q(2)]]] + evidence = [] + for matrix in matrices: + baseline = run_case("baseline", matrix, True) + candidate = run_case("candidate", matrix, True) + savings, expected = saved_reads(matrix) + require(baseline["output"] == candidate["output"], "complete physical output equality") + actual = [[Q(v) for v in row] for row in candidate["output"]] + require(actual == expected, "independent rational output") + identity(matrix, actual) + require(baseline["counts"]["get"] - candidate["counts"]["get"] == savings, + "exact matrix-read savings") + require(baseline["counts"]["set"] == candidate["counts"]["set"], "same matrix writes") + if matrix == fixture("dense4"): + require(all(candidate["counts"]["pooled_tape"][key] < baseline["counts"]["pooled_tape"][key] + for key in ("reads", "writes", "moves")), "paid pooled-tape improvement") + require(candidate["counts"]["pool_peak"] == baseline["counts"]["pool_peak"] + 2, + "two extra peak scratch leases are charged") + evidence.append({"matrix": [[str(v) for v in row] for row in matrix], + "baseline": baseline, "candidate": candidate, "saved_reads": savings}) + return evidence + + +def rejecting_controls(): + cases = [([[Q(0)]], "positive exact setup pivot"), + ([[Q(-1)]], "positive exact setup pivot"), + ([[Q(1), Q(1)], [Q(1), Q(1)]], "positive exact setup pivot"), + ([[Q(1), Q(0), Q(0)], [Q(0), Q(1), Q(0)]], "square exact inverse")] + for matrix, message in cases: + for engine in ("baseline", "candidate"): + try: + run_case(engine, matrix) + except ValueError as error: + require(str(error) == message, "same boundary rejection and cleanup") + else: + raise ValueError("missing physical inverse rejection") + return 2 * len(cases) + + +def run(): + physical = physical_corroboration() + return {"physical_fixtures": physical, "host_matrices": host_corroboration(), + "domain_rejections": rejecting_controls(), "status": "PASS_GAUSSIAN_INVERSE_SETTLED_COLUMNS"} diff --git a/research/gaussian-inverse-settled-columns/inverse.py b/research/gaussian-inverse-settled-columns/inverse.py new file mode 100644 index 0000000000..751ee4ab69 --- /dev/null +++ b/research/gaussian-inverse-settled-columns/inverse.py @@ -0,0 +1,81 @@ +"""Skip proved identity columns in the physical Gaussian setup inverse. + +Derived from Jose Manuel's PR3851 gaussian_matrix.inverse, Apache-2.0. +The suffix traversal and its resource proof were produced by Nick Petalas. +""" +from contextlib import closing +from cardinal_counts import Count +from encoded import compare, subtract +from gaussian_matrix import Matrix +from gaussian_rationals import Rational +from router_metadata import indices, owned +from words import need + + +def suffix_indices(start, stop): + """Borrow endpoints and yield an owned encoded cursor on [start, stop).""" + need(compare(start, stop) <= 0, "ordered inverse column interval") + with owned(Count(start), subtract(stop, start)) as (cursor, length): + for _ in indices(length): + yield cursor + cursor.increment() + + +def normalize(augmented, k, pivot): + with closing(suffix_indices(k, augmented.columns)) as columns: + for j in columns: + with owned(augmented.get(k, j)) as (previous,): + if previous.numerator.magnitude.zero(): + continue + with owned(previous.over(pivot)) as (value,): + augmented.set(k, j, value) + + +def eliminate(augmented, k, dimension): + for i in indices(dimension): + if compare(i, k) == 0: + continue + with owned(augmented.get(i, k)) as (factor,): + if factor.numerator.magnitude.zero(): + continue + with closing(suffix_indices(k, augmented.columns)) as columns: + for j in columns: + with owned(augmented.get(k, j)) as (source,): + if source.numerator.magnitude.zero(): + continue + with owned(augmented.get(i, j)) as (previous,): + with owned(factor.times(source)) as (product,): + with owned(previous.minus(product)) as (value,): + augmented.set(i, j, value) + + +def inverse(matrix): + """Same positive-pivot contract and exact result as PR3851's inverse.""" + need(compare(matrix.rows, matrix.columns) == 0, "square exact inverse") + dimension = matrix.rows + + def entry(i, j): + if compare(j, dimension) < 0: + return matrix.get(i, j) + with owned(subtract(j, dimension)) as (column,): + return Rational.literal(1 if compare(i, column) == 0 else 0) + + with owned(Count(dimension)) as (twice,): + twice.multiply_small(2) + augmented = Matrix(dimension, twice, matrix.pool, entry) + try: + for k in indices(dimension): + with owned(augmented.get(k, k)) as (pivot,): + need(not pivot.numerator.negative and not pivot.numerator.magnitude.zero(), + "positive exact setup pivot") + normalize(augmented, k, pivot) + eliminate(augmented, k, dimension) + + def right(i, j): + with owned(Count(j)) as (column,): + column.add(dimension) + return augmented.get(i, column) + + return Matrix(dimension, dimension, matrix.pool, right) + finally: + augmented.close() diff --git a/research/gaussian-inverse-settled-columns/physical.py b/research/gaussian-inverse-settled-columns/physical.py new file mode 100644 index 0000000000..71535709fd --- /dev/null +++ b/research/gaussian-inverse-settled-columns/physical.py @@ -0,0 +1,143 @@ +"""Source-bound complete encoded inversion workload and literal output oracle.""" +from contextlib import contextmanager, nullcontext +from fractions import Fraction +from hashlib import sha256 +import importlib +import json +from pathlib import Path +import sys +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/physical-gaussian-core" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + source_path = HERE / "SOURCES.json" + require(source_path.stat().st_size <= 65536, "bounded source manifest") + manifest = json.loads(source_path.read_text()) + require(len(manifest["files"]) <= 16, "bounded source inventory") + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + require(path.resolve().is_relative_to(ROOT.resolve()), "repository-relative input") + require(path.is_file() and not path.is_symlink(), "regular source input") + require(path.stat().st_size <= 128 * 1024 * 1024, "bounded source input") + require(sha256(path.read_bytes()).hexdigest() == row["sha256"], + "source hash mismatch: " + row["path"]) + + +@contextmanager +def runtime(): + authenticate() + require(not any(n in sys.modules for n in + ("gaussian_sources", "gaussian_matrix", "gaussian_rationals")), + "cold physical Gaussian namespace") + sys.path.insert(0, str(SOURCE)) + sources = importlib.import_module("gaussian_sources") + with sources.opened(): + yield + + +def fixture(name): + require(name in ("dense3", "rational3", "dense4", "identity4"), "known workload") + if name == "rational3": + return [[Fraction(4), Fraction(-1), Fraction(0)], + [Fraction(1, 3), Fraction(5), Fraction(-1, 2)], + [Fraction(0), Fraction(1, 4), Fraction(3)]] + n = 3 if name == "dense3" else 4 + return [[Fraction((n + 1 if i == j else 1) if name != "identity4" + else int(i == j)) for j in range(n)] for i in range(n)] + + +def run_case(engine, values, instrument=False): + from cardinal_counts import Count + from check_support import no_decode + from gaussian_matrix import Matrix, inverse as baseline + from router_metadata import owned + from scratch_pool import ScratchPool + from session import OuterScope, borrowed_tape, erase_marker, sealed_constructors + from words import BLANK + from ring_check_words import decode + from inverse import inverse as candidate + + require(engine in ("baseline", "candidate"), "known inverse engine") + require(1 <= len(values) <= 4 and 1 <= len(values[0]) <= 4 + and all(len(row) == len(values[0]) for row in values), "bounded rectangular fixture") + pool = ScratchPool(256) + scope = OuterScope(pool) + counts = {"get": 0, "set": 0} + try: + with sealed_constructors(), scope.installed(): + with owned(Count.literal(len(values)), Count.literal(len(values[0]))) as (rows, columns): + matrix = Matrix(rows, columns, pool, lambda i, j: encode(values[decode(i)][decode(j)])) + try: + saved = (bytes(borrowed_tape(matrix.current).cells), borrowed_tape(matrix.current).head) + with counted(Matrix, counts) if instrument else nullcontext(): + with no_decode(): + result = baseline(matrix) if engine == "baseline" else candidate(matrix) + with owned(result): + output = decode_matrix(result) + require(saved == (bytes(borrowed_tape(matrix.current).cells), borrowed_tape(matrix.current).head), "source preserved") + finally: + matrix.close() + finally: + pool.empty() + require(not pool.live, "empty physical scratch pool") + for tape in pool.tapes: + erase_marker(tape) + require(tape.head == 1 and all(v == BLANK for v in tape.cells), "physical scratch restored") + if instrument: + counts["pooled_tape"] = {key: sum(getattr(t.meter, key) for t in pool.tapes) + for key in ("reads", "writes", "moves")} + counts["pool_peak"] = pool.peak + return {"output": [[str(v) for v in row] for row in output], "counts": counts} + + +def encode(value): + from cardinal_counts import Count + from gaussian_rationals import Rational + from ring_words import Signed + value = Fraction(value) + require(abs(value.numerator) < 2**16 and value.denominator < 2**16, "bounded fixture scalar") + return Rational(Signed(Count.literal(abs(value.numerator)), value < 0), + Count.literal(value.denominator)) + + +def decode_matrix(matrix): + from cardinal_counts import Count + from ring_check_words import decode + from router_metadata import owned + output = [] + for i in range(decode(matrix.rows)): + row = [] + for j in range(decode(matrix.columns)): + with owned(Count.literal(i), Count.literal(j)) as (a, b): + with owned(matrix.get(a, b)) as (value,): + n, d = decode(value.numerator.magnitude), decode(value.denominator) + row.append(Fraction(-n if value.numerator.negative else n, d)) + output.append(row) + return output + + +@contextmanager +def counted(matrix_type, counts): + old_get, old_set = matrix_type.get, matrix_type.set + + def get(self, row, column): + counts["get"] += 1 + return old_get(self, row, column) + + def set_value(self, row, column, value): + counts["set"] += 1 + return old_set(self, row, column, value) + + with patch.object(matrix_type, "get", get), patch.object(matrix_type, "set", set_value): + yield diff --git a/research/gaussian-inverse-settled-columns/verify.py b/research/gaussian-inverse-settled-columns/verify.py new file mode 100644 index 0000000000..6b239c2fbb --- /dev/null +++ b/research/gaussian-inverse-settled-columns/verify.py @@ -0,0 +1,34 @@ +"""Bounded conformance and a complete cold physical inverse workload.""" +import argparse +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from physical import fixture, run_case, runtime +from checks import identity, run + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--workload", action="store_true") + parser.add_argument("--engine", choices=("baseline", "candidate"), default="candidate") + parser.add_argument("--fixture", choices=("dense3", "rational3", "dense4", "identity4"), default="dense3") + parser.add_argument("--instrument", action="store_true") + args = parser.parse_args() + with runtime(): + if args.workload: + values = fixture(args.fixture) + result = run_case(args.engine, values, args.instrument) + identity(values, [[Fraction(v) for v in row] for row in result["output"]]) + else: + result = run() + paths = sorted(p for p in Path(__file__).resolve().parent.iterdir() if p.is_file()) + result["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() for p in paths} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()