diff --git a/docs/research/rational-rank-integer-pivots-benchmark.json b/docs/research/rational-rank-integer-pivots-benchmark.json new file mode 100644 index 0000000000..34c25f6d65 --- /dev/null +++ b/docs/research/rational-rank-integer-pivots-benchmark.json @@ -0,0 +1,47 @@ +{ + "benchmark_sha256": "af75f07c4da859705ce9679b0dbfcc0e98852ecf127179479d9104fa1c751f5f", + "certificate_sha256": "4c0ef08a132525002271c5a6a0415c78efe681e0d37af2eaebf5dfa391d30e60", + "cpu_count": 16, + "fixture": { + "columns": 64, + "rank": 8, + "rows": 48 + }, + "medians_ns": { + "after": 673682500, + "before": 727398100 + }, + "pairs": 7, + "parser_sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6", + "platform": "Windows-11-10.0.26300-SP0", + "problem_sha256": "914197cf63eeab2157e26ad92720418a7924d3811bdddf7c057fb29b9c5dbbd7", + "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr 8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]", + "samples_ns": { + "after": [ + 624360100, + 658604900, + 673682500, + 683518700, + 716061500, + 689858500, + 639098800 + ], + "before": [ + 663245300, + 713954900, + 738263800, + 727398100, + 875404400, + 734227900, + 677459200 + ] + }, + "schema": "rational-rank-pivot-benchmark/v1", + "source_sha256": { + "after": "6fb4fe3be86fc996ae60ee764ae67c3d824947b6cae067f43e55ee8ac358f647", + "before": "c09b90259f43cab334e6e6f39b786a7960aee1935daa94a31f28d8c504bdbd0b" + }, + "successful_cli_commands": 32, + "wall_time_reduction": 0.07384621983477824, + "warmup_bundles": 2 +} diff --git a/docs/research/rational-rank-integer-pivots.md b/docs/research/rational-rank-integer-pivots.md new file mode 100644 index 0000000000..616c938535 --- /dev/null +++ b/docs/research/rational-rank-integer-pivots.md @@ -0,0 +1,153 @@ +# Primitive integer pivots for rational-rank certificates + +The complete rational-rank generate/save/check path is **7.38% faster** in the +local paired benchmark below: median 727.3981 ms becomes 673.6825 ms. The change +replaces only pivot discovery's per-entry `Fraction` arithmetic with primitive +integer rows. It retains the exact pivot policy and serialized certificates. +This is a measured implementation improvement, not a new rank algorithm, +supplier, exponent saving, or multiplication theorem. + +## Task, sources and overlap + +Started from canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. The +`replay-runtime` card was selected using the verifier-engineering expertise +override, nonce `3cf44b857eaf6b65fc973b72558b25c7`, scope key +`b1dd41940c60d240b47a`. Scope is **refined** to the shared rank-certificate +producer, with a stop rule of one measured full-path improvement preserving +all existing checks. The selected binding-only orientation passed; it is not +a scientific replay. + +Ali Romman's [PR5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789) +supplies the exact rank, factorization and complete-kernel certificate interface. +Nick Petalas's [PR6272](https://github.com/CrocSwap/integer-mult-bounds/pull/6272) +already accelerates all four verification products. The present change acts on +the remaining **forward pivot elimination**, not those product checks. The +48-by-64 rank-eight benchmark fixture is reproduced from PR6272 with credit; +the two reported speedups are not added together or compared across hosts. + +Before work, the live handoff thread #1166, onboarding #1163 and active +Discussions were read. Targeted all-state PR-body searches covered `rational +rank`, `certify_rational_rank`, and `rank`/`elimination`; a later open-PR search +covered `rational-rank`. No matching pivot implementation was identified. +`find_overlap.py --task replay-runtime --offline` explicitly reported incomplete +local coverage (1 of 8,917 HEAD notes) and no remote cache; the authenticated +GitHub connector and rendered Discussions supplied the bounded live checks. +Hidden discussion items, arbitrary diffs and unpublished work are not covered. +This is not a novelty certificate. No advance reservation was posted for this +short session. Main was fetched again before publication and remained unchanged. + +The unchanged baseline source at the commit above has SHA-256 +`c09b90259f43cab334e6e6f39b786a7960aee1935daa94a31f28d8c504bdbd0b`. +The exact parser dependency has SHA-256 +`3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6`. +The benchmark receipt binds both compared sources and the harness. Frozen +predecessor packages and selected-result files are unchanged. + +## Why the certificates are identical + +Clear each input row's denominators, then divide a nonzero integer row by the +gcd of its entries. Each work row is a nonzero rational multiple of the +corresponding row in the original forward elimination. This also makes sense +for a zero row, which is left zero. + +Suppose the pivot row and another row are `s R` and `t S`, where `s,t` are +nonzero rational numbers. Write their entries in the pivot column as `a,b`, +with `a != 0`, and let `g = gcd(a,b)`. The new integer elimination is + +```text +(a/g) (t S) - (b/g) (s R) + = (s t R[j]/g) (S - (S[j]/R[j]) R). +``` + +The coefficient is nonzero. Dividing the resulting nonzero row by its gcd +preserves the invariant. A zero row remains zero; when `b=0`, both algorithms +leave the row alone. All earlier pivot entries are already zero, so retaining +only the tail and restoring the zero prefix is exact. Therefore both algorithms +see the same zero pattern, take the same first available pivot in every +column, and perform the same row swaps. Negative pivots require no special +sign convention. + +The original matrix is untouched. Once pivot row/column indices are known, +minor inversion, coefficient construction, both complete kernel bases, +serialization and all verification predicates are unchanged. Consequently the +complete certificate is identical for every accepted input, not merely its +rank. Exact input-byte binding and damaged-certificate rejection remain active; +there is no result cache or new invalidation rule. + +The existing interface permits at most 64 denominators of at most 10^9 per +row. Thus the initial common denominator is below 2^1920. This observation +bounds initial denominator clearing only; it is not a fixed-memory or universal +runtime guarantee for intermediate elimination. + +## Evidence and reproduction + +On Windows 11 build 26300, CPython 3.12.10, 16 logical CPUs: + +- All eight rank unit tests pass normally and with isolated optimized Python. + The new test compares exact pivot choices and complete certificates for + 154 matrices against the original Fraction pivot policy, including zero, + dependent, rectangular, signed, boundary-size and boundary-value cases. + Existing independent permutation-minor checks cover all 512 binary 3-by-3 + matrices and 60 rational rectangular matrices; existing corruption and + exact input-byte rejection controls remain. +- PR6272's unchanged conformance verifier passes normally and under `-O`: + 591 complete certificate equalities, 802 product/mutation cases and 24 + certificate rejections. These overlap some unit-test domains and are not + claimed as a disjoint census. +- Seven alternating fresh-process timing pairs, after warming both complete + paths, all produce byte-identical certificates. All 32 CLI commands pass, + including warmups. Every timed bundle generates the certificate, saves it, + then verifies it in another process. All seven after measurements are below + their corresponding before measurements. + +Raw milliseconds, in pair order: + +```text +before: 663.2453 713.9549 738.2638 727.3981 875.4044 734.2279 677.4592 +after: 624.3601 658.6049 673.6825 683.5187 716.0615 689.8585 639.0988 +``` + +The [machine-readable receipt](rational-rank-integer-pivots-benchmark.json) +retains exact nanoseconds, source/fixture/output hashes and environment. +Windows stdout uses CRLF; certificate-byte hashes can differ on POSIX while +the same-host before/after comparison must remain exact. The harness accepts +either platform's success-line terminator. + +From the repository root, use Python 3.12+: + +```sh +python -B -W error -m unittest discover -s tests -p test_research_rational_rank.py -v +python -I -O -W error -B tests/test_research_rational_rank.py -v +python -W error -B research/integer-rank-product-checks/verify.py +python -O -W error -B research/integer-rank-product-checks/verify.py +``` + +To reproduce timing, save the exact original script outside the checkout and +create an empty scratch directory. This Python command preserves source bytes +on Windows and POSIX; substitute an actual external path for `/tmp/rank-before.py`: + +```sh +python -c "import pathlib,subprocess; pathlib.Path('/tmp/rank-before.py').write_bytes(subprocess.check_output(['git','show','7c49fe32c55de02c2c873655c804b16e4c3fef0a:scripts/certify_rational_rank.py']))" +python -B scripts/benchmark_rational_rank.py --before /tmp/rank-before.py --scratch /tmp/rank-benchmark +``` + +The opt-in benchmark writes only to the supplied scratch directory. It includes +interpreter startup and file I/O; the improvement is specific to this synthetic +fixture and host. No all-input speed claim, supplier cold replay, Lean proof, +independent human review, or hosted CI success is asserted by these local checks. + +## Open next questions + +- Does the complete-path gain persist on a named consumer's exported matrices? + Pin one actual input and reuse the paired harness before making a production + throughput claim. Such a consumer workload is not supplied here. +- How do high-rank matrices with unrelated denominators affect peak memory and + speed? First compare both exact implementations on a declared bounded family; + the current timing receipt establishes neither a worst-case bound nor a + fixed-capacity backend contract. + +Classical denominator clearing, Gaussian elimination and primitive-row +normalization retain their usual credit. Prepared for +`josecarlosgonzalezroque-design` with substantial OpenAI Codex assistance, one +agent. Apache-2.0. Predecessor authors and their source notices are retained. diff --git a/scripts/benchmark_rational_rank.py b/scripts/benchmark_rational_rank.py new file mode 100644 index 0000000000..32ecf73866 --- /dev/null +++ b/scripts/benchmark_rational_rank.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Compare complete rank-certificate CLI bundles against a saved source file. + +The dense rank-eight fixture is Nick Petalas's PR6272 fixture, using Ali +Romman's PR5789 certificate interface. Prepared with OpenAI Codex assistance. +Timing is opt-in, local evidence; outputs go only to --scratch. +""" +import argparse +from fractions import Fraction +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import random +import statistics +import subprocess +import sys +import time + +ROOT=Path(__file__).resolve().parents[1] + + +def fixture(): + rng=random.Random(5789) + left=[[rng.randrange(-4,5) for _ in range(8)] for _ in range(48)] + right=[[rng.randrange(-4,5) for _ in range(64)] for _ in range(8)] + return {'schema':'rational-rank-problem/v1','matrix':[ + [str(Fraction(sum(left[i][k]*right[k][j] for k in range(8)), + 2**(i%5)*3**(j%4))) for j in range(64)] for i in range(48)]} + + +def bundle(script,problem,certificate,environment): + command=[sys.executable,'-B','-W','error','-X', + 'pycache_prefix='+str(problem.parent/'bytecode'),str(script),str(problem)] + start=time.perf_counter_ns() + result=subprocess.run(command,env=environment,capture_output=True,timeout=120) + if result.returncode or result.stderr: + raise RuntimeError('Certificate production failed: '+repr(result.stderr)) + certificate.write_bytes(result.stdout) + checked=subprocess.run(command+['--check',str(certificate)],env=environment, + capture_output=True,timeout=120) + elapsed=time.perf_counter_ns()-start + if (checked.returncode or checked.stderr + or checked.stdout.splitlines()!=[b'PASS_RATIONAL_RANK_CERTIFICATE']): + raise RuntimeError('Saved certificate check failed: '+repr(checked.stderr)) + return elapsed,sha256(result.stdout).hexdigest() + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--before',required=True,type=Path,help='Unchanged baseline Python source') + parser.add_argument('--scratch',required=True,type=Path,help='Existing output directory') + args=parser.parse_args() + if not args.before.is_file() or not args.scratch.is_dir(): + parser.error('--before must be a file and --scratch an existing directory') + scratch=args.scratch.resolve();before=args.before.resolve() + problem=scratch/'rank-problem.json' + problem.write_bytes(json.dumps(fixture(),sort_keys=True).encode('utf-8')) + scripts={'before':before,'after':ROOT/'scripts/certify_rational_rank.py'} + environment=dict(os.environ,PYTHONPATH=str(ROOT/'scripts'),PYTHONDONTWRITEBYTECODE='1') + environment.pop('PYTHONOPTIMIZE',None) + environment.pop('PYTHONPYCACHEPREFIX',None) + samples={side:[] for side in scripts};digests=set() + # Warm both complete paths; warmup times are excluded, hashes still checked. + for side,script in scripts.items(): + _,digest=bundle(script,problem,scratch/(side+'-certificate.json'),environment) + digests.add(digest) + for pair in range(7): + for side in (('before','after') if pair%2==0 else ('after','before')): + elapsed,digest=bundle(scripts[side],problem,scratch/(side+'-certificate.json'),environment) + samples[side].append(elapsed);digests.add(digest) + if len(digests)!=1: + raise RuntimeError('Serialized certificates differ') + medians={side:statistics.median(values) for side,values in samples.items()} + report={'schema':'rational-rank-pivot-benchmark/v1', + 'python':sys.version,'platform':platform.platform(),'cpu_count':os.cpu_count(), + 'fixture':{'rows':48,'columns':64,'rank':8},'pairs':7,'warmup_bundles':2, + 'successful_cli_commands':32,'samples_ns':samples,'medians_ns':medians, + 'wall_time_reduction':1-medians['after']/medians['before'], + 'problem_sha256':sha256(problem.read_bytes()).hexdigest(), + 'certificate_sha256':next(iter(digests)), + 'source_sha256':{side:sha256(path.read_bytes()).hexdigest() for side,path in scripts.items()}, + 'parser_sha256':sha256((ROOT/'scripts/compare_recursive_invoices.py').read_bytes()).hexdigest(), + 'benchmark_sha256':sha256(Path(__file__).read_bytes()).hexdigest()} + (scratch/'benchmark.json').write_text(json.dumps(report,indent=2,sort_keys=True)+'\n',encoding='utf-8') + print(json.dumps(report,sort_keys=True)) + + +if __name__=='__main__':main() diff --git a/scripts/certify_rational_rank.py b/scripts/certify_rational_rank.py index ef1e3f7f80..73b5c08749 100644 --- a/scripts/certify_rational_rank.py +++ b/scripts/certify_rational_rank.py @@ -9,7 +9,7 @@ from fractions import Fraction as Q from hashlib import sha256 import json -from math import lcm +from math import gcd, lcm from pathlib import Path import re import sys @@ -67,8 +67,20 @@ def inverse(a): return [row[n:] for row in rows] -def certify(value): - a=validate(value);m,n=len(a),len(a[0]);work=[row[:] for row in a] +def _pivot_minor(a): + """Choose the same pivots as rational elimination, using primitive rows. + + Each work row is a nonzero rational multiple of the corresponding row + in ordinary elimination. Clearing denominators and dividing by the gcd + preserve that invariant, so zero tests and first-pivot choices agree. + Validated inputs have at most 64 denominators of at most 10^9 per row. + """ + m,n=len(a),len(a[0]);work=[] + for row in a: + denominator=lcm(*(x.denominator for x in row)) + values=[x.numerator*(denominator//x.denominator) for x in row] + divisor=gcd(*values) + work.append([x//divisor for x in values] if divisor else values) row_ids=list(range(m));chosen_rows=[];cols=[] for j in range(n): r=len(cols);pivot=next((i for i in range(r,m) if work[i][j]),None) @@ -77,8 +89,18 @@ def certify(value): chosen_rows.append(row_ids[r]);cols.append(j) for i in range(r+1,m): if work[i][j]: - c=work[i][j]/work[r][j] - for k in range(j,n):work[i][k]-=c*work[r][k] + divisor=gcd(work[r][j],work[i][j]) + p,c=work[r][j]//divisor,work[i][j]//divisor + tail=[p*work[i][k]-c*work[r][k] for k in range(j+1,n)] + divisor=gcd(*tail) + if divisor:tail=[x//divisor for x in tail] + work[i]=[0]*(j+1)+tail + return chosen_rows,cols + + +def certify(value): + a=validate(value);m,n=len(a),len(a[0]) + chosen_rows,cols=_pivot_minor(a) r=len(cols);inv=inverse([[a[i][j] for j in cols] for i in chosen_rows]) coeff=[[sum((inv[k][l]*a[chosen_rows[l]][j] for l in range(r)),Q(0)) for j in range(n)] for k in range(r)] right=[] diff --git a/tests/test_research_rational_rank.py b/tests/test_research_rational_rank.py index 307cb3a37c..fa4e967826 100644 --- a/tests/test_research_rational_rank.py +++ b/tests/test_research_rational_rank.py @@ -9,6 +9,7 @@ import sys import tempfile import unittest +from unittest.mock import patch ROOT=Path(__file__).resolve().parents[1];sys.path.insert(0,str(ROOT/'scripts')) import certify_rational_rank as tool @@ -33,7 +34,47 @@ def oracle(a): return 0 +def rational_pivots(a): + """Independent Fraction representation of the original pivot policy.""" + rows=[row[:] for row in a];ids=list(range(len(a)));chosen=[];columns=[] + for column in range(len(a[0])): + rank=len(columns) + pivot=next((i for i in range(rank,len(rows)) if rows[i][column]),None) + if pivot is None:continue + rows[rank],rows[pivot]=rows[pivot],rows[rank] + ids[rank],ids[pivot]=ids[pivot],ids[rank] + chosen.append(ids[rank]);columns.append(column) + for i in range(rank+1,len(rows)): + multiple=rows[i][column]/rows[rank][column] + rows[i]=[x-multiple*y for x,y in zip(rows[i],rows[rank])] + return chosen,columns + + class RankTests(unittest.TestCase): + def test_primitive_pivots_preserve_complete_certificates(self): + rng=random.Random(5789) + cases=[[[0]],[[0,0,0],[0,0,0]],[[0,0],[0,-3],[0,6]], + [[0,0,0,0],[0,0,-2,1],[0,3,0,2],[0,6,-4,6]], + [['-999999999/1000000000','1/999999937'], + ['999999999/1000000000','-1/999999937']]] + for m,n in itertools.product(range(1,7),repeat=2): + for _ in range(4): + cases.append([[str(Q(rng.randrange(-9,10),rng.randrange(1,30))) + for _ in range(n)] for _ in range(m)]) + for m,n,rank in ((64,64,0),(64,64,1),(48,64,8),(64,48,8),(16,24,16)): + left=[[rng.randrange(-4,5) for _ in range(rank)] for _ in range(m)] + right=[[rng.randrange(-4,5) for _ in range(n)] for _ in range(rank)] + cases.append([[str(Q(sum(left[i][k]*right[k][j] for k in range(rank)), + 2**(i%5)*3**(j%4))) for j in range(n)] for i in range(m)]) + for raw in cases: + value=problem(raw);a=tool.validate(value);unchanged=[row[:] for row in a] + self.assertEqual(tool._pivot_minor(a),rational_pivots(a)) + self.assertEqual(a,unchanged) + actual=tool.certify(value) + with patch.object(tool,'_pivot_minor',rational_pivots): + expected=tool.certify(value) + self.assertEqual(actual,expected) + def test_integer_products_keep_rational_and_empty_boundaries(self): a=[[Q(1,2),Q(-2,3)],[Q(5,7),Q(11,13)]] b=[[Q(3,17)],[Q(-19,23)]]