diff --git a/research/rational-box-fraction-free/README.md b/research/rational-box-fraction-free/README.md new file mode 100644 index 0000000000..a49cba11f3 --- /dev/null +++ b/research/rational-box-fraction-free/README.md @@ -0,0 +1,211 @@ +# Fraction-free solves in the complete rational parameter optimizer + +This contribution was produced by Nick Petalas. Apache-2.0. + +An opt-in integer elimination kernel removes **15.49% of measured complete +solve-and-check wall time** on the declared six-parameter workload. The +median falls from 0.079004 to 0.066770 seconds across seven alternating runs +per arm. Every certificate byte agrees, including the first chosen optimal +basis, its 757 examined bases, exact point, dual and objective 24. + +Claim type: scoped implementation proof, finite correctness evidence and a +local performance measurement. This improves execution of Ali Romman's +[PR5792](https://github.com/CrocSwap/integer-mult-bounds/pull/5792) parameter +tool. It does not prove a new LP theorem or improve kappa. The elementary +fraction-free algorithm and LP duality are classical. The new contribution +is their bounded implementation in this complete caller and its evidence. + +## Use and reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/rational-box-fraction-free/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/rational-box-fraction-free/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rational-box-fraction-free +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rational-box-fraction-free --check-source-history +``` + +The direct marker is `PASS_RATIONAL_BOX_FRACTION_FREE`. Each direct command +prints a generated JSON receipt bound to hashes of the package files. Replay +writes only temporary files outside the checkout. Set `IMB_RUN_DIR` to an +existing scratch directory to place all temporary files there. Another +CPython 3.12 interpreter can replace the displayed local path. + +Use the unchanged input and output schemas with the new opt-in runner: + +```sh +python3.12 -B research/rational-box-fraction-free/run.py problem.json > certificate.json +python3.12 -B research/rational-box-fraction-free/run.py problem.json --check certificate.json +``` + +The runner authenticates all three declared source inputs before importing +the original engine. It replaces only that process's `solve` binding and +restores it on return. Input parsing, incumbent validation, basis order, +feasibility tests, dual tests, JSON output and certificate checking are the +original code. No default or shared source file changes. + +## Why the replacement solves the same systems + +The source optimizer permits one to six parameters, at most 24 total rows, +at most 50,000 active bases, and rational numerators and denominators bounded +by 10^9. Both primal and dual solves use square matrices within this domain. +The new kernel checks that domain and requires exact `Fraction` entries. + +First multiply each augmented equation by the positive least common +multiple of its own denominators. This preserves its rational solution set +and produces an integer augmented matrix. Perform ordinary row pivoting, +then use the fraction-free update + +```text +next[i,j] = (pivot * current[i,j] - current[i,k] * current[k,j]) / previous_pivot +previous_pivot = 1 before the first column +``` + +The classical Sylvester determinant identity expresses the numerator as +`previous_pivot` times an integer minor. It applies to the augmented column +as well as coefficient columns. Row interchanges permute equations and the +corresponding minors. Thus every division is exact; the implementation also +checks its remainder explicitly. Over the rationals each update is a +nonzero scaled elimination step, preserving the solution set. A missing +pivot, or zero final diagonal, means a singular coefficient matrix. The +return is `None`, including inconsistent singular systems, as in the source. +Otherwise exact rational back substitution gives the unique solution. +Inputs are never mutated. + +Therefore each square solve has the same answer. The unchanged caller takes +the same branches in the same basis enumeration and returns the same full +certificate. Its unchanged final primal-dual checker still runs. This proof +is scoped to this bounded solver interface; the finite tests corroborate it. + +The complete workload maximizes +`x0-2x1+3x2-4x3+5x4-6x5`, with `-1<=xi<=2` and +`xi+x(i+1 mod 6)<=1/3`. Its exact optimum is independently visible: each +positive-price coordinate is at most 4/3 because its negative-price neighbor +is at least -1. Hence the objective is at most +`(1+3+5)*4/3+(2+4+6)=24`. Alternating 4/3 and -1 attains it. +This is a parameter-tool workload, not an authenticated supplier invoice. + +## Correctness evidence + +The verifier checks all 5,625 augmented two-dimensional systems whose four +matrix entries lie in `{-2,-1,0,1,2}` and whose right-hand entries lie in +`{-1,0,1}`. A separate literal determinant classifies their 1,161 singular +cases. Every nonsingular answer has zero exact residual and unchanged input. +Another 360 seeded rational systems cover every dimension one through six, +with forced singular rows in part of that domain. All 5,985 answers agree +with the source kernel. No timing result uses those differential loops. + +Eight kernel controls cover shape, exact types, numerator and denominator +limits, a late row pivot and the maximum accepted rational boundary. All six +inherited regression groups run with the replacement in-process kernel, +including 100 independent geometric LP oracles, a fractional optimum, +degenerate boxes, zero objectives, invalid incumbents and forged duals. +The inherited portable subprocess test still exercises the original CLI; +a separate exported, Git-free candidate CLI test compares complete output +bytes and checks its certificate. Each of the three actual declared input +files is then changed separately and must reject before engine import. +Normal and optimized checks retain explicit exceptions throughout. + +## Complete-path measurement + +The opt-in benchmark is: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/rational-box-fraction-free/benchmark.py +``` + +It times two fresh processes per observation: generate the complete optimum, +write its certificate, then run the separate CLI certificate check. Startup, +imports, parsing, the complete optimization, source gates on the candidate, +serialization and checking are inside the timed region. Fixture creation and +result comparison are outside it. Every output must be byte-identical and +must report objective 24 and 757 examined bases. All 14 complete pairs pass; +there are zero errors. The generated stdout receipt records the fixture, +output and source hashes, checks source stability before and after the run, +and includes every raw wall and child-CPU sample. Timing is not a CI gate. + +Measured on macOS 27.0.1, arm64, CPython 3.12.15, using the interpreter above. +The host has 18 logical CPUs; the entry load averages were 2.11, 2.02, 1.49. +Another Python process was active, and the machine was unreserved. The run +order is baseline, candidate, repeated seven times. The complete wall-time +samples, in seconds, are: + +| Round | Baseline | Candidate | +| ---: | ---: | ---: | +| 1 | 0.079575208 | 0.066769792 | +| 2 | 0.079004042 | 0.066722000 | +| 3 | 0.078111000 | 0.068358500 | +| 4 | 0.080634459 | 0.066205500 | +| 5 | 0.078052458 | 0.066579042 | +| 6 | 0.077945250 | 0.068450875 | +| 7 | 0.080182458 | 0.069031500 | + +Baseline range is 0.077945..0.080634 seconds; candidate range is +0.066205..0.069032 seconds. Median child CPU time falls from 0.075766 to +0.063610 seconds. The wall-time ranges are disjoint. This is one bounded +workload on one host; no uniform speedup across all legal LPs is claimed. + +A separate diagnostic profile of the unchanged complete in-process optimizer +records 814 square solves using 0.099 of 0.123 profiled seconds. Those times +are excluded from the benchmark. Fraction arithmetic is the measured +computation bottleneck. Feasibility arithmetic and two interpreter startups +remain, so the complete improvement is smaller than a solve-only comparison. +The observed saving fits within that work; no cached optimum is used. + +## Scope, sources and review limits + +Scientific base is canonical main +`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. The selected +conditional kappa remains 781451/250000000, with its five framework assumptions. +The current selected-binding first example passed as metadata orientation. +No selected scientific replay, Lean, Docker, supplier admission or complete +multiplication theorem is claimed. Source-to-constraint correctness, strict +physical margins, native implementation, ownership, restoration, precision, +tape costs and outer use remain separate obligations. + +The original `replay-runtime` card is refined to this independently posed +implementation question. The advance +[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294680) +preceded the new implementation. The first passing improvement is packaged; +there is no second optimization round. The fresh overlap snapshot covered +333 open PRs and 6,046 Discussion records with complete remote pagination. +Only 98 of 8,722 main note paths were materialized in its local scan. Separate +main-tree searches covered the exact tool name, rational-box model, active +bases and fraction-free parameter optimization, including general dimension +wording. Merged-title searches and the source PR body were read. PR5792 and +its released Discussion5776 supply the predecessor, not a competing active +claim. Empty matches and sparse coverage are not novelty guarantees. + +The new code is nonrecursive. The kernel stores at most six augmented rows +of seven integer entries, performs at most five elimination stages and six +back-substitution stages, and uses functions below 60 physical lines. With +input bounds, cleared entries are at most 10^72 in magnitude; determinant +bounds control intermediate minors and their products. Python allocates +integers, Fractions and JSON dynamically within these finite capacities. +This is a managed-runtime deviation from allocation-free execution. +The scoped engine-binding replacement and inherited test loader have one +authenticated target and restore their mutable bindings. Each child has a +30-second timeout; registered checks have 120 seconds. Warning-strict normal +and optimized execution, in-memory compilation and whitespace checks provide +the local diagnostics. External Python linters were unavailable. The optional +benchmark uses POSIX `resource`; Windows +benchmarking is unclaimed. Independent human and formal proof-kernel review +are unclaimed. + +## Open next questions + +1. Can the unchanged complete feasibility checks be accelerated while preserving + the first optimal basis and output bytes? Start with a separate profile after + this kernel. A second correctness and complete-path measurement is required. +2. Which authenticated supplier parameter problem benefits from this complete + solver? Derive every row from one pinned full bill and include a positive + margin variable. An LP optimum does not establish physical legality. + +## Credit + +Credit Ali Romman and PR5792 for the retained bounded optimizer, exact +certificate checker, original tests and parameter guide. Credit zxv for the inherited invoice-parser boundary helpers, and classical +LP, denominator-clearing, Sylvester and Bareiss methods. All predecessor bytes and their credit remain unchanged. +The new kernel, opt-in integration, controls and measurements were produced +by Nick Petalas. diff --git a/research/rational-box-fraction-free/SOURCES.json b/research/rational-box-fraction-free/SOURCES.json new file mode 100644 index 0000000000..c2e520d7b2 --- /dev/null +++ b/research/rational-box-fraction-free/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/compare_recursive_invoices.py", + "usage": "input", + "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48", + "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" + }, + { + "path": "scripts/optimize_rational_box.py", + "usage": "input", + "git_blob": "95c79882bcd5dced19be66faaf54829599dad72c", + "sha256": "2b466207d9f0c6aa14f37f7be4e9a9feb78ef74e90ca5fabb71e1004783c5059" + }, + { + "path": "tests/test_research_rational_box.py", + "usage": "input", + "git_blob": "63c9ef81dc308d9763d746e98da2b10fedef2f83", + "sha256": "38472b11f48cbbc2d176abc51372e51dbfab07c3a670e1282a5061c83556583f" + } + ] +} diff --git a/research/rational-box-fraction-free/TASK.json b/research/rational-box-fraction-free/TASK.json new file mode 100644 index 0000000000..c098608ea4 --- /dev/null +++ b/research/rational-box-fraction-free/TASK.json @@ -0,0 +1,67 @@ +{ + "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": "An opt-in fraction-free integer solve kernel in the unchanged complete rational-box optimizer, with byte-identical certificates and complete-process timing.", + "scope_change_reason": "Refine replay-runtime to an originally posed exact parameter-tool improvement. No predecessor audit or source-specific mathematical extension is the deliverable.", + "bottleneck_link": "Cheaper complete exact parameter optimization can reduce the cost of finding and certifying bounded supplier parameter choices. Source-to-constraint correctness remains separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact candidate with a measured complete-path improvement; do not expand the search or claim a new kappa.", + "outcome": "completed", + "evidence": "5,985 exact systems; eight kernel controls; six unchanged inherited test groups; complete CLI byte equality; all three source mutations reject; seven alternating complete CLI pairs per arm. See README and generated stdout receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the unchanged complete feasibility checks be accelerated without changing the first optimal basis or output bytes?", + "why_it_matters": "They and interpreter startup remain after the integer solve improvement.", + "first_step": "Profile a complete authenticated caller after installing the present kernel, separately from reported timing.", + "blocked_by": "A new bounded correctness and performance comparison is required; no second optimization is supplied here." + }, + { + "question": "Which authenticated supplier parameter problem benefits from this complete solver?", + "why_it_matters": "The present six-cycle fixture is a tool workload, not a supplier invoice.", + "first_step": "Derive every closed linear constraint from one pinned complete bill and include a positive margin variable.", + "blocked_by": "Native, ownership, restoration, compiler and outer conditions are not established by an LP optimum." + } + ] +} diff --git a/research/rational-box-fraction-free/VERIFY.json b/research/rational-box-fraction-free/VERIFY.json new file mode 100644 index 0000000000..f180d8d737 --- /dev/null +++ b/research/rational-box-fraction-free/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/compare_recursive_invoices.py", + "scripts/optimize_rational_box.py", + "tests/test_research_rational_box.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "5,985 exact systems, kernel boundaries, six inherited test groups, complete CLI byte equality and three actual source corruptions." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with assertions disabled; all new checks use explicit exceptions." + } + ] +} diff --git a/research/rational-box-fraction-free/benchmark.py b/research/rational-box-fraction-free/benchmark.py new file mode 100644 index 0000000000..8ba51e4a0c --- /dev/null +++ b/research/rational-box-fraction-free/benchmark.py @@ -0,0 +1,90 @@ +"""Time complete fresh-process solve plus certificate-check CLI pairs. + +Produced by Nick Petalas. Apache-2.0. Timing is an opt-in local measurement. +""" +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import resource +import statistics +import subprocess +import sys +import tempfile +import time + +from run import ROOT, PACKAGE, authenticate +from workload import problem + + +def source_hashes(): + paths = (ROOT / "scripts/optimize_rational_box.py", + ROOT / "scripts/compare_recursive_invoices.py", + PACKAGE / "run.py", PACKAGE / "solver.py", PACKAGE / "workload.py", + PACKAGE / "benchmark.py", PACKAGE / "SOURCES.json") + return {str(path.relative_to(ROOT)): sha256(path.read_bytes()).hexdigest() for path in paths} + + +def one(script, value, certificate): + command = [sys.executable, "-B", str(script), str(value)] + start_cpu = resource.getrusage(resource.RUSAGE_CHILDREN) + start = time.perf_counter() + generated = subprocess.run(command, capture_output=True, timeout=30, check=True) + certificate.write_bytes(generated.stdout) + checked = subprocess.run(command + ["--check", str(certificate)], + capture_output=True, timeout=30, check=True) + elapsed = time.perf_counter() - start + end_cpu = resource.getrusage(resource.RUSAGE_CHILDREN) + cpu = end_cpu.ru_utime + end_cpu.ru_stime - start_cpu.ru_utime - start_cpu.ru_stime + if checked.stdout != b"PASS_RATIONAL_BOX_OPTIMUM\n": + raise ValueError("Certificate was not checked") + return elapsed, cpu, generated.stdout + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=7) + args = parser.parse_args() + if not 5 <= args.rounds <= 15: + parser.error("Use 5..15 rounds per arm") + authenticate() + sources = source_hashes() + records = {"baseline": [], "candidate": []} + scripts = {"baseline": ROOT / "scripts/optimize_rational_box.py", + "candidate": PACKAGE / "run.py"} + reference = None + with tempfile.TemporaryDirectory(dir=os.environ.get("IMB_RUN_DIR")) as directory: + scratch = Path(directory) + value = scratch / "problem.json" + value.write_text(json.dumps(problem(), sort_keys=True)) + fixture_digest = sha256(value.read_bytes()).hexdigest() + for _ in range(args.rounds): + for arm in ("baseline", "candidate"): + wall, cpu, output = one(scripts[arm], value, scratch / (arm + ".json")) + if reference is None: + reference = output + if output != reference: + raise ValueError("Complete optimization output changed") + parsed = json.loads(output) + if parsed["bases_examined"] != 757 or parsed["objective"] != "24": + raise ValueError("Complete workload changed") + records[arm].append({"wall_seconds": wall, "cpu_seconds": cpu}) + authenticate() + if sources != source_hashes(): + raise ValueError("Benchmark source bytes changed during measurement") + medians = {arm: statistics.median(row["wall_seconds"] for row in values) + for arm, values in records.items()} + result = {"marker": "MEASURED_RATIONAL_BOX_COMPLETE_CLI", "python": sys.version, + "platform": platform.platform(), "rounds_per_arm": args.rounds, + "fixture_sha256": fixture_digest, "output_sha256": sha256(reference).hexdigest(), + "bases_per_solve": 757, "checked_cli_pairs": 2 * args.rounds, + "errors": 0, "samples": records, "median_wall_seconds": medians, + "fraction_wall_time_removed": 1 - medians["candidate"] / medians["baseline"], + "sources_sha256": sources} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/rational-box-fraction-free/run.py b/research/rational-box-fraction-free/run.py new file mode 100644 index 0000000000..4c8696a62d --- /dev/null +++ b/research/rational-box-fraction-free/run.py @@ -0,0 +1,51 @@ +"""Opt-in complete rational-box CLI with a fraction-free solve kernel. + +Produced by Nick Petalas. Apache-2.0. The original optimizer is Ali Romman's. +""" +from hashlib import sha256 +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def authenticate(root=ROOT, package=PACKAGE): + raw = (package / "SOURCES.json").read_bytes() + if len(raw) > 1024 * 1024: + raise ValueError("Source manifest exceeds 1 MiB") + records = json.loads(raw)["files"] + expected = { + "scripts/optimize_rational_box.py", + "scripts/compare_recursive_invoices.py", + "tests/test_research_rational_box.py", + } + inputs = [row for row in records if row["usage"] == "input"] + if len(inputs) != 3 or {row["path"] for row in inputs} != expected: + raise ValueError("Unexpected source input inventory") + for row in inputs: + data = (root / row["path"]).read_bytes() + if sha256(data).hexdigest() != row["sha256"]: + raise ValueError("Source bytes changed: " + row["path"]) + + +def main(argv=None): + try: + authenticate() + except (OSError, ValueError, KeyError, TypeError) as error: + print(str(error), file=sys.stderr) + return 2 + sys.path.insert(0, str(ROOT / "scripts")) + import optimize_rational_box as engine + from solver import solve + original = engine.solve + engine.solve = solve + try: + return engine.main(argv) + finally: + engine.solve = original + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/rational-box-fraction-free/solver.py b/research/rational-box-fraction-free/solver.py new file mode 100644 index 0000000000..66cbc577c3 --- /dev/null +++ b/research/rational-box-fraction-free/solver.py @@ -0,0 +1,54 @@ +"""Bounded rational solves by classical fraction-free elimination. + +Produced by Nick Petalas. Apache-2.0. +""" +from fractions import Fraction +from math import lcm + + +def integer_rows(matrix, rhs): + """Clear each augmented row with its own positive denominator.""" + size = len(matrix) + if not 1 <= size <= 6 or len(rhs) != size: + raise ValueError("Use square systems of size 1..6") + result = [] + for row, value in zip(matrix, rhs): + if len(row) != size: + raise ValueError("Wrong matrix row size") + entries = list(row) + [value] + if any(type(x) is not Fraction for x in entries): + raise ValueError("Use exact Fraction entries") + if any(abs(x.numerator) > 10**9 or x.denominator > 10**9 for x in entries): + raise ValueError("Input rational limit is 10^9") + scale = lcm(*(x.denominator for x in entries)) + result.append([x.numerator * (scale // x.denominator) for x in entries]) + return result + + +def solve(matrix, rhs): + """Return the unique solution, or None for a singular coefficient matrix.""" + rows = integer_rows(matrix, rhs) + size = len(rows) + previous = 1 + for column in range(size - 1): + pivot = next((i for i in range(column, size) if rows[i][column]), None) + if pivot is None: + return None + rows[column], rows[pivot] = rows[pivot], rows[column] + diagonal = rows[column][column] + for i in range(column + 1, size): + for j in range(column + 1, size + 1): + numerator = diagonal * rows[i][j] - rows[i][column] * rows[column][j] + quotient, remainder = divmod(numerator, previous) + if remainder: + raise ValueError("Fraction-free division invariant failed") + rows[i][j] = quotient + rows[i][column] = 0 + previous = diagonal + if not rows[-1][size - 1]: + return None + answer = [Fraction(0)] * size + for i in range(size - 1, -1, -1): + tail = sum((rows[i][j] * answer[j] for j in range(i + 1, size)), Fraction(0)) + answer[i] = (rows[i][-1] - tail) / rows[i][i] + return answer diff --git a/research/rational-box-fraction-free/verify.py b/research/rational-box-fraction-free/verify.py new file mode 100644 index 0000000000..855d85314d --- /dev/null +++ b/research/rational-box-fraction-free/verify.py @@ -0,0 +1,167 @@ +"""Check the new kernel, complete CLI, and source-invalidation boundaries. + +Produced by Nick Petalas. Apache-2.0. +""" +from fractions import Fraction as Q +from hashlib import sha256 +import io +from itertools import product +import json +import os +from pathlib import Path +import random +import runpy +import shutil +import subprocess +import sys +import tempfile +import unittest + +from run import PACKAGE, ROOT, authenticate +from solver import solve +from workload import problem + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def kernel_checks(original): + count = singular = 0 + for entries in product(range(-2, 3), repeat=4): + matrix = [[Q(x) for x in entries[:2]], [Q(x) for x in entries[2:]]] + determinant = entries[0] * entries[3] - entries[1] * entries[2] + for values in product(range(-1, 2), repeat=2): + rhs = list(map(Q, values)) + before = [row[:] for row in matrix], rhs[:] + actual = solve(matrix, rhs) + require(actual == original(matrix, rhs), "Kernel result differs") + require((actual is None) == (determinant == 0), "Singular classification") + require(before == (matrix, rhs), "Kernel mutated its input") + if actual is not None: + require(all(sum(x*y for x, y in zip(row, actual)) == b + for row, b in zip(matrix, rhs)), "Residual is nonzero") + else: + singular += 1 + count += 1 + rng = random.Random(103002) + for size in range(1, 7): + for trial in range(60): + matrix = [[Q(rng.randrange(-7, 8), rng.randrange(1, 8)) + for _ in range(size)] for _ in range(size)] + if size > 1 and trial % 3 == 0: + matrix[-1] = matrix[0][:] + rhs = [Q(rng.randrange(-9, 10), rng.randrange(1, 8)) for _ in range(size)] + actual = solve(matrix, rhs) + require(actual == original(matrix, rhs), "Rational kernel result differs") + if actual is not None: + require(all(sum(x*y for x, y in zip(row, actual)) == b + for row, b in zip(matrix, rhs)), "Rational residual") + count += 1 + return {"systems": count, "exhaustive_singular_systems": singular} + + +def contract_controls(): + invalid = [([], []), ([[Q(1)]], []), ([[Q(1), Q(0)]], [Q(1)]), + ([[1]], [Q(1)]), ([[Q(10**9 + 1)]], [Q(0)]), + ([[Q(1, 10**9 + 1)]], [Q(0)]), + ([[Q(0)] * 7 for _ in range(7)], [Q(0)] * 7)] + for matrix, rhs in invalid: + try: + solve(matrix, rhs) + except ValueError: + continue + raise ValueError("Invalid kernel contract accepted") + matrix = [[Q(0), Q(1, 10**9)], [Q(-10**9), Q(0)]] + require(solve(matrix, [Q(1), Q(1)]) == [Q(-1, 10**9), Q(10**9)], + "Boundary pivot/size control") + return len(invalid) + 1 + + +def complete_checks(engine): + original = engine.solve + baseline = engine.optimize(problem()) + engine.solve = solve + try: + candidate = engine.optimize(problem()) + require(candidate == baseline, "Complete certificate differs") + require(candidate["objective"] == "24" and candidate["bases_examined"] == 757, + "Complete fixture changed") + namespace = runpy.run_path(str(ROOT / "tests/test_research_rational_box.py")) + suite = unittest.defaultTestLoader.loadTestsFromTestCase(namespace["BoxTests"]) + result = unittest.TextTestRunner(stream=io.StringIO()).run(suite) + require(result.wasSuccessful() and result.testsRun == 6, "Inherited regression failure") + finally: + engine.solve = original + require(engine.solve is original, "Original binding was not restored") + return {"objective": "24", "bases_examined": 757, "inherited_test_groups": 6} + + +def invoke(command, cwd): + result = subprocess.run(command, cwd=cwd, capture_output=True, text=True, timeout=30) + require(len(result.stdout) + len(result.stderr) < 1024 * 1024, "Excessive output") + return result + + +def cli_and_invalidation(scratch): + exported = scratch / "export" + package = exported / "research" / PACKAGE.name + package.mkdir(parents=True) + for path in PACKAGE.iterdir(): + if path.is_file() and path.suffix in (".py", ".json", ".md"): + shutil.copyfile(path, package / path.name) + records = json.loads((PACKAGE / "SOURCES.json").read_text())["files"] + inputs = [row["path"] for row in records if row["usage"] == "input"] + for name in inputs: + target = exported / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, target) + value = scratch / "problem.json" + value.write_text(json.dumps(problem())) + flags = ["-O"] if sys.flags.optimize else [] + command = [sys.executable, *flags, "-B", str(package / "run.py"), str(value)] + result = invoke(command, scratch) + require(result.returncode == 0, "Git-free CLI failed: " + result.stderr) + baseline = invoke([sys.executable, *flags, "-B", str(ROOT / "scripts/optimize_rational_box.py"), + str(value)], scratch) + require(baseline.returncode == 0 and result.stdout == baseline.stdout, + "Complete CLI bytes differ") + certificate = scratch / "certificate.json" + certificate.write_text(result.stdout) + checked = invoke(command + ["--check", str(certificate)], scratch) + require(checked.returncode == 0 and checked.stdout.strip() == "PASS_RATIONAL_BOX_OPTIMUM", + "Complete certificate check failed") + for name in inputs: + target = exported / name + data = target.read_bytes() + target.write_bytes(data + b"\n") + failed = invoke(command, scratch) + require(failed.returncode == 2 and "Source bytes changed: " + name in failed.stderr, + "Changed source was accepted") + target.write_bytes(data) + return {"complete_cli_byte_equality": True, "changed_input_rejections": len(inputs)} + + +def main(): + authenticate() + sys.path.insert(0, str(ROOT / "scripts")) + import optimize_rational_box as engine + result = {"marker": "PASS_RATIONAL_BOX_FRACTION_FREE"} + result.update(kernel_checks(engine.solve)) + result["contract_controls"] = contract_controls() + with tempfile.TemporaryDirectory(dir=os.environ.get("IMB_RUN_DIR")) as directory: + previous = tempfile.tempdir + tempfile.tempdir = directory + try: + result.update(complete_checks(engine)) + result.update(cli_and_invalidation(Path(directory))) + finally: + tempfile.tempdir = previous + result["sha256"] = {str(path.relative_to(ROOT)): sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.iterdir()) if path.is_file()} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/rational-box-fraction-free/workload.py b/research/rational-box-fraction-free/workload.py new file mode 100644 index 0000000000..10cf366019 --- /dev/null +++ b/research/rational-box-fraction-free/workload.py @@ -0,0 +1,20 @@ +"""Declared complete CLI fixture, with a known exact optimum. + +Produced by Nick Petalas. Apache-2.0. +""" + + +def problem(): + """Maximize alternating prices under a six-cycle's adjacent upper bounds.""" + return { + "schema": "rational-box-lp/v1", + "objective": [1, -2, 3, -4, 5, -6], + "lower": [-1] * 6, + "upper": [2] * 6, + "feasible": [0] * 6, + "constraints": [ + {"coefficients": [int(j in (i, (i + 1) % 6)) for j in range(6)], + "bound": "1/3"} + for i in range(6) + ], + }