diff --git a/research/cached-dirty-paths/BENCHMARK.json b/research/cached-dirty-paths/BENCHMARK.json new file mode 100644 index 0000000000..978d3e46cd --- /dev/null +++ b/research/cached-dirty-paths/BENCHMARK.json @@ -0,0 +1,73 @@ +{ + "executable_sha256": { + "SOURCES.json": "c8ac64e892500c3423d1d5733b19e1d793d977704f476f1d10281c5e43ba5951", + "benchmark.py": "a123eaf27a7dec4edda569e832985760dfc3927e6ebfe5996ee83a2eef565fd8", + "check_certificate.py": "ee53974866ba979b9e2ff13bcb44ba63f770351b9f24e5eccb18aaf44d66bfd9", + "replay.py": "af6feb7d42c909f5057c64f9173de30753a253f50f5215bc24145253c7f88a86" + }, + "failures": 0, + "input_sha256": { + "research/cyclic-dirty-commutator-audit/echo.py": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b", + "research/universal-dirty-certificates/README.md": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca", + "research/universal-dirty-certificates/SOURCES.json": "5d2c0b2a8921b8dc0f724fa11f93cdfeb764e57cfdfb7fa236ec958d72306899", + "research/universal-dirty-certificates/check_certificate.py": "09cba2605c62f8af0dc48cf60b4eab9f8711cba820e22698d0447833c1a16c37", + "research/universal-dirty-certificates/examples/binary-echo3.certificate.json": "cd088d9d5c0a8378361341c99e25ae5654a6be0b20398c9757a76804df2ab66a", + "research/universal-dirty-certificates/examples/binary-echo3.json": "a5199c1dc6236e346891c641b9402d8065c5bd29087c560e76fcdf2299cdfcf9", + "research/universal-dirty-certificates/examples/dirty-echo3.certificate.json": "21444c604e17d0cbd707ffbecde10edb4bdff0bdc5a3ffb71819be04c3ac58c5", + "research/universal-dirty-certificates/examples/dirty-echo3.json": "862281041cd5616a8785b526d0cee57a50aa7457a8cb64a0abff1133d6d60798", + "research/universal-dirty-certificates/examples/wrong-order.certificate.json": "54850450cc231e4db2a1c4637fc3f7a49dfb694d9c64cfeb8faa8df91d529a79", + "research/universal-dirty-certificates/examples/wrong-order.json": "137def9876c1195456a312b8c232d656ff063cc5caae645be6afc3d06709742c", + "research/universal-dirty-certificates/fields.py": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7", + "research/universal-dirty-certificates/linear_words.py": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584", + "research/universal-dirty-certificates/verify.py": "2759a2e7514453012ed0e4ffc7017375dea973925672dc16f127d91790dcb6e5" + }, + "load_average_at_end": [ + 5.4560546875, + 4.09814453125, + 2.72216796875 + ], + "logical_cpus": 18, + "median_seconds": { + "baseline": 5.680195042, + "cached": 4.398449334 + }, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "reduction_percent": 22.56517071196725, + "samples_seconds": { + "baseline": [ + 5.680195042, + 5.481301333, + 6.071584333, + 5.704761833, + 5.459807334 + ], + "cached": [ + 4.318586542, + 4.34075425, + 4.426208458, + 4.558830625, + 4.398449334 + ] + }, + "schema": "complete-dirty-path-benchmark/v1", + "scientific_output": { + "certificate_rejections": 15, + "committed_examples": 3, + "differential_cases": 120, + "echo_identities": 210, + "exponential_support": { + "basis_rows": 65, + "distinct_words": 18446744073709551616, + "states": 130 + }, + "finite_field_operations": 596, + "gaussian_field_controls": 51, + "input_rejections": 9, + "literal_counterexamples": 180, + "max_echo_basis_rows": 38, + "max_echo_states": 284, + "tensor_of_sum_rejections": 1 + }, + "successful_complete_replays": 10 +} diff --git a/research/cached-dirty-paths/README.md b/research/cached-dirty-paths/README.md new file mode 100644 index 0000000000..764115d489 --- /dev/null +++ b/research/cached-dirty-paths/README.md @@ -0,0 +1,157 @@ +# Shared-prefix replay for complete dirty-circuit certificates + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: exact implementation-preservation argument and measured performance +improvement. The complete PR5235 scientific caller runs with a prefix cache +local to each certificate check. No new dirty-circuit theorem, supplier, +selected-frontier update or kappa is claimed. Independent human and formal +proof-kernel review are unclaimed. + +## Result and evidence + +The implementation replaces repeated rooted path traversal with a trie. Every +requested output role owns a separate root. All certificate predicates and every +initial, +terminal and operator-closure equation remain in place. The source producer, +field arithmetic, fixtures and complete scientific caller are unchanged. + +Five alternating runs per side give a **22.57% reduction** in complete replay +wall time, with zero failures and identical scientific output. + +| Complete replay | Median seconds | Range seconds | +| --- | ---: | ---: | +| baseline | 5.680195 | 5.459807 to 6.071584 | +| cached | 4.398449 | 4.318587 to 4.558831 | + +The timed path includes interpreter startup, authentication of thirteen source +files, imports, the complete scientific replay and its output. Only the two +explicit elapsed-time fields are removed for scientific output comparison. +Every replay retains 210 echo identities, 120 differential circuits, +180 literal counterexamples, 15 certificate rejections, 9 input rejections, +596 finite-field operations, 51 Gaussian controls, three committed examples +and the 130-state, 65-basis-row exponential-support fixture with 2^64 words. +These are predecessor coverage counts, preserved here, not new mathematical results. + +An untimed profile found rooted path evaluation used 5.906 of 20.534 instrumented +seconds. Those times identify the changed work and are excluded from performance +samples. Producer elimination and full closure checks remain paid. The machine +has 18 logical CPUs and other research processes may run concurrently. Alternating +the sides limits drift. These are local measurements, not a portable speed ratio. + +## Why the checker accepts the same certificates + +For ordinary JSON inputs, fix one call, its reconstructed roots and exact +transition function. Define +R(i,empty)=root_i and R(i,wa)=step(R(i,w),a). The old function evaluates this +recursion by a finite loop on each requested word. + +The new trie starts with root_i. When a child labelled a is absent, it stores +step(R(i,w),a). Induction on prefix length proves that every stored row equals +the old R(i,w). An existing child therefore returns exactly the old result. +Roots remain keyed by output role, and the trie belongs to one check call. +No reuse crosses problems, fields, shifted interpretations or certificates. + +Stored row dictionaries remain unchanged. The retained transition, terminal +and linear-combination functions build new dictionaries, and scalar operations +do not mutate operands. Every request still checks its output index and every +symbol before consulting the cache. A valid cached prefix cannot bypass path +validation. The rest of the checker is byte-for-byte unchanged. `verify.py` +reverses the declared cache-only edit and requires exact equality with the +authenticated predecessor source. + +Let P be the sum of requested path lengths, U the number of distinct nonempty +rooted prefixes and R the number of requested roots. The old path evaluator +applies P transitions; the cache applies U. Full closure evaluation is unchanged. +For S dependency states, each sparse row has at most S entries, so extra retained +space is O(S(U+R)). This is a memory tradeoff, not a constant-memory claim. + +New controls use two roots with shared symbol sequences over Q, Q(i), F2, F3 +and F5, degrees one through eight, and both shifted interpretations. They compare +verdicts and check the exact P-U transition saving. Repeated calls test cache +lifetime. Both implementations reject malformed shared-prefix paths, Boolean or +out-of-range roles, missing initial/closure coverage and wrong source digests. +The complete old and new scientific outputs must agree as well. + +## Reproduce + +From the repository root, using standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cached-dirty-paths +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cached-dirty-paths/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/cached-dirty-paths/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cached-dirty-paths --check-source-history +``` + +Expected result: `PASS_CACHED_DIRTY_PATHS`. Registered checks run both complete +variants and all new controls. Normal execution writes nothing. Any CPython 3.12 +executable can replace the absolute interpreter path. + +For a fresh ten-run measurement, choose a new path outside the checkout: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cached-dirty-paths/benchmark.py --receipt /absolute/new/external/benchmark.json +``` + +`BENCHMARK.json` is the retained generated measurement artifact. Replay checks +its executable/input hashes, success count, exact scientific output and derived +medians. A fresh measurement need not reproduce the local wall times. It must +preserve the scientific output. Every live source file is pinned by SHA256 and +Git blob in SOURCES.json and declared in VERIFY.json. + +## Scope and implementation constraints + +Only this opt-in package changes. The retained PR5235 package stays immutable. +`replay.py --baseline` uses its checker; the default uses the cached copy. The +wrapper authenticates every source file before loading it. The copied checker +keeps its original attribution. No general adoption is made here. + +New cache code has no recursion, eviction or global result cache. Traversal is +bounded by word length. The new fixtures have at most sixteen unary calls; +the retained complete caller bounds the shipped replay. The benchmark has ten +child processes with 90-second deadlines and captures bounded complete reports. + +Power-of-ten deviations: Python dictionaries and exact arithmetic allocate during +execution. The cache bound above and fixed replay domains constrain live memory; +no fixed-allocation compliance is claimed. The retained independently transcribed +`reconstruct` function is 86 lines and remains byte-identical. Splitting it would +exceed this cache-only change and its exact-delta gate. New functions are below +60 lines. The fixed-module loader is needed to run the unchanged caller and +authenticates its source inventory first. Warning-strict normal and optimized +Python, exact-delta and behavioral checks provide the available diagnostics. +A future larger adapter must price its cache memory explicitly. + +No selected supplier replay, native/physical admission, rounded execution, +compiler closure, storage/stock/tape pricing, analytic recovery, Lean, Docker or +independent human review is supplied. The five selected framework assumptions +remain. Faster replay does not improve the selected multiplication bound. + +## Open next questions + +Can a larger source-bound independent-symbol program retain the benefit within +a stated peak-memory budget? Start by measuring its rooted-prefix count and +sparse-row sizes, then compare the complete producer/checker path. A compatible +real adapter and measured memory budget are blockers. The present cache avoids +no transitions when every requested prefix is distinct. + +## Credit and overlap + +zxv / [PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235) supplies +the compiler, independent checker, scalar layer, proof, fixtures and explicit +repeated-path performance handoff. Classical weighted-automata equivalence and +noncommutative identity testing retain their Kiefer and Raz-Shpilka credit. +The echo scheduler retains androolloyd, Chafik Boukhalfa / PR628 and Ali Romman / +PR621 credit. Cinna Davis / PR4100 and PR4088, ToikY, Sagar Thakrar, roger-sato, +Charles Bethin and Ross Richardson retain the dirty-phase, tensor and register +attribution in the predecessor README. No predecessor mathematics is claimed +or audited as this contribution. + +The cache, preservation argument and measurements were produced by Nick Petalas. +The target was reserved in the [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294845). +Live PRs, active Discussions, local reservations, recent account work, main README +text and merged object/formula searches were checked. The cached search covered +333 open PRs and 6,046 Discussion records but omitted 8,623 sparse main notes. +Separate Git searches covered relevant main README text. Arbitrary diffs, +unpublished work and later publications remain outside that coverage. +These searches do not establish global novelty. diff --git a/research/cached-dirty-paths/SOURCES.json b/research/cached-dirty-paths/SOURCES.json new file mode 100644 index 0000000000..6053501322 --- /dev/null +++ b/research/cached-dirty-paths/SOURCES.json @@ -0,0 +1,96 @@ +{ + "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": "research/cyclic-dirty-commutator-audit/echo.py", + "usage": "input", + "sha256": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b", + "git_blob": "76a31171368eb945815cc00dce931c6c7a88e836" + }, + { + "path": "research/universal-dirty-certificates/README.md", + "usage": "input", + "sha256": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca", + "git_blob": "be4e5981e57bdd2aa8d2ba8c36479594cf38b5d2" + }, + { + "path": "research/universal-dirty-certificates/SOURCES.json", + "usage": "input", + "sha256": "5d2c0b2a8921b8dc0f724fa11f93cdfeb764e57cfdfb7fa236ec958d72306899", + "git_blob": "78109486a46ebc0f6552d8de4cc09afa5a783535" + }, + { + "path": "research/universal-dirty-certificates/check_certificate.py", + "usage": "input", + "sha256": "09cba2605c62f8af0dc48cf60b4eab9f8711cba820e22698d0447833c1a16c37", + "git_blob": "cdb1d3fe14ba929cbe343d181cd08ff56f7f42e9" + }, + { + "path": "research/universal-dirty-certificates/examples/binary-echo3.certificate.json", + "usage": "input", + "sha256": "cd088d9d5c0a8378361341c99e25ae5654a6be0b20398c9757a76804df2ab66a", + "git_blob": "34996f4e4234ad769010ba88b108b8141b835e75" + }, + { + "path": "research/universal-dirty-certificates/examples/binary-echo3.json", + "usage": "input", + "sha256": "a5199c1dc6236e346891c641b9402d8065c5bd29087c560e76fcdf2299cdfcf9", + "git_blob": "8bb08f646562569d4c48168f9f4459cb57e8a120" + }, + { + "path": "research/universal-dirty-certificates/examples/dirty-echo3.certificate.json", + "usage": "input", + "sha256": "21444c604e17d0cbd707ffbecde10edb4bdff0bdc5a3ffb71819be04c3ac58c5", + "git_blob": "f19706f07112e6d6b0b8a5301a6b1284274d5cea" + }, + { + "path": "research/universal-dirty-certificates/examples/dirty-echo3.json", + "usage": "input", + "sha256": "862281041cd5616a8785b526d0cee57a50aa7457a8cb64a0abff1133d6d60798", + "git_blob": "13c38bf647c050243f5691d5a61be75ea3e4a4d9" + }, + { + "path": "research/universal-dirty-certificates/examples/wrong-order.certificate.json", + "usage": "input", + "sha256": "54850450cc231e4db2a1c4637fc3f7a49dfb694d9c64cfeb8faa8df91d529a79", + "git_blob": "20e3102d5a6e68b6fa19345080d0eeb957977c23" + }, + { + "path": "research/universal-dirty-certificates/examples/wrong-order.json", + "usage": "input", + "sha256": "137def9876c1195456a312b8c232d656ff063cc5caae645be6afc3d06709742c", + "git_blob": "85482942f052694a3a6d15d364d18823b51e1b00" + }, + { + "path": "research/universal-dirty-certificates/fields.py", + "usage": "input", + "sha256": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7", + "git_blob": "f1b6dc83e26bd9fd9ec67ded3fedb330ef89598d" + }, + { + "path": "research/universal-dirty-certificates/linear_words.py", + "usage": "input", + "sha256": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584", + "git_blob": "4a877e1ab9a87a0f01eb13e28ddf309c2060bd5e" + }, + { + "path": "research/universal-dirty-certificates/verify.py", + "usage": "input", + "sha256": "2759a2e7514453012ed0e4ffc7017375dea973925672dc16f127d91790dcb6e5", + "git_blob": "abccca3c9e9005343e254a78dc3482693eabd993" + } + ] +} diff --git a/research/cached-dirty-paths/TASK.json b/research/cached-dirty-paths/TASK.json new file mode 100644 index 0000000000..fb95a0ee23 --- /dev/null +++ b/research/cached-dirty-paths/TASK.json @@ -0,0 +1,61 @@ +{ + "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": "Cache rooted path prefixes within each complete PR5235 certificate check, preserving every predicate and equation; measure the complete unchanged scientific caller.", + "scope_change_reason": "The replay-runtime card is narrowed to the explicit repeated-path traversal handoff of PR5235.", + "bottleneck_link": "Quicker exact complete-endpoint checking helps test recursive-interface candidates while preserving all dirty returns. This is verifier engineering, not a supplier or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first source-bound complete-caller timing improvement with exact output parity, five alternating runs per side and all rejection controls; otherwise release the failed method.", + "outcome": "completed", + "evidence": "README.md; BENCHMARK.json; verify.py; replay.py; source-bound cache-only delta; normal and optimized registered replay.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a larger source-bound independent-symbol adapter retain a benefit within a measured peak-memory budget?", + "why_it_matters": "The trie trades extra sparse-row retention for fewer repeated transitions; large callers need a complete cost comparison.", + "first_step": "Measure distinct rooted prefixes, sparse row sizes and complete producer/checker time on one compatible actual adapter.", + "blocked_by": "A source-bound real adapter and measured memory budget are absent." + } + ] +} diff --git a/research/cached-dirty-paths/VERIFY.json b/research/cached-dirty-paths/VERIFY.json new file mode 100644 index 0000000000..24aacc8358 --- /dev/null +++ b/research/cached-dirty-paths/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cyclic-dirty-commutator-audit/echo.py", + "research/universal-dirty-certificates/README.md", + "research/universal-dirty-certificates/SOURCES.json", + "research/universal-dirty-certificates/check_certificate.py", + "research/universal-dirty-certificates/examples/binary-echo3.certificate.json", + "research/universal-dirty-certificates/examples/binary-echo3.json", + "research/universal-dirty-certificates/examples/dirty-echo3.certificate.json", + "research/universal-dirty-certificates/examples/dirty-echo3.json", + "research/universal-dirty-certificates/examples/wrong-order.certificate.json", + "research/universal-dirty-certificates/examples/wrong-order.json", + "research/universal-dirty-certificates/fields.py", + "research/universal-dirty-certificates/linear_words.py", + "research/universal-dirty-certificates/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact cache-only delta; 80 two-root field/shift fixtures; transition work law and per-call lifetime; malformed shared-prefix controls; generated timing receipt; complete baseline and cached scientific caller with exact output parity." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact cache-only delta; 80 two-root field/shift fixtures; transition work law and per-call lifetime; malformed shared-prefix controls; generated timing receipt; complete baseline and cached scientific caller with exact output parity." + } + ] +} diff --git a/research/cached-dirty-paths/benchmark.py b/research/cached-dirty-paths/benchmark.py new file mode 100644 index 0000000000..f434cc7417 --- /dev/null +++ b/research/cached-dirty-paths/benchmark.py @@ -0,0 +1,81 @@ +"""Time five alternating pairs of complete, source-authenticated replays. + +Produced by Nick Petalas. Apache-2.0. +""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import replay + + +def normalized(output): + suffix = "\nPASS_UNIVERSAL_DIRTY_CERTIFICATES\n" + replay.need(output.endswith(suffix), "complete caller success marker") + report = json.loads(output[:-len(suffix)]) + del report["seconds"] + del report["exponential_support"]["seconds"] + return report + + +def executable_hashes(): + names = ("benchmark.py", "check_certificate.py", "replay.py", "SOURCES.json") + return {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names} + + +def run_pairs(): + hashes, inputs = executable_hashes(), replay.authenticate() + samples = {"baseline": [], "cached": []} + expected = None + for trial in range(5): + for side in ("baseline", "cached"): + command = [sys.executable, "-I", "-W", "error", "-B", str(HERE / "replay.py")] + if side == "baseline": + command.append("--baseline") + start = time.perf_counter_ns() + result = subprocess.run(command, cwd=replay.ROOT, capture_output=True, + text=True, check=True, timeout=90) + elapsed = (time.perf_counter_ns() - start) / 1e9 + replay.need(not result.stderr, "warning-free complete replay") + report = normalized(result.stdout) + if expected is None: + expected = report + replay.need(report == expected, "complete scientific output differs") + samples[side].append(elapsed) + print(json.dumps({"trial": trial, "side": side, "seconds": elapsed}), flush=True) + replay.need(executable_hashes() == hashes and replay.authenticate() == inputs, + "sources changed during measurement") + before, after = (statistics.median(samples[side]) for side in ("baseline", "cached")) + return {"schema": "complete-dirty-path-benchmark/v1", "python": sys.version, + "platform": platform.platform(), "logical_cpus": os.cpu_count(), + "load_average_at_end": os.getloadavg(), "failures": 0, + "executable_sha256": hashes, "input_sha256": inputs, + "samples_seconds": samples, "median_seconds": {"baseline": before, "cached": after}, + "reduction_percent": 100 * (before - after) / before, + "scientific_output": expected, "successful_complete_replays": 10} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, required=True) + args = parser.parse_args() + output = args.receipt.resolve() + replay.need(not output.is_relative_to(replay.ROOT), "receipt must be outside checkout") + replay.need(not output.exists(), "receipt must be a new path") + receipt = run_pairs() + with output.open("x") as stream: + stream.write(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + print("PASS_COMPLETE_DIRTY_PATH_BENCHMARK", receipt["reduction_percent"]) + + +if __name__ == "__main__": + main() diff --git a/research/cached-dirty-paths/check_certificate.py b/research/cached-dirty-paths/check_certificate.py new file mode 100644 index 0000000000..01151eb028 --- /dev/null +++ b/research/cached-dirty-paths/check_certificate.py @@ -0,0 +1,208 @@ +"""Small proof checker: no search, Gaussian elimination, or producer import. + +The trusted surface includes this separately transcribed register compiler. +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +import argparse +import hashlib +import json +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from fields import scalars + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def combine(terms): + result = {} + for c, v in terms: + for i, x in v.items(): + result[i] = result.get(i, F(0))+c*x + return {i: x for i, x in result.items() if x} + + +def reconstruct(problem, shifted): + """Reconstruct a dense dependency table using immutable register versions.""" + n = problem["roles"] + require(type(n) is int and n > 0, "roles") + require(set(problem) <= {"field", "roles", "program", "reference", "target"}, "problem keys") + field = scalars(problem) + require(("target" in problem) != ("reference" in problem), "reference/target") + dependencies, labels, final = [], [], [] + + def scalar(x): + require(type(x) in (str, int), "coefficient type") + return field(x) + + def role(i): + require(type(i) is int and 0 <= i < n, "role index") + return i + + def leaf(i): + j = len(labels) + labels.append(None) + dependencies.append({}) + final.append(i) + return {j: field(1)} + + def unary(s, v): + require(type(s) is str and s, "symbol") + j = len(labels) + labels.append(s) + dependencies.append(v.copy()) + final.append(None) + return combine([(F(1), {j: field(1)}), (F(1), v)]) if shifted else {j: field(1)} + + def instructions(ops): + require(type(ops) is list, "instruction list") + registers = [leaf(i) for i in range(n)] + for op in ops: + require(type(op) is dict, "instruction") + k = op.get("op") + keys = {"add": {"op", "src", "dst", "coefficient"}, + "query": {"op", "src", "dst", "symbol", "coefficient"}, + "apply": {"op", "dst", "symbol"}, + "scale": {"op", "dst", "coefficient"}, + "swap": {"op", "src", "dst"}} + require(k in keys and set(op) <= keys[k], "instruction keys") + d = role(op["dst"]) + if k in ("add", "query", "swap"): + s = role(op["src"]) + if k == "swap": + registers[s], registers[d] = registers[d], registers[s] + elif k == "scale": + registers[d] = combine([(scalar(op["coefficient"]), registers[d])]) + elif k == "apply": + registers[d] = unary(op["symbol"], registers[d]) + else: + image = registers[s].copy() + if k == "query": + image = unary(op["symbol"], image) + registers[d] = combine([(F(1), registers[d]), (scalar(op.get("coefficient", 1)), image)]) + return registers + + left = instructions(problem["program"]) + if "reference" in problem: + right = instructions(problem["reference"]) + else: + t = problem["target"] + require(type(t) is dict and set(t) <= {"identity", "terms"}, "target") + require(type(t.get("identity", True)) is bool and type(t.get("terms", [])) is list, "target types") + leaves = [leaf(i) for i in range(n)] + right = [v.copy() if t.get("identity", True) else {} for v in leaves] + for term in t.get("terms", []): + require(type(term) is dict and set(term) <= {"out", "in", "word", "coefficient"}, "term keys") + i, j = role(term["out"]), role(term["in"]) + require(type(term["word"]) is list, "word") + image = leaves[j] + for a in term["word"][::-1]: + image = unary(a, image) + right[i] = combine([(F(1), right[i]), (scalar(term.get("coefficient", 1)), image)]) + roots = [combine([(F(1), x), (F(-1), y)]) for x, y in zip(left, right)] + + def transition(v, a): + return combine([(x, dependencies[i]) for i, x in v.items() if labels[i] == a]) + + def terminal(v): + return combine([(x, {final[i]: F(1)}) for i, x in v.items() if final[i] is not None]) + + return roots, transition, terminal, len(labels), sorted(set(labels)-{None}) + + +def follow_prefixes(node, word, step): + """Follow an already validated word; rows are immutable within one check.""" + row, children = node + for symbol in word: + if symbol not in children: + children[symbol] = (step(row, symbol), {}) + row, children = children[symbol] + return row + + +def check(problem, certificate): + require(certificate.get("schema") == "dirty-linear-certificate/v1", "certificate schema") + source_hash = hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + require(certificate.get("problem_sha256") == source_hash, "problem digest") + shifted = certificate.get("shifted") + require(type(shifted) is bool and type(certificate.get("equivalent")) is bool, "certificate flags") + roots, step, terminal, states, alphabet = reconstruct(problem, shifted) + field = scalars(problem) + require(certificate.get("states") == states, "state count") + + prefixes = {} # Owned by this check call; no cross-certificate reuse. + + def path(output, word): + require(type(output) is int and 0 <= output < len(roots), "output role") + require(type(word) is list and all(a in alphabet for a in word), "path alphabet") + node = prefixes.setdefault(output, (roots[output], {})) + return follow_prefixes(node, word, step) + + if not certificate["equivalent"]: + out = terminal(path(certificate["output"], certificate["word"])) + j = certificate["input"] + require(type(j) is int and 0 <= j < len(roots), "input role") + require(type(certificate["coefficient"]) is str, "witness coefficient type") + require(out.get(j, field(0)) == field(certificate["coefficient"]) != 0, "nonzero coefficient") + require(certificate["matrix_dimension"] == len(certificate["word"])+1, "matrix dimension") + return "counterexample" + + paths = certificate["paths"] + require(type(paths) is list and len(paths) <= states, "basis size") + basis = [path(p["output"], p["word"]) for p in paths] + require(all(not terminal(v) for v in basis), "basis output is nonzero") + + def expand(c): + require(type(c) is dict, "coordinates must be a sparse object") + terms = [] + for j, x in c.items(): + require(type(j) is str and j.isascii() and j.isdecimal() and str(int(j)) == j, "coordinate key") + require(0 <= int(j) < len(basis) and type(x) is str, "coordinate range/type") + terms.append((field(x), basis[int(j)])) + return combine(terms) + + init = certificate["initial"] + require(type(init) is list and len(init) == len(roots), "initial coverage") + require(all(expand(c) == v for c, v in zip(init, roots)), "initial span") + closure = certificate["closure"] + require(type(closure) is dict and set(closure) == set(alphabet), "complete operator closure") + for a in alphabet: + rows = closure[a] + require(type(rows) is list and len(rows) == len(basis), "closure row coverage") + require(all(expand(c) == step(v, a) for c, v in zip(rows, basis)), "invariant closure") + return "universal-identity" + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument("problem", type=Path) + p.add_argument("certificate", type=Path) + p.add_argument("--matrices", action="store_true", help="print sparse concrete counterexample matrices") + args = p.parse_args() + problem, certificate = json.loads(args.problem.read_text()), json.loads(args.certificate.read_text()) + verdict = check(problem, certificate) + if args.matrices: + require(verdict == "counterexample", "a positive certificate has no counterexample") + word = certificate["word"] + d = len(word)+1 + _, _, _, _, alphabet = reconstruct(problem, certificate["shifted"]) + matrices = {} + for a in alphabet: + triples = [[j, j, 1] for j in range(d)] if certificate["shifted"] else [] + triples += [[j, j+1, 1] for j, b in enumerate(word) if b == a] + matrices[a] = triples + print(json.dumps({"field": problem.get("field", "Q"), "dimension": d, + "operators_as_row_column_value": matrices, + "input_role": certificate["input"], "input_payload_basis": d-1, + "output_role": certificate["output"], "output_coordinate": 0, + "endpoint_discrepancy": certificate["coefficient"]}, indent=2, sort_keys=True)) + else: + print("PASS_DIRTY_LINEAR_CERTIFICATE", verdict) + + +if __name__ == "__main__": + main() diff --git a/research/cached-dirty-paths/replay.py b/research/cached-dirty-paths/replay.py new file mode 100644 index 0000000000..4717a73c0a --- /dev/null +++ b/research/cached-dirty-paths/replay.py @@ -0,0 +1,61 @@ +"""Complete unchanged PR5235 caller with an opt-in prefix-cached checker. + +The adapter and cache were produced by Nick Petalas. Apache-2.0. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = ROOT / "research/universal-dirty-certificates" + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + need(len(rows) == 13, "complete source inventory") + for row in rows: + data = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["sha256"], "source SHA256: " + row["path"]) + header = b"blob " + str(len(data)).encode() + b"\0" + need(hashlib.sha1(header + data).hexdigest() == row["git_blob"], "source blob: " + row["path"]) + return {row["path"]: row["sha256"] for row in rows} + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + need(spec is not None and spec.loader is not None, "source module loader") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def setup(cached): + authenticate() + caller = load("retained_dirty_caller", SOURCE / "verify.py") + baseline = caller.checker + fast = load("cached_dirty_checker", HERE / "check_certificate.py") + if cached: + caller.checker = fast + return caller, baseline, fast + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--baseline", action="store_true") + args = parser.parse_args() + caller, _, _ = setup(not args.baseline) + caller.main() + + +if __name__ == "__main__": + main() diff --git a/research/cached-dirty-paths/verify.py b/research/cached-dirty-paths/verify.py new file mode 100644 index 0000000000..e410596f66 --- /dev/null +++ b/research/cached-dirty-paths/verify.py @@ -0,0 +1,171 @@ +"""Preservation, exact cache-work controls, and the complete scientific caller. + +Produced by Nick Petalas. Apache-2.0. +""" +from contextlib import redirect_stdout +from copy import deepcopy +import hashlib +import io +import json +from pathlib import Path +import statistics +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import benchmark +import replay + +HELPER = '''def follow_prefixes(node, word, step): + """Follow an already validated word; rows are immutable within one check.""" + row, children = node + for symbol in word: + if symbol not in children: + children[symbol] = (step(row, symbol), {}) + row, children = children[symbol] + return row + + +''' +OLD_PATH = ''' def path(output, word): + require(type(output) is int and 0 <= output < len(roots), "output role") + require(type(word) is list and all(a in alphabet for a in word), "path alphabet") + v = roots[output] + for a in word: + v = step(v, a) + return v +''' +NEW_PATH = ''' prefixes = {} # Owned by this check call; no cross-certificate reuse. + + def path(output, word): + require(type(output) is int and 0 <= output < len(roots), "output role") + require(type(word) is list and all(a in alphabet for a in word), "path alphabet") + node = prefixes.setdefault(output, (roots[output], {})) + return follow_prefixes(node, word, step) +''' + + +def delta_check(): + source = (replay.SOURCE / "check_certificate.py").read_text() + actual = (HERE / "check_certificate.py").read_text() + replay.need(actual.count(HELPER) == actual.count(NEW_PATH) == 1, "one declared cache change") + recovered = actual.replace(HELPER, "").replace(NEW_PATH, OLD_PATH) + replay.need(recovered == source, "non-cache code or predicate changed") + + +def counted_check(module, problem, certificate): + original, count = module.reconstruct, [0] + + def reconstructed(problem, shifted): + roots, step, terminal, states, alphabet = original(problem, shifted) + + def counted(row, symbol): + count[0] += 1 + return step(row, symbol) + + return roots, counted, terminal, states, alphabet + + module.reconstruct = reconstructed + try: + verdict = module.check(problem, certificate) + finally: + module.reconstruct = original + return verdict, count[0] + + +def fixture(degree, field): + ops = [{"op": "query", "src": role, "dst": role, "symbol": "X"} + for role in range(2) for _ in range(degree)] + factor, inverse = (1, "1") if field == 2 else (2, "1/2") + start = [{"op": "scale", "dst": role, "coefficient": factor} for role in range(2)] + finish = [{"op": "scale", "dst": role, "coefficient": inverse} for role in range(2)] + return {"field": field, "roles": 2, "program": ops, "reference": start + ops + finish} + + +def prefix_work(certificate): + paths = certificate["paths"] + total = sum(len(path["word"]) for path in paths) + prefixes = {(path["output"], tuple(path["word"][:j])) + for path in paths for j in range(1, len(path["word"]) + 1)} + return total - len(prefixes) + + +def cache_controls(caller, baseline, fast): + cases = saved = 0 + for field in ("Q", "Qi", 2, 3, 5): + for degree in range(1, 9): + problem = fixture(degree, field) + for shifted in (False, True): + certificate = caller.producer.decide(problem, shifted) + expected = counted_check(baseline, problem, certificate) + actual = counted_check(fast, problem, certificate) + replay.need(expected[0] == actual[0] == "universal-identity", "complete fixture endpoint") + reduction = prefix_work(certificate) + replay.need(expected[1] - actual[1] == reduction, "exact distinct-prefix work law") + replay.need(counted_check(fast, problem, certificate) == actual, "cache leaked between calls") + cases += 1 + saved += reduction + replay.need(saved > 0, "cache must actually avoid transitions") + return {"complete_two_root_cases": cases, "saved_transition_calls": saved} + + +def rejection_controls(caller, baseline, fast): + problem = fixture(4, "Q") + original = caller.producer.decide(problem) + mutations = [] + bad = deepcopy(original); bad["paths"][-1]["word"].append("unknown"); mutations.append(bad) + bad = deepcopy(original); bad["paths"][-1]["output"] = True; mutations.append(bad) + bad = deepcopy(original); bad["paths"][-1]["output"] = 2; mutations.append(bad) + bad = deepcopy(original); bad["closure"].clear(); mutations.append(bad) + bad = deepcopy(original); bad["initial"][0] = {}; mutations.append(bad) + bad = deepcopy(original); bad["problem_sha256"] = "0" * 64; mutations.append(bad) + for bad in mutations: + for module in (baseline, fast): + try: + module.check(problem, bad) + except (ValueError, KeyError, TypeError, ZeroDivisionError): + pass + else: + raise ValueError("cache-related malformed certificate accepted") + return len(mutations) * 2 + + +def complete(caller): + output = io.StringIO() + with redirect_stdout(output): + caller.main() + return benchmark.normalized(output.getvalue()) + + +def receipt_check(): + receipt = json.loads((HERE / "BENCHMARK.json").read_text()) + replay.need(receipt["executable_sha256"] == benchmark.executable_hashes(), "measured executable hashes") + replay.need(receipt["input_sha256"] == replay.authenticate(), "measured input hashes") + samples = receipt["samples_seconds"] + replay.need(set(samples) == {"baseline", "cached"}, "both measured sides") + for side, values in samples.items(): + replay.need(len(values) == 5 and all(type(v) is float and v > 0 for v in values), "five successful runs") + replay.need(statistics.median(values) == receipt["median_seconds"][side], "measured median") + before, after = (receipt["median_seconds"][side] for side in ("baseline", "cached")) + replay.need(receipt["reduction_percent"] == 100 * (before - after) / before, "measured reduction") + replay.need(receipt["failures"] == 0 and receipt["successful_complete_replays"] == 10, "no failed samples") + replay.need(max(samples["cached"]) < min(samples["baseline"]), "timing ranges must separate") + return receipt["scientific_output"] + + +def main(): + delta_check() + caller, baseline, fast = replay.setup(False) + controls = cache_controls(caller, baseline, fast) + controls["rejections"] = rejection_controls(caller, baseline, fast) + expected = receipt_check() + old = complete(caller) + caller.checker = fast + new = complete(caller) + replay.need(old == new == expected, "complete caller scientific fields") + print(json.dumps({"controls": controls, "complete_scientific_output": new}, sort_keys=True)) + print("PASS_CACHED_DIRTY_PATHS") + + +if __name__ == "__main__": + main()