From 46c937e504abc9f463dd66c34aabfc33a5abaa05 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 13:53:06 +0000 Subject: [PATCH] perf(research): accelerate exact rational-rank product checks --- docs/research/rational-rank-certificates.md | 8 + .../integer-rank-product-checks/README.md | 168 ++++++++++++++++++ .../integer-rank-product-checks/SOURCES.json | 30 ++++ .../integer-rank-product-checks/TASK.json | 76 ++++++++ .../integer-rank-product-checks/VERIFY.json | 35 ++++ .../integer-rank-product-checks/baseline.py | 142 +++++++++++++++ .../integer-rank-product-checks/benchmark.py | 86 +++++++++ .../integer-rank-product-checks/fixtures.py | 36 ++++ .../integer-rank-product-checks/verify.py | 131 ++++++++++++++ scripts/certify_rational_rank.py | 54 ++++-- tests/test_research_rational_rank.py | 12 ++ 11 files changed, 768 insertions(+), 10 deletions(-) create mode 100644 research/integer-rank-product-checks/README.md create mode 100644 research/integer-rank-product-checks/SOURCES.json create mode 100644 research/integer-rank-product-checks/TASK.json create mode 100644 research/integer-rank-product-checks/VERIFY.json create mode 100644 research/integer-rank-product-checks/baseline.py create mode 100644 research/integer-rank-product-checks/benchmark.py create mode 100644 research/integer-rank-product-checks/fixtures.py create mode 100644 research/integer-rank-product-checks/verify.py diff --git a/docs/research/rational-rank-certificates.md b/docs/research/rational-rank-certificates.md index e14377a85e..11096ef29c 100644 --- a/docs/research/rational-rank-certificates.md +++ b/docs/research/rational-rank-certificates.md @@ -27,6 +27,14 @@ nonpivot rows. The producer uses elimination; the checker only uses products, coordinate identities and the rank factorization. Empty kernels and rank zero have explicit valid certificates. +The product checker clears row and column denominators and compares exact +integer dot products. If a common denominator exceeds 16384 bits, it uses +the original Fraction predicate for that product. Certificate contents and +acceptance conditions are unchanged. The +[implementation proof and complete-CLI benchmark](../../research/integer-rank-product-checks/README.md) +retain the original interface and credit; the integer-product implementation +was produced by Nick Petalas. + The CLI binds the exact problem bytes by SHA-256. It accepts integers and rational strings, rejects duplicate JSON keys and floats, and uses the Python standard library. Limits are 64 rows and columns, input numerator/denominator diff --git a/research/integer-rank-product-checks/README.md b/research/integer-rank-product-checks/README.md new file mode 100644 index 0000000000..2a17929d5e --- /dev/null +++ b/research/integer-rank-product-checks/README.md @@ -0,0 +1,168 @@ +# Integer product checks for complete rational-rank certificates + +The complete rational-rank certificate produce/save/check path takes 54.94% +less wall time on the retained dense 48-by-64 rank-eight rational fixture. +This contribution was produced by Nick Petalas. Claim type: scoped exact-arithmetic +implementation proof with finite conformance and local performance evidence. +No new rank theorem, kappa, native supplier or selected-frontier change is claimed. + +The shared `scripts/certify_rational_rank.py` keeps the existing input and output +formats, pivot selection, elimination, certificate serialization and exact +acceptance predicates. It changes the four multiplication checks for the pivot +minor inverse, rank factorization and complete right/left kernel bases. The +proof below covers arbitrary valid rational matrices in the existing interface. +Finite conformance is additional evidence, not an all-input exhaustive search. + +## Exact replacement + +For a left row x and right column y, let d and e be positive common +denominators, with X=d*x and Y=e*y integral. For every rational target z, + +```text +sum(x_t*y_t) = z +if and only if +sum(X_t*Y_t) * denominator(z) = numerator(z) * d * e. +``` + +The new checker computes d by successive least common multiples and constructs +X exactly. It computes e and Y independently for each right column, then uses +integer dot products and the displayed cross-multiplication. Positivity makes +both implications valid. A zero inner dimension gives d=e=1 and the empty +integer sum zero, so rank zero and empty kernels retain their previous meaning. + +The other checks still validate the same shapes, pivot-index sets, free-coordinate +identity blocks and rational syntax. Thus the inverse product still proves the +rank lower bound, the factorization still proves the upper bound, and the exact +kernel products and identity blocks still establish the same complete bases. +The producer and serialized result do not change. If several fields are invalid, +the first error message can change because kernel products are now batched; +all the original rejection predicates and CLI failure status remain. + +To bound common-denominator growth, a row whose running least common multiple +exceeds 16384 bits declines the integer path. The corresponding product then +uses the original exact Fraction dot-product predicate. This branch changes +cost only; it neither accepts a false product nor rejects a true one. It avoids +constructing the full scaled row for a large coprime denominator product. + +## Measured complete path + +Each timed bundle starts a fresh certificate producer, captures its complete +JSON output, saves that output and starts a fresh `--check` process. Both +processes must exit successfully, the checker must print its exact success +marker, and every output hash must agree. The fixture is generated before timing; +profiling is a separate untimed run. Imports, input parsing, elimination, all +certificate checks, serialization, process startup, saved-file I/O and replay +are inside the timed region. There are no skipped mathematical checks. + +Five alternating pairs on CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs: + +| Complete bundle | Median | Observed range | +| --- | ---: | ---: | +| Original | 440.23 ms | 434.41 to 461.09 ms | +| Integer checks | 198.39 ms | 195.43 to 210.60 ms | + +Raw samples in milliseconds, in each side's observation order: + +```text +original: 434.406917, 450.502708, 461.090000, 436.349834, 440.234625 +integer: 198.391583, 201.852167, 210.603875, 197.723625, 195.430375 +``` + +All ten bundles and twenty CLI commands succeeded. All ten produced the +certificate SHA256 `48b99c3926885f307aef55c25bfed6336fe8c734834b3ce9805b24f63be81f26`. +The fixture JSON SHA256 is +`914197cf63eeab2157e26ad92720418a7924d3811bdddf7c057fb29b9c5dbbd7`. +The generated benchmark report binds the actual measured source files to SHA256. +The machine was shared; the reported end load average was about 3.09 across +18 logical CPUs. Pair order reverses on alternate pairs to spread host noise. + +The untimed profile attributes 0.503 of 0.572 profiled seconds in the original +`certify` call to `verify`, including 697321 Fraction arithmetic dispatch calls. +Those instrumented times locate the bottleneck; they are not the reported +performance measurement. The measured complete-path reduction is below that +fraction of time. Parsing, elimination and process startup still limit the gain. +This is a local result for one synthetic interface fixture, not a universal +speed guarantee or a production supplier replay benchmark. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/integer-rank-product-checks/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/integer-rank-product-checks/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-rank-product-checks +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-rank-product-checks --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B -m unittest discover -s tests -p test_research_rational_rank.py -v +``` + +Replace the absolute interpreter with another CPython 3.12 executable as needed. +Both direct commands print `PASS_INTEGER_RANK_PRODUCTS` in a generated JSON +receipt bound to package and implementation hashes. The registered replay also +prints `PASS_REGISTERED_RESEARCH_PACKAGE`. It checks 591 complete certificate +equalities, 802 exact product/false-product cases and 24 certificate rejections. +The product cases include zero dimensions and explicit scale-limit fallbacks. +Seven relevant unit tests also pass normally and with `-O`. + +For timing, provide an existing external scratch directory: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/integer-rank-product-checks/benchmark.py --scratch /absolute/external/scratch +``` + +This emits a generated source-bound report, two final saved certificates, +the fixture and an untimed profile into that directory. It runs exactly five +pairs. Timing is deliberately opt-in rather than a CI performance threshold. +Registered commands contain only bounded correctness checks. + +## Scope, source and credit + +Ali Romman's [PR5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789) +supplies the rational-rank interface, rank factorization, complete kernel +certificates and separate product checker. The byte-identical original script +is retained as `baseline.py`, including its original attribution. Its bytes +are checked against the provenance pin at canonical main +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. Classical denominator clearing, +Gaussian elimination and rank factorization retain their credit. The new +application changes implementation cost, not their mathematical content. +The parser dependency is a source-bound live input. The changed shared script +is a declared replay input; the original script's source pin is provenance. + +The current `replay-runtime` card is refined to this implementation question. +The selected-binding first example passed. Existing published rank values and +predecessor scientific conclusions are premises, not the deliverable being +audited. All five framework assumptions, physical delivery, caller, precision, +stock and supplier admission obligations remain outside this change. No Lean, +Docker, complete selected replay or independent human/kernel review is claimed. + +## Verification constraints + +The changed shared functions are at most 35 physical lines. All their loops +inherit the validated 64-row/column bound. Certificate boundary validation +and arithmetic equalities remain enabled under `-O`. There is no recursion, +code generation, approximate arithmetic or cache of certificate decisions. +The fallback preserves the previous exact arithmetic when scaling is too large. + +Power-of-Ten rule 3 has a managed-runtime deviation: Python allocates integers, +Fractions and matrices during arithmetic. The finite CLI bounds and 16384-bit +scale guard bound the new scaled representation. The parser still limits +certificate rational strings to 4096 characters and inputs to 64-by-64; no +fixed-capacity embedded implementation is claimed. Interpreter allocations +and Fraction fallback cost are not statically allocated. Warning-strict direct, +registered and unit-test commands provide the available language diagnostics; +no static type checker is configured for this script. The benchmark's subprocesses +have 120-second timeouts and fixed invocation counts; all outputs go outside +the checkout. The literal frozen baseline remains unchanged. + +## Open next questions + +1. Does the complete-path improvement persist on a named interface search's + actual exported matrices? First export and source-bind one such matrix, + then reuse the paired CLI harness. The missing input is a declared caller + workload; the synthetic benchmark does not settle this question. +2. Can the scale threshold follow from a fixed-capacity backend's proven + memory and arithmetic budget? Start with that backend's integer capacity. + No such backend contract is supplied here. + +The structured versions are in `TASK.json`. Apache-2.0. Independent human and +formal proof-kernel review are unclaimed. diff --git a/research/integer-rank-product-checks/SOURCES.json b/research/integer-rank-product-checks/SOURCES.json new file mode 100644 index 0000000000..bc87c798f5 --- /dev/null +++ b/research/integer-rank-product-checks/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "scripts/certify_rational_rank.py", + "usage": "provenance", + "git_blob": "dcbd47f60f009a6402702d704e49ea1e6e1e252b", + "sha256": "a8416038115d638adc388c9bb66ee17d350f9a7e1712675a683d6a6f3e0590e7" + }, + { + "path": "scripts/compare_recursive_invoices.py", + "usage": "input", + "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48", + "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" + } + ] +} diff --git a/research/integer-rank-product-checks/TASK.json b/research/integer-rank-product-checks/TASK.json new file mode 100644 index 0000000000..70bf28b0a7 --- /dev/null +++ b/research/integer-rank-product-checks/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "Accelerate the complete rational-rank certificate produce/save/check path by exact bounded denominator clearing in all four product checks.", + "scope_change_reason": "The replay-runtime card is refined to the PR5789 rank certificate interface and its bounded dense rectangular fixture; this is an implementation improvement, not a scientific audit.", + "bottleneck_link": "Exact interface searches require full rank and both kernel certificates. Faster complete certificate production and checking reduce that verification cost while retaining every certificate predicate.", + "budget_minutes": 60, + "stop_rule": "Ship the first measured full-path improvement after exact conformance and rejection checks. Do not extend to other consumers.", + "outcome": "completed", + "evidence": "591 complete certificate equalities, 802 rational product/mutant cases, 24 witness rejections and seven unit tests; five paired complete CLI bundles per side, twenty successful commands, byte-identical output and a local 54.94% median wall-time reduction. See README.md and the generated benchmark report.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does this full-path improvement persist on an actual large interface-search workload with heterogeneous certificate denominators?", + "why_it_matters": "The retained fixture is dense and rational but synthetic; a broader production speed claim requires that workload.", + "first_step": "Export one source-bound interface matrix and run the unchanged paired CLI harness on it.", + "blocked_by": "A named consumer and its exact matrix export are not supplied here." + }, + { + "question": "Can the 16384-bit scaling threshold be chosen from a proved allocation and arithmetic budget for a constrained backend?", + "why_it_matters": "The fallback preserves exact acceptance while the current threshold only bounds this Python fast path.", + "first_step": "Compare fixed-memory product algorithms under an explicit integer-capacity limit.", + "blocked_by": "No fixed-capacity runtime or whole-supplier resource contract is declared." + } + ], + "evidence_details": { + "complete_certificates": 591, + "rational_products_and_mutants": 802, + "certificate_rejections": 24, + "benchmark": "Five alternating fresh-process produce/save/check bundles per side; twenty successful CLI commands; identical serialized certificate hash. Raw timing arrays and profile attribution are retained in README.md.", + "local_python": "3.12.15", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294774" + }, + "claim_type": "Scoped exact-arithmetic implementation proof with finite conformance and a measured local 54.94% complete-CLI wall-time reduction." +} diff --git a/research/integer-rank-product-checks/VERIFY.json b/research/integer-rank-product-checks/VERIFY.json new file mode 100644 index 0000000000..b6f0335dc6 --- /dev/null +++ b/research/integer-rank-product-checks/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/certify_rational_rank.py", + "scripts/compare_recursive_invoices.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete certificate equality, exact rational products, zero-dimensional factors and corrupted witnesses." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same arithmetic and rejection checks with assertions disabled." + } + ] +} diff --git a/research/integer-rank-product-checks/baseline.py b/research/integer-rank-product-checks/baseline.py new file mode 100644 index 0000000000..dcbd47f60f --- /dev/null +++ b/research/integer-rank-product-checks/baseline.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Export exact rank, factorization and complete left/right kernel witnesses. + +Classical Gaussian elimination and rank factorization. Prepared for +Ali Romman with substantial OpenAI Codex assistance. +""" +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +import re +import sys +from compare_recursive_invoices import _pairs, _integer, _not_integer, require + + +def rational(x): + require(type(x) is int or type(x) is str and len(x) <= 4096 + and re.fullmatch(r'-?[0-9]+(?:/[1-9][0-9]*)?',x,re.ASCII), 'Use exact rational entries') + return Q(x) + + +def encode_rational(q): + require(max(abs(q.numerator).bit_length(), q.denominator.bit_length()) <= 6000, + 'Exact certificate exceeds the 6000-bit rational budget') + return str(q) + + +def read(path, limit): + with Path(path).open('rb') as f: raw=f.read(limit+1) + require(len(raw)<=limit,'JSON byte limit exceeded') + return json.loads(raw,object_pairs_hook=_pairs,parse_int=_integer, + parse_float=_not_integer,parse_constant=_not_integer),sha256(raw).hexdigest() + + +def matrix(raw,m,n): + require(type(raw) is list and len(raw)==m + and all(type(row) is list and len(row)==n for row in raw),'Wrong matrix shape') + return [[rational(x) for x in row] for row in raw] + + +def validate(value): + require(type(value) is dict and value.keys()=={'schema','matrix'} + and value['schema']=='rational-rank-problem/v1','Invalid rank problem') + raw=value['matrix'] + require(type(raw) is list and 1<=len(raw)<=64 and type(raw[0]) is list + and 1<=len(raw[0])<=64,'Use 1..64 rows and columns') + a=matrix(raw,len(raw),len(raw[0])) + require(all(abs(x.numerator)<=10**9 and x.denominator<=10**9 for row in a for x in row), + 'Input numerator and denominator limit is 10^9') + return a + + +def inverse(a): + n=len(a);rows=[row[:]+[Q(i==j) for j in range(n)] for i,row in enumerate(a)] + for k in range(n): + pivot=next(i for i in range(k,n) if rows[i][k]) + rows[k],rows[pivot]=rows[pivot],rows[k];d=rows[k][k];rows[k]=[x/d for x in rows[k]] + for i in range(n): + if i!=k and rows[i][k]: + c=rows[i][k];rows[i]=[x-c*y for x,y in zip(rows[i],rows[k])] + 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] + 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) + if pivot is None:continue + work[r],work[pivot]=work[pivot],work[r];row_ids[r],row_ids[pivot]=row_ids[pivot],row_ids[r] + 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] + 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=[] + for free in (j for j in range(n) if j not in cols): + v=[Q(j==free) for j in range(n)] + for k,j in enumerate(cols):v[j]=-coeff[k][free] + right.append(v) + left=[] + for free in (i for i in range(m) if i not in chosen_rows): + v=[Q(i==free) for i in range(m)] + for l,i in enumerate(chosen_rows):v[i]=-sum((a[free][cols[k]]*inv[k][l] for k in range(r)),Q(0)) + left.append(v) + encode=lambda rows:[[encode_rational(x) for x in row] for row in rows] + result={'schema':'rational-rank-certificate/v1','rank':r,'rows':chosen_rows,'columns':cols, + 'minor_inverse':encode(inv),'coefficients':encode(coeff), + 'right_kernel':encode(right),'left_kernel':encode(left)} + verify(value,result);return result + + +def verify(value,result): + """Check the factorization, minor inverse and complete kernel bases by products.""" + a=validate(value);m,n=len(a),len(a[0]) + require(type(result) is dict and result.get('schema')=='rational-rank-certificate/v1','Invalid certificate') + r=result.get('rank');require(type(r) is int and 0<=r<=min(m,n),'Invalid rank') + rows,cols=result.get('rows'),result.get('columns') + for indices,bound in ((rows,m),(cols,n)): + require(type(indices) is list and len(indices)==r and len(set(indices))==r + and all(type(i) is int and 0<=iMAX_PRODUCT_SCALE_BITS:return None + result.append(([x.numerator*(denominator//x.denominator) for x in row],denominator)) + return result + + +def _product_equal(a,b,c,m,k,n): + """Test A B = C using exact integer dot products after row/column scaling. + + Shapes have already been checked at the certificate boundary. Explicit + dimensions preserve empty factors and zero-dimensional kernels. + """ + left=_scaled_rows(a) + right=_scaled_rows([[b[i][j] for i in range(k)] for j in range(n)]) + if left is None or right is None: + return all(sum((a[i][t]*b[t][j] for t in range(k)),Q(0))==c[i][j] + for i in range(m) for j in range(n)) + for i in range(m): + row,rd=left[i] + for j in range(n): + column,cd=right[j];target=c[i][j] + numerator=sum(x*y for x,y in zip(row,column)) + if numerator*target.denominator != target.numerator*rd*cd:return False + return True + + def verify(value,result): """Check the factorization, minor inverse and complete kernel bases by products.""" a=validate(value);m,n=len(a),len(a[0]) @@ -104,22 +140,20 @@ def verify(value,result): require(type(indices) is list and len(indices)==r and len(set(indices))==r and all(type(i) is int and 0<=i