From d2d528a7220b79d9ef150c57237e0ee07c912f5e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 14:05:36 +0000 Subject: [PATCH] perf(research): skip zero coupled-recurrence row updates --- research/sparse-coupled-certificate/PROOF.md | 127 ++++++++++++++++++ research/sparse-coupled-certificate/README.md | 101 ++++++++++++++ .../sparse-coupled-certificate/SOURCES.json | 30 +++++ research/sparse-coupled-certificate/TASK.json | 63 +++++++++ .../sparse-coupled-certificate/VERIFY.json | 37 +++++ .../sparse-coupled-certificate/adapter.py | 66 +++++++++ .../sparse-coupled-certificate/benchmark.py | 86 ++++++++++++ research/sparse-coupled-certificate/verify.py | 102 ++++++++++++++ scripts/certify_coupled_recurrence.py | 2 + 9 files changed, 614 insertions(+) create mode 100644 research/sparse-coupled-certificate/PROOF.md create mode 100644 research/sparse-coupled-certificate/README.md create mode 100644 research/sparse-coupled-certificate/SOURCES.json create mode 100644 research/sparse-coupled-certificate/TASK.json create mode 100644 research/sparse-coupled-certificate/VERIFY.json create mode 100644 research/sparse-coupled-certificate/adapter.py create mode 100644 research/sparse-coupled-certificate/benchmark.py create mode 100644 research/sparse-coupled-certificate/verify.py diff --git a/research/sparse-coupled-certificate/PROOF.md b/research/sparse-coupled-certificate/PROOF.md new file mode 100644 index 0000000000..7cd012a80c --- /dev/null +++ b/research/sparse-coupled-certificate/PROOF.md @@ -0,0 +1,127 @@ +# Skipping zero elimination rows preserves complete recurrence certificates + +This contribution was produced by Nick Petalas. Apache-2.0. + +The result is a scoped implementation-equivalence argument with exact finite +conformance and local performance evidence. No new M-matrix theorem or κ is +claimed. Ali Romman retains the certificate construction and checker. + +## Change and invariant + +In scripts/certify_coupled_recurrence.py, certify first validates A>=0 and b>=0 +and builds the augmented matrix [I-A | 1 | b]. A nonpositive pivot emits the +existing noncontraction witness and returns after the unchanged checker. +Otherwise the pivot is strictly positive before the lower-row loop begins. + +The only change is + +```python +for i in range(k+1,n): + if rows[i][k] == 0: + continue + factor = rows[i][k]/rows[k][k] + for j in range(k,n+2): rows[i][j] -= factor*rows[k][j] +``` + +The equality test is exact Fraction equality. At zero, the original factor +is zero because the pivot is positive. Every omitted assignment is x<-x-0*y, +which returns the same canonical rational value. The original block performs +no validation or side effect beyond those assignments. Induction over rows +and pivots therefore gives identical augmented matrices at every pivot. + +Every nonpositive-pivot decision, backsolve, weight, ratio and forcing total +is identical. The serialization budget and separate matrix-vector verifier +are unchanged, as are input parsing and CLI input hashes. The guard cannot +hide an invalid pivot because its test happens after the original pivot gate. +Invalid inputs encounter the unchanged validator before reaching elimination. +Both contracting and noncontracting alternatives retain their original scope. + +This argument covers every input accepted by the original bounded interface. +It does not depend on a sparse input, an upper-triangular shape or the finite +fixtures. Dense nonzero coefficients use the original update. + +## Source and conformance contract + +adapter.py authenticates the current script and unchanged JSON/validation +helper by exact SHA256 before compilation. Removing exactly the two new +guard lines must reproduce the exact baseline SHA256 at canonical main +2485805a6d47f36ea83ddde6327d453ac82d44dc. It does not reconstruct an +approximation of the baseline. All certificate fields are compared, and +both original certificate checkers validate the opposite producer's result. + +The registered checker covers the complete two-type grid with coefficients +0,1/2,1,3/2, plus seven sizes from one through 64. The latter include the +nilpotent half-chain, a dense positive contraction, and noncontraction at +the first and last diagonal position with zero forcing. Two additional +fixtures exercise a coupling-driven failure and the coefficient boundary. +The generated receipt reports the enumerated status counts. + +Six malformed inputs, three false certificates and two mutated source-byte +inputs must reject. The repository's existing six tests additionally cover +the retained source barrier, coupled failure, reducibility, singularity, +64 types, serialization overflow and the complete portable CLI check mode. +This validates the implementation change; it is not a new audit deliverable +for the predecessor's mathematical alternatives. + +## Complete-path benchmark + +The workload is the existing full-size test's 64-type half-chain, with +A[i,i+1]=1/2, all other entries zero and forcing vector one. It is a valid +declared feed-forward recurrence at the interface's maximum type count. +No new sparse-only interface is introduced. This workload reaches both +backsolves, the complete matrix-vector checks, serialization and input hash. + +benchmark.py times ten fresh complete CLI processes, five alternating pairs. +Both sides use the same interpreter, flags, JSON bytes and helper bytes. +Only the authenticated zero guard differs. It checks successful exit, empty +stderr, the 64-entry weights and total, and byte equality of complete stdout +before admitting each time. It reports every sample, median, range, CPU count, +load and exact source hashes. It includes CLI startup, parsing, validation, +certificate generation, internal verification and serialization. Setup and +the separate conformance suite are outside the timed region. No timing +threshold is imposed on CI or on future machines. + +An untimed cProfile run of the complete baseline attributes most cost to +Fraction arithmetic in certify. It records 107776 calls to Fraction._mul +and 95616 to Fraction._sub. The zero coefficient row updates are unused +work; skipping them is the first accepted mechanism. The benchmark does +not compare configurations, omit any proof check, or time a cached result. +The generated local receipt contains the measurements; it is not hand-written. +This is a local sparse-workload result. Dense speed, all-input acceleration +and full-frontier runtime are unclaimed. + +## Bounds and implementation decisions + +The production change introduces no allocation, recursion, callbacks or new +authority. Existing n<=64 validation bounds its loops. All other production +code and the original contributor notice keep their bytes. + +The supporting package bounds source files at 256 KiB, matrix dimension at +64, and conformance generation at 286 fixtures. Each benchmark process has +a 30-second timeout and there are exactly ten processes. The benchmark's +temporary directories are inside the caller's external output directory and +are cleaned on success or failure; existing output files are never overwritten. +The registered conformance path writes no files. Assertions are not required +for acceptance, so normal and optimized modes use the same checks. + +Power-of-Ten rule 3 deviation: CPython allocates exact integers, Fractions, +lists and JSON structures dynamically. A fixed-allocation port would change +the supported runtime. The original validated dimension/coefficient bounds +remain; new fixtures and source sizes are explicitly bounded. Such a port is +deferred until a consumer requires constant allocation. No memory-speed claim +or uniform bit-complexity improvement is made. + +Rule 8 deviation: the conformance loader compiles two authenticated versions +of one script and one authenticated helper. This is needed to compare the +exact old and current artifacts without a Git dependency or vendored duplicate. +Only fixed source hashes and the single literal guard are accepted; actual +source mutations reject before loading. The loader bypasses .pyc files and +restores its one temporary sys.modules entry in a finally block. Replacing +this bounded comparison seam is appropriate only if a stable production +version-selection API is introduced. + +Rule 9 deviation: rejection checks invoke a bounded set of old/new certify, +verify and authentication callables. Their targets are explicit and finite. +There is no arbitrary plugin or callback input. Normal/optimized replays, +AST compilation and function-size inspection provide available diagnostics. +No static type-analyzer acceptance is claimed. diff --git a/research/sparse-coupled-certificate/README.md b/research/sparse-coupled-certificate/README.md new file mode 100644 index 0000000000..a31044497b --- /dev/null +++ b/research/sparse-coupled-certificate/README.md @@ -0,0 +1,101 @@ +# Faster complete sparse coupled-recurrence certificates + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped implementation equivalence with finite conformance and +local performance evidence. No new κ.** Two lines in +scripts/certify_coupled_recurrence.py skip exact-zero elimination coefficients. +Both contraction alternatives, forcing solve, separate certificate verifier, +input validation, serialization and CLI remain intact. + +The complete 64-type half-chain CLI is the benchmark workload. It is the +existing full-size test's recurrence, with one half-weight edge to the next +type and forcing one. Five alternating fresh-process pairs produce identical +complete certificate bytes. Measured timings and environment are recorded in +the PR's generated receipt, not inferred from a helper microbenchmark. +Dense and arbitrary-input speedups are not claimed. + +[PROOF.md](PROOF.md) gives the all-accepted-input equivalence argument. +For a zero coefficient and a positive pivot, the original factor is zero, +so every omitted assignment leaves its rational value unchanged. The pivot +gate and every nonzero update keep their order and behavior. + +## Evidence and reproduction + +The opt-in checker authenticates the current producer and unchanged helper, +then reconstructs the exact old producer by removing exactly the two guard +lines and checking the historical digest. It compares full certificates on +286 fixture executions, including the complete two-type grid, sparse/dense sizes through +64, early/late noncontraction, a coupling failure and near-boundary input. +It cross-checks both producer outputs with both verifiers and checks input +preservation. Six malformed inputs, three false certificates and two source +mutations reject. The receipt enumerates contracting/noncontracting cases +and binds the actual package files. + +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/sparse-coupled-certificate/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sparse-coupled-certificate/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sparse-coupled-certificate +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B -m unittest discover -s tests -p 'test_research_coupled_recurrence.py' -v +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sparse-coupled-certificate --check-source-history --check-modes +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/sparse-coupled-certificate/benchmark.py --output /absolute/external/directory/benchmark.json +``` + +Use a corresponding interpreter path elsewhere. The benchmark needs a fresh +external output path and runs on POSIX systems with os.getloadavg. It creates +all temporary files under that output's parent and cleans them. The default +scientific commands write no files and each has a 60-second cap. The success +markers are PASS_SPARSE_COUPLED_CERTIFICATE and PASS_REGISTERED_RESEARCH_PACKAGE. + +## Scope and provenance + +Base is canonical main 2485805a6d47f36ea83ddde6327d453ac82d44dc, priority +revision 8. The selected binding-only first example passes; selected κ remains +.003125804. No selected scientific cold replay, native/caller admission, +proof-kernel check or complete rounded multiplier is supplied. Independent +human and formal proof-kernel review are unclaimed. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294807) +was updated before this implementation began. This originally posed +verifier-engineering target changes the replay-runtime card to the complete +bounded certificate CLI. + +Live open PRs, claims and local reservations, recent account work, main-tree +README terms and merged/all-state object searches were checked. Bounded +coverage does not establish global novelty. The source-specific optimization +is not a re-audit of the predecessor theorem. Classical zero-elimination +skipping also appears in thakrarsagar's [PR736](https://github.com/CrocSwap/integer-mult-bounds/pull/736), +an optional cyclotomic-inverse adapter on a different consumer; its method +is credited and not claimed as a new algorithm here. + +SOURCES.json pins the original producer as provenance, because that file is +the intended production edit. VERIFY.json declares both current live script +inputs. adapter.py additionally pins the exact current producer, exact old +producer and unchanged helper by SHA256. A source change invalidates this +finite conformance binding. The checks do not import or execute .pyc caches. +The benchmark compares exact old/current CLI sources, not the loader's speed. + +The change touches one shared tool and adds this opt-in evidence package. +Frozen packages, upstream archives and selected-frontier files are unchanged. +Python allocation and the bounded authenticated comparison seam are documented +in PROOF.md. All five framework assumptions remain. + +## Open next questions + +Does a real coupled caller still spend most of its time in elimination after +this guard? First profile its complete actual matrix, with its density and +forcing preserved. No further optimization or consumer is reserved. This +package does not justify a broader sparse-storage or fraction-free rewrite. + +## Credit + +Ali Romman retains the complete constructive alternative, rational certificate +checker and coupled-update lineage. Nick Petalas's least-barrier fixture, +David Ganz / Dugongue's inverse interface, Jose Manuel's setup context and +their retained predecessors keep their credit. M-matrix theory and exact +Gaussian elimination are classical. thakrarsagar retains PR736's earlier +zero-update optimization on its different replay. The new contribution is +the production guard in this consumer, its complete conformance bridge and +the measured full-CLI improvement. diff --git a/research/sparse-coupled-certificate/SOURCES.json b/research/sparse-coupled-certificate/SOURCES.json new file mode 100644 index 0000000000..232de6e8f6 --- /dev/null +++ b/research/sparse-coupled-certificate/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/compare_recursive_invoices.py", + "usage": "input", + "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48", + "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" + }, + { + "path": "scripts/certify_coupled_recurrence.py", + "usage": "provenance", + "git_blob": "0012e51d2063c293aacf271f779ef8ea20d295eb", + "sha256": "b2e69c54f3114f201fa2deacf3370a3d8dcd0b854f6cb4497ae4f315d9a63b1e" + } + ] +} diff --git a/research/sparse-coupled-certificate/TASK.json b/research/sparse-coupled-certificate/TASK.json new file mode 100644 index 0000000000..3dc8cb1da6 --- /dev/null +++ b/research/sparse-coupled-certificate/TASK.json @@ -0,0 +1,63 @@ +{ + "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": "changed", + "actual_scope": "Skip exact-zero elimination coefficients in the complete bounded coupled-recurrence certificate producer, preserving both alternatives and full certificate verification.", + "scope_change_reason": "Originally posed verifier-engineering implementation target on a complete CLI consumer, not an audit or new mathematical recurrence theorem.", + "bottleneck_link": "Reduce measured exact-arithmetic overhead while preserving the complete declared coupled-cost certificate interface. This does not supply native costs or change any supplier moment.", + "budget_minutes": 60, + "stop_rule": "Ship the first measured complete-path improvement after exact conformance. Do not extend to another arithmetic mechanism or consumer.", + "outcome": "completed", + "evidence": "Two-line production guard; PROOF.md; authenticated old/current full certificate comparisons and rejection controls in verify.py; unchanged repository tests; alternating complete CLI benchmark.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Where does a real coupled caller spend time after zero updates are skipped?", + "why_it_matters": "Further optimization requires a measured complete-consumer bottleneck.", + "first_step": "Profile the actual declared matrix and forcing with the complete producer and checker.", + "blocked_by": "No additional consumer or remaining dominant cost has been established." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294807", + "question_source": "original" +} diff --git a/research/sparse-coupled-certificate/VERIFY.json b/research/sparse-coupled-certificate/VERIFY.json new file mode 100644 index 0000000000..7c6f4b546e --- /dev/null +++ b/research/sparse-coupled-certificate/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/certify_coupled_recurrence.py", + "scripts/compare_recursive_invoices.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticated exact old/current complete certificate conformance on 286 fixtures, both verifier directions, input preservation, malformed inputs, false certificates and source mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticated exact old/current complete certificate conformance on 286 fixtures, both verifier directions, input preservation, malformed inputs, false certificates and source mutations. Optimized control." + } + ] +} diff --git a/research/sparse-coupled-certificate/adapter.py b/research/sparse-coupled-certificate/adapter.py new file mode 100644 index 0000000000..80b3b16133 --- /dev/null +++ b/research/sparse-coupled-certificate/adapter.py @@ -0,0 +1,66 @@ +"""Authenticated baseline/current modules. Produced by Nick Petalas. Apache-2.0.""" + +import hashlib +from pathlib import Path +import sys +import types + +BASELINE_SHA = "b2e69c54f3114f201fa2deacf3370a3d8dcd0b854f6cb4497ae4f315d9a63b1e" +CURRENT_SHA = "ea77f4b29452ad71612d9ff773d10bfb003eb774232106f10b1e875497f1075a" +HELPER_SHA = "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" +GUARD = b" if rows[i][k] == 0:\n continue\n" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(current, helper): + need(len(current) <= 262144 and len(helper) <= 262144, "bounded source bytes") + need(hashlib.sha256(current).hexdigest() == CURRENT_SHA, "current source changed") + need(hashlib.sha256(helper).hexdigest() == HELPER_SHA, "helper source changed") + need(current.count(GUARD) == 1, "one exact zero guard") + baseline = current.replace(GUARD, b"", 1) + need(hashlib.sha256(baseline).hexdigest() == BASELINE_SHA, "baseline reconstruction changed") + return baseline + + +def sources(): + root = Path(__file__).resolve().parents[2] + payloads = [] + for name in ("certify_coupled_recurrence.py", "compare_recursive_invoices.py"): + path = root / "scripts" / name + need(not path.is_symlink() and path.stat().st_size <= 262144, "bounded source file") + payloads.append(path.read_bytes()) + current, helper = payloads + return authenticate(current, helper), current, helper + + +def module_from_bytes(source, name): + module = types.ModuleType(name) + module.__file__ = name + ".py" + exec(compile(source, module.__file__, "exec"), module.__dict__) + return module + + +def versions(): + baseline, current, helper = sources() + previous = sys.modules.get("compare_recursive_invoices") + try: + sys.modules["compare_recursive_invoices"] = module_from_bytes(helper, "compare_recursive_invoices") + old = module_from_bytes(baseline, "coupled_baseline") + new = module_from_bytes(current, "coupled_current") + finally: + if previous is None: + sys.modules.pop("compare_recursive_invoices", None) + else: + sys.modules["compare_recursive_invoices"] = previous + return old, new + + +def chain_problem(size=64): + need(type(size) is int and 1 <= size <= 64, "chain size") + return {"schema": "coupled-recurrence/v1", + "matrix": [["1/2" if i + 1 == j else "0" for j in range(size)] + for i in range(size)], "forcing": ["1"] * size} diff --git a/research/sparse-coupled-certificate/benchmark.py b/research/sparse-coupled-certificate/benchmark.py new file mode 100644 index 0000000000..1eb7919b0d --- /dev/null +++ b/research/sparse-coupled-certificate/benchmark.py @@ -0,0 +1,86 @@ +#!/usr/bin/env python3 +"""Alternating complete CLI timings. Produced by Nick Petalas. Apache-2.0.""" + +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import runpy +import statistics +import subprocess +import sys +import tempfile +import time + +PACKAGE = Path(__file__).resolve().parent +API = runpy.run_path(str(PACKAGE / "adapter.py")) +need = API["need"] + + +def run_commands(root, problem): + runs = {"baseline": [], "changed": []} + expected = None + sequence = ["baseline", "changed"] * 5 + for label in sequence: + command = [sys.executable, "-B", "-W", "error", + str(root / label / "certify_coupled_recurrence.py"), str(problem)] + start = time.perf_counter() + result = subprocess.run(command, capture_output=True, timeout=30, check=False) + elapsed = time.perf_counter() - start + need(result.returncode == 0 and not result.stderr, "complete CLI failure") + certificate = json.loads(result.stdout) + need(certificate["status"] == "contracting" and len(certificate["weights"]) == 64 + and len(certificate["total"]) == 64, "complete 64-type certificate") + if expected is None: + expected = result.stdout + need(result.stdout == expected, "complete stdout mismatch") + runs[label].append(elapsed) + return runs, hashlib.sha256(expected).hexdigest(), sequence + + +def measure(parent): + baseline, current, helper = API["sources"]() + load_before = os.getloadavg() + with tempfile.TemporaryDirectory(prefix="coupled-benchmark-", dir=parent) as temporary: + root = Path(temporary) + for label, source in (("baseline", baseline), ("changed", current)): + directory = root / label + directory.mkdir() + (directory / "certify_coupled_recurrence.py").write_bytes(source) + (directory / "compare_recursive_invoices.py").write_bytes(helper) + path = root / "chain64.json" + path.write_text(json.dumps(API["chain_problem"]()) + "\n") + runs, digest, sequence = run_commands(root, path) + summary = {name: {"median_seconds": statistics.median(values), + "range_seconds": [min(values), max(values)]} for name, values in runs.items()} + return {"python": sys.version, "platform": platform.platform(), "cpu_count": os.cpu_count(), + "load_before": load_before, "load_after": os.getloadavg(), "sequence": sequence, + "runs_seconds": runs, "summary": summary, "complete_cli_executions": 10, + "errors": 0, "stdout_mismatches": 0, "stdout_sha256": digest, + "baseline_source_sha256": API["BASELINE_SHA"], + "current_source_sha256": API["CURRENT_SHA"], "helper_source_sha256": API["HELPER_SHA"], + "fraction_wall_time_saved": 1 - summary["changed"]["median_seconds"] + / summary["baseline"]["median_seconds"]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", required=True, type=Path) + args = parser.parse_args() + output = args.output.resolve() + need(not output.is_relative_to(PACKAGE.parents[1]) and output.parent.is_dir(), + "output must have an existing external parent") + need(not output.exists(), "output already exists") + receipt = measure(output.parent) + receipt["implementation_sha256"] = { + name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("adapter.py", "benchmark.py", "verify.py")} + with output.open("x") as stream: + stream.write(json.dumps(receipt, indent=2) + "\n") + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/sparse-coupled-certificate/verify.py b/research/sparse-coupled-certificate/verify.py new file mode 100644 index 0000000000..d0779d42cd --- /dev/null +++ b/research/sparse-coupled-certificate/verify.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Complete certificate conformance. Produced by Nick Petalas. Apache-2.0.""" + +import copy +import hashlib +import itertools +import json +from pathlib import Path +import runpy + +PACKAGE = Path(__file__).resolve().parent +API = runpy.run_path(str(PACKAGE / "adapter.py")) +need = API["need"] + + +def problem(matrix, forcing=None): + return {"schema": "coupled-recurrence/v1", "matrix": matrix, + "forcing": forcing if forcing is not None else ["1"] * len(matrix)} + + +def fixtures(): + values = ("0", "1/2", "1", "3/2") + for a, b, c, d in itertools.product(values, repeat=4): + yield problem([[a, b], [c, d]]) + for size in (1, 2, 4, 8, 16, 32, 64): + yield API["chain_problem"](size) + yield problem([["1/" + str(2 * size)] * size for _ in range(size)]) + for failure in (0, size - 1): + matrix = [["0"] * size for _ in range(size)] + matrix[failure][failure] = "1" + yield problem(matrix, ["0"] * size) + yield problem([["0", "2"], ["1", "0"]]) + yield problem([["999999999999/1000000000000"]]) + + +def compare_certificates(old, new): + statuses = {"contracting": 0, "noncontracting": 0} + for value in fixtures(): + saved = copy.deepcopy(value) + left, right = old.certify(value), new.certify(value) + need(left == right, "complete certificate mismatch") + need(value == saved, "input mutated") + need(old.verify(value, right) is True and new.verify(value, left) is True, + "separate certificate checks") + statuses[right["status"]] += 1 + return statuses + + +def failure(call, *args): + try: + call(*args) + except (ValueError, TypeError, ZeroDivisionError) as error: + return type(error).__name__, str(error) + raise ValueError("expected rejection") + + +def rejection_controls(old, new): + controls = [problem([[True]]), problem([[-1]]), problem([[0.5]]), + problem([["0"]] * 2), problem([["0"] * 65 for _ in range(65)]), + problem([["1000000000001"]])] + for value in controls: + need(failure(old.certify, value) == failure(new.certify, value), "changed rejection") + value = problem([["0", "1/2"], ["1/2", "0"]]) + good = new.certify(value) + for field in ("weights", "total", "ratio"): + bad = copy.deepcopy(good) + if field == "ratio": + bad[field] = "0" + else: + bad[field][0] = "0" + need(failure(old.verify, value, bad) == failure(new.verify, value, bad), + "changed false-certificate rejection") + baseline, current, helper = API["sources"]() + need(bool(baseline), "nonempty authenticated baseline") + failure(API["authenticate"], current + b"\n", helper) + failure(API["authenticate"], current, helper + b"\n") + return {"invalid_inputs": len(controls), "false_certificates": 3, "source_mutations": 2} + + +def package_hashes(): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "adapter.py", "verify.py", "benchmark.py") + result = {} + for name in names: + path = PACKAGE / name + need(path.stat().st_size <= 262144, "bounded package file") + result[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + old, new = API["versions"]() + result = {"certificate_statuses": compare_certificates(old, new), + "controls": rejection_controls(old, new), + "baseline_sha256": API["BASELINE_SHA"], "current_sha256": API["CURRENT_SHA"], + "package_sha256": package_hashes()} + print(json.dumps(result, sort_keys=True)) + print("PASS_SPARSE_COUPLED_CERTIFICATE") + + +if __name__ == "__main__": + main() diff --git a/scripts/certify_coupled_recurrence.py b/scripts/certify_coupled_recurrence.py index 0012e51d20..5e46014c92 100644 --- a/scripts/certify_coupled_recurrence.py +++ b/scripts/certify_coupled_recurrence.py @@ -69,6 +69,8 @@ def certify(value): 'witness': list(map(encode_rational,v))} verify(value,result); return result for i in range(k+1,n): + if rows[i][k] == 0: + continue factor = rows[i][k]/rows[k][k] for j in range(k,n+2): rows[i][j] -= factor*rows[k][j] w = backsolve(rows,[row[n] for row in rows],n)