From d562956726caa39ff588c6595ba16cae7391c07a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 11:14:04 +0000 Subject: [PATCH] perf(research): speed up complete rank-eight proof replay --- .../rank8-rup-signed-values/BENCHMARK.json | 90 ++++++++++ research/rank8-rup-signed-values/CHECKS.json | 65 ++++++++ research/rank8-rup-signed-values/PROOF.md | 131 +++++++++++++++ research/rank8-rup-signed-values/README.md | 126 ++++++++++++++ research/rank8-rup-signed-values/SOURCES.json | 84 ++++++++++ research/rank8-rup-signed-values/TASK.json | 66 ++++++++ research/rank8-rup-signed-values/VERIFY.json | 72 ++++++++ research/rank8-rup-signed-values/adapter.py | 79 +++++++++ research/rank8-rup-signed-values/benchmark.py | 68 ++++++++ research/rank8-rup-signed-values/verify.py | 156 ++++++++++++++++++ 10 files changed, 937 insertions(+) create mode 100644 research/rank8-rup-signed-values/BENCHMARK.json create mode 100644 research/rank8-rup-signed-values/CHECKS.json create mode 100644 research/rank8-rup-signed-values/PROOF.md create mode 100644 research/rank8-rup-signed-values/README.md create mode 100644 research/rank8-rup-signed-values/SOURCES.json create mode 100644 research/rank8-rup-signed-values/TASK.json create mode 100644 research/rank8-rup-signed-values/VERIFY.json create mode 100644 research/rank8-rup-signed-values/adapter.py create mode 100644 research/rank8-rup-signed-values/benchmark.py create mode 100644 research/rank8-rup-signed-values/verify.py diff --git a/research/rank8-rup-signed-values/BENCHMARK.json b/research/rank8-rup-signed-values/BENCHMARK.json new file mode 100644 index 0000000000..6eb19fed92 --- /dev/null +++ b/research/rank8-rup-signed-values/BENCHMARK.json @@ -0,0 +1,90 @@ +{ + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "timer": "perf_counter_ns around completed subprocess and output validation", + "runs_per_side_per_unit": 5, + "order": "baseline,candidate repeated five times", + "units": [ + { + "unit": "P112", + "seconds": { + "baseline": [ + 14.258376833, + 14.881683875, + 14.733169458, + 15.05273, + 15.36443425 + ], + "candidate": [ + 9.883126333, + 9.580750792, + 10.003980833, + 10.372319291, + 10.272758542 + ] + }, + "medians": { + "baseline": 14.881683875, + "candidate": 10.003980833 + }, + "ranges": { + "baseline": [ + 14.258376833, + 15.36443425 + ], + "candidate": [ + 9.580750792, + 10.372319291 + ] + }, + "wall_time_reduction_percent": 32.776553264877094, + "errors": 0, + "scientific_checks_executed": 610, + "stdout_sha256": "5d259769ddf28097254546e6c368c1431bdafcbc31cad951a66a92b310dea41d", + "certificate_sha256": "a1f7ad167f54adef23f0e350732ce6fb5563a146d283284cfc30022fd7b9ef89" + }, + { + "unit": "P120", + "seconds": { + "baseline": [ + 6.822026333, + 7.03627825, + 7.088361542, + 6.766746167, + 6.652103792 + ], + "candidate": [ + 5.061493, + 5.050159959, + 5.0374595, + 4.933055375, + 4.774791791 + ] + }, + "medians": { + "baseline": 6.822026333, + "candidate": 5.0374595 + }, + "ranges": { + "baseline": [ + 6.652103792, + 7.088361542 + ], + "candidate": [ + 4.774791791, + 5.061493 + ] + }, + "wall_time_reduction_percent": 26.158896871558003, + "errors": 0, + "scientific_checks_executed": 410, + "stdout_sha256": "4a5350bb9fd78ecd41b236742a642452b7688ce24931a0d468728cf44ed6ba53", + "certificate_sha256": "0b8615f6117ec3971ca8ead529e03e926fc010fc5f9db3868562066fd890dff6" + } + ], + "files": { + "adapter.py": "d2c447166f60bd9246b282bca9fc67bbd4efbf5e9ff7cb3e763b7a9bbfc53957", + "benchmark.py": "46ec32047ec46f4140967638cd87e43923c562eda6c35a8d54ae432812140cf2", + "verify.py": "0672e429a4243d526ab3c84703fa9bb658777a13f79b730e5809563845ec4204" + } +} diff --git a/research/rank8-rup-signed-values/CHECKS.json b/research/rank8-rup-signed-values/CHECKS.json new file mode 100644 index 0000000000..39abfd6f3d --- /dev/null +++ b/research/rank8-rup-signed-values/CHECKS.json @@ -0,0 +1,65 @@ +{ + "generated_from": "separately timed registered commands", + "checks": [ + { + "command": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "seconds": 0.10024058306589723, + "exit": 0 + }, + { + "command": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "seconds": 0.11422341596335173, + "exit": 0 + }, + { + "command": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py", + "--unit", + "P112" + ], + "seconds": 24.499774541938677, + "exit": 0 + }, + { + "command": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py", + "--unit", + "P120" + ], + "seconds": 11.581851250026375, + "exit": 0 + } + ], + "files": { + "adapter.py": "d2c447166f60bd9246b282bca9fc67bbd4efbf5e9ff7cb3e763b7a9bbfc53957", + "verify.py": "0672e429a4243d526ab3c84703fa9bb658777a13f79b730e5809563845ec4204", + "benchmark.py": "46ec32047ec46f4140967638cd87e43923c562eda6c35a8d54ae432812140cf2", + "SOURCES.json": "1acaac56b312a59d26601e1648c9f4e85dc8c509a5a92b55784f2480bf537c59", + "VERIFY.json": "3b54db95b97ab47382f8033336296e2c7f742eeb7865e931546e465aecff3e97" + } +} diff --git a/research/rank8-rup-signed-values/PROOF.md b/research/rank8-rup-signed-values/PROOF.md new file mode 100644 index 0000000000..271031fd8b --- /dev/null +++ b/research/rank8-rup-signed-values/PROOF.md @@ -0,0 +1,131 @@ +# Direct signed-literal replay equivalence + +Claim type: scoped implementation-equivalence proof with exact finite conformance +and local performance evidence. This contribution was produced by Nick Petalas. +No new decoder theorem, supplier, kappa or multiplication theorem is claimed. + +## State relation + +The predecessor stores one ternary value `a[v]` per variable `1 <= v <= n`. +It evaluates a literal `l` as `a[abs(l)] * sign(l)`. Replace this by a list `s` +of length `2*n+1` satisfying + +``` +s[v] = a[v] +s[-v] = -a[v] +``` + +Python translates index `-v` to `2*n+1-v`. The positive slots are `1..n` and +the negative slots are `n+1..2*n`; they are disjoint and in bounds. Slot zero +is unused. Thus direct lookup `s[l]` equals the old literal value for both +signs, including the unassigned value zero. + +To assign literal `l` true, set `s[l],s[-l] = 1,-1`. This preserves the state +relation whether `l` is positive or negative. To erase its trail entry, set +both slots to zero. The empty initial table satisfies the relation. The case +`n=0` has no legal nonzero literal and is unchanged. + +## Trace induction + +`adapter.signed_source` changes exactly one authenticated function. It makes +seven bounded text replacements with checked occurrence counts: allocation, +removal of the old value helper, its two read sites, all three trail-reset +sites, and the two assignment sites. All source outside that function remains +byte-identical. Missing or changed replacement sites fail before execution. + +Induct over the original propagation trace. Corresponding seed literals have +the same value by the state relation. A conflict takes the same early exit +and clears the same trail. A new assignment updates both representations +consistently and appends the same literal to the same queue and trail. Each +clause visit therefore sees the same sequence of literal values. It takes +the same satisfied, multiple-unassigned, unit or conflict branch. Unit updates +and all normal-exit resets preserve the state relation. Consequently each +propagation call returns the same conflict decision and resets to the same +empty assignment. + +The parser, clause database, occurrence lists, top-level units, proof order, +deletions, duplicate handling, checked count, limit handling and error strings +are unchanged. Induction over proof lines gives identical complete return +triples. Every accepted and rejected RUP call is identical. The complete main +program therefore takes the same later branches, constructs the same certificate +and emits the same stdout. This argument covers the legal input contract, +not only the finite certificate fixtures used in the measurements. + +This is a representation improvement to the existing occurrence-list +algorithm. RUP soundness and the predecessor's mathematical decoder arguments +are cited premises. Neither is claimed as new or independently audited here. +The two-watched-literal algorithms in the P108/P110 successors and PR4360 are +prior alternative checkers; this change keeps PR1212's original visit order. + +## Cost and finite evidence + +The original complete P112 profile executes 205,432,164 `value` calls. The new +function has no value helper, so every one of those calls and their `abs`/sign +operations disappears on the equivalent trace. Parser range checks still use +`abs`; the claim does not remove every absolute-value operation. Assignment +and reset sites now write two slots. The ternary table grows from `n+1` to +`2*n+1` slots, an increase of exactly `n` list slots. The largest retained unit +has 4,032 variables, so the increase is 32,256 list-slot bytes on the measured +64-bit CPython host. No claim about total process memory reduction is made. + +The exact small-domain checks compare the real original and transformed +functions, including parser errors, comments, deletions, duplicates, empty +clauses, proof limits and repeated propagation resets. The complete checks +compare every stdout byte and every certificate field for P112 and P120. +Across those two commands all eight pinned proof files and all 61/41 retained +check lines remain reached. All live inputs are hash-checked before loading; +corruption of each of the nine live files and a missing proof fail admission. +A changed adapter replacement site also fails admission. Counts are emitted by +the checker, rather than handwritten as a receipt. + +Five alternating fresh-process measurements per side and live unit measure +complete CLI execution, including source authentication, geometry, every RUP +proof, rational calculations, existing rejection controls and output validation. +The benchmark refuses unequal stdout, unequal certificate objects, nonzero +exits, stderr or scientific failures. BENCHMARK.json contains the measured +samples, environment, source hashes and check counts. Profiling is separate +from the timed samples. No individual RUP microbenchmark is used as the +headline improvement. + +## Engineering scope + +All new loops range over pinned manifest entries, bounded source AST nodes, +fixed replacement sites or explicit finite test domains. Production replay +uses the predecessor's existing bounded files and variable domains. Each new +subprocess has a 150-second timeout and all registered checks have a +240-second outer limit or less. Source files are not mutated. Scratch is +owned by temporary directories or the benchmark's explicitly new output +folder. The verifier writes only stdout after temporary cleanup. + +Power of Ten rule 3 has a managed-runtime deviation: Python lists, AST nodes, +strings and exact integers allocate dynamically. The changed ternary table has +an explicit `2*n+1` capacity; the original clause and proof storage are unchanged. +Rule 8 has a constrained source-adapter deviation: exact SHA256-bound source, +one AST-selected function, seven checked replacement entries and unchanged +surrounding bytes. No supplied code is evaluated beyond the pinned predecessor +and these replacements. Existing predecessor recursion and large main function +are retained unchanged, not claimed as Power of Ten compliant. New functions +stay below 60 physical lines. Warning-strict normal/optimized checks provide +the available Python diagnostics; no external static analyzer or proof kernel +is claimed. + +## Limits and next question + +Timings are local performance evidence and are not portable runtime guarantees. +Default adoption, complete Linux workflow timing, scientific supplier admission, +selected cold replay, native all-columns, ownership, compiler, precision/tape +and analytic recovery obligations remain outside scope. Independent human and +formal proof-kernel review are unclaimed. The exact next adoption question is +recorded in TASK.json. Frozen predecessor files and the selected frontier stay +unchanged. + +## Credit + +Brett Halligan / burntout76's PR1212, head +`57099cb5684f38877f31d149d598801671a633db`, supplies the complete verifier, +proof certificates, theorem and failure controls. Its DreamingOfClouds / PR717, +themilkman216 / PR968, GamingPuzzled / PR620, Mihir Srivastava / PR845, +woklerx / PR998 and related decoder lineage retain full predecessor credit. +Classical signed arrays, induction and RUP are not claimed as novel algorithms. +The new adapter, equivalence argument, conformance and complete-command +performance measurements were produced by Nick Petalas. Apache-2.0. diff --git a/research/rank8-rup-signed-values/README.md b/research/rank8-rup-signed-values/README.md new file mode 100644 index 0000000000..f8e02637dd --- /dev/null +++ b/research/rank8-rup-signed-values/README.md @@ -0,0 +1,126 @@ +# Complete rank-eight replay with direct signed-literal values + +The complete PR1212 P112 primary command takes **32.78% less median wall time** +locally, from 14.881683875 s to 10.003980833 s. P120 takes 26.16% less time, +from 6.822026333 s to 5.037459500 s. Each comparison uses five alternating +fresh-process runs per side, with identical complete stdout and certificate +objects, zero errors and disjoint observed timing ranges. + +Claim type: scoped implementation-equivalence proof, exact finite conformance +and local performance evidence. The new contribution was produced by Nick +Petalas. No new decoder theorem or kappa is claimed. This package does not +audit or re-establish the predecessor's mathematical result. + +## Change and evidence + +An opt-in adapter stores both signs of each ternary assignment. It replaces the +205,432,164 literal-value helper calls in the profiled complete P112 run with +direct list indexing. Clause visits, the propagation queue, trail resets, +proof parsing, all scientific checks and every rejection control remain in +the same order. The old and new state representations are related by +`s[v]=a[v]` and `s[-v]=-a[v]`. [PROOF.md](PROOF.md) proves exact trace +equivalence by induction and records resource limits. + +[BENCHMARK.json](BENCHMARK.json) is generated by the measurement driver. It +contains every sample, environment, source hashes and check counts. Measured +on CPython 3.12.15, macOS 27.0.1 arm64, with 18 logical CPUs and load averages +1.92/2.07/1.85 before profiling. Other contributions could run on the host; +alternation limits the effect of shared-host drift. No timing threshold is +an acceptance gate in CI. + +| Complete command | Original range, seconds | New range, seconds | Repeated checks | +| --- | ---: | ---: | ---: | +| P112 | 14.2584 to 15.3644 | 9.5808 to 10.3723 | 610 | +| P120 | 6.6521 to 7.0884 | 4.7748 to 5.0615 | 410 | + +The separately profiled complete P112 run spent 37.382 of 43.688 profiled +seconds inside RUP calls. The value helper accounted for 16.708 cumulative +seconds. These instrumented durations identify the limiter and are not the +before/after timing samples. The measured reduction is below the fraction +of the path affected by the change. Both sides use the same interpreter, +flags, exact fixtures, proof data, process start and validation path. + +Local correctness evidence includes 12,030 signed-literal reads over every +ternary state through six variables; 9,282 exact original/transformed RUP +parser, decision and checked-count cases; and 11 source-admission controls. +The two complete CLIs retain all 61/41 check lines and replay all eight proof +files across the pair. Registered commands compare every stdout byte and +certificate field, not just a summary digest. The generated stdout receipt +binds the package files by SHA256. No handwritten receipt is used. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library only. +The local interpreter is shown exactly; another CPython 3.12 path can replace it. +Choose a new external scratch directory for generated files. + +```sh +export TMPDIR=/absolute/path/to/existing/scratch +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank8-rup-signed-values +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank8-rup-signed-values/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/rank8-rup-signed-values/adapter.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/rank8-rup-signed-values/adapter.py --live P120 +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank8-rup-signed-values/benchmark.py --output-dir "$TMPDIR/new-benchmark" +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank8-rup-signed-values --check-source-history +``` + +All four registered checks passed locally in 0.100 s, 0.114 s, 24.500 s and +11.582 s. [CHECKS.json](CHECKS.json) contains the generated timing record. +The registered runner emits `PASS_REGISTERED_RESEARCH_PACKAGE`. The new checker +emits `PASS_RANK8_RUP_SIGNED_VALUES`; the adapter retains the original +`PASS_COMPLEX_RANK8_DECODER_RIGIDITY` output. Benchmark output directories must +not already exist. The adapter reads the nine live files in SOURCES.json and +rejects source or proof changes before loading the predecessor. VERIFY.json +declares each file for CI invalidation. This is opt-in and changes no default +entry point or frozen predecessor bytes. + +## Scope and limits + +The signed table adds `n` list slots, at most 32,256 slot bytes on the measured +64-bit interpreter. It trades these additional writes and slots for fewer +Python calls. The only optimized artifact is the complete fixed PR1212 primary +CLI. Local wall-time results do not promise the same speedup on another host. +No decoder construction, physical supplier, new kappa or selected-frontier +change follows from this implementation improvement. + +Selected cold replay, default adoption, end-to-end Linux workflow timing, +Lean, Docker, independent human review and formal proof-kernel review are +unrun. All five selected framework assumptions remain. SOURCES.json pins the +historical card and selected record at canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`; those files are provenance rather +than live scientific dependencies. The replay-runtime card is refined to +this measured implementation task. Build the Lever determined the reusable +adapter and benchmark; Prove It Works determined complete CLI/certificate +comparison rather than a helper-only timing. One hypothesis was kept; none +was rejected or extended after the first measured improvement. + +Live open PRs, handoffs, main/merged RUP and rigidity searches, this account's +recent submissions and local reservations were checked. The overlap helper +covered 539 open PRs and 6,564 Discussion records with complete pagination, +but only 133 of 8,917 main README paths in this sparse checkout. Direct main +README searches supplemented that cache. Arbitrary diffs and unpublished work +remain limits. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372279). + +## Open next questions + +Should an explicit successor adopt the signed table by default? First retain +its source binding and run the complete workflow on Linux. The present opt-in +adapter leaves every historical checker unchanged; default adoption and a +broader workflow cost are not supplied. [TASK.json](TASK.json) records the +question, relevance, first step and blocker. + +## Credit + +Brett Halligan / burntout76's [PR1212](https://github.com/CrocSwap/integer-mult-bounds/pull/1212), +head `57099cb5684f38877f31d149d598801671a633db`, supplies the original verifier, +mathematical results, proof certificates and controls. Its retained decoder +lineage includes DreamingOfClouds / PR717, themilkman216 / PR968, +GamingPuzzled / PR620, Mihir Srivastava / PR845 and woklerx / PR998. Their +claims and credit are unchanged. Classical RUP, signed arrays and induction +are credited as existing methods. The P108/P110 successors and pinterbanget's +PR4360 already contain two-watched-literal checkers; this contribution changes +the representation of PR1212's original occurrence-list checker instead. + +The adapter, equivalence argument, conformance checks and complete-command +measurements were produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/rank8-rup-signed-values/SOURCES.json b/research/rank8-rup-signed-values/SOURCES.json new file mode 100644 index 0000000000..080ec936f4 --- /dev/null +++ b/research/rank8-rup-signed-values/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/complex-rank8-decoder-rigidity/verify.py", + "usage": "input", + "git_blob": "c3707b0993d04b78e20c5d3512d370495690df8b", + "sha256": "7dd78f3deacf6067a30d6f195ca09dd98db7d9e4f68eda7cad9868f407608edd" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P104-11111111.drup", + "usage": "input", + "git_blob": "e71c3c93deeb43a08772614fc439bd4b7bd08a24", + "sha256": "e33407bad56df4bad7415a39afe3e897ff86be31dc79b2175bcb55b9799f5c2d" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P104-2222.drup", + "usage": "input", + "git_blob": "c4dac56c9928f5cbdc91c27af17fbab691949844", + "sha256": "98318a46c721a615f6618b6981ecb157a9d9b92e2b914d70dfb3f68a6f075db4" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P104-44.drup", + "usage": "input", + "git_blob": "976ce90f0dc9b00e820cc3ea84c1dd26ca4fa2f3", + "sha256": "6e940db9f8b6c16c42cad4b0713b67c8532f492fdfb56985ee74a89400632ed3" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P111.drup", + "usage": "input", + "git_blob": "31f25bc28c8f065439c063ce91309267ab1edbf7", + "sha256": "fec7c8c3e90ebe1c17b9808f4c0efb93733e34a487193018b21c995c41e7c980" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P112-two-diag.drup", + "usage": "input", + "git_blob": "a7a192b83327b90f986010084c1dac059dd72581", + "sha256": "bb0de4f68a050828e1ae77e9d865c07e473090ed3abcd41f35dcdf6eed836c61" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P112.drup", + "usage": "input", + "git_blob": "c601dc927d4da14abb07028b2bfd9ab529884c83", + "sha256": "d3997e05c3106c357f47181bcba3609f30c86a2ee0c7d9bad3a6369c2d9b61da" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P120-two-diag.drup", + "usage": "input", + "git_blob": "1b360bc5d4c7961c94533197e2ab05fa7e6edb97", + "sha256": "43b7f584f85d6cd5f4129e5540ee4e16e6c5662d1844c3e5192e81ab2a272166" + }, + { + "path": "research/complex-rank8-decoder-rigidity/proof-P120.drup", + "usage": "input", + "git_blob": "7beba7cbce4eaca667c5d0b5b33f50558581295e", + "sha256": "dbc96c6478b2dfc75649a3779866dffc5cbf6d9ecc0594ea6abd0b66afd3d034" + }, + { + "path": "research/complex-rank8-decoder-rigidity/README.md", + "usage": "provenance", + "git_blob": "1bf959ace7299ef0f7ea5bdb5d33e77fd38c1d0f", + "sha256": "2904cd26666d9dd386084ad0912fa41ef0abb48fbd3d1f749f862ccf6f177269" + }, + { + "path": "research/complex-rank8-decoder-rigidity/PROOF.md", + "usage": "provenance", + "git_blob": "5940f280c1ffe46148f4a75ab0107933f8f9ce29", + "sha256": "bccab452803cb0094685c298fe4fba5ceeddf9d6158a6af0b584712391db14c9" + } + ] +} diff --git a/research/rank8-rup-signed-values/TASK.json b/research/rank8-rup-signed-values/TASK.json new file mode 100644 index 0000000000..928d32b560 --- /dev/null +++ b/research/rank8-rup-signed-values/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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 direct signed-literal representation for PR1212's complete P112/P120 primary replay, with exact behavior equivalence and fresh-process measurements.", + "scope_change_reason": "The replay-runtime card is narrowed to one measured literal-evaluation bottleneck. This is implementation research, not a scientific re-audit of the predecessor.", + "bottleneck_link": "Lower complete verification cost without losing source invalidation or any scientific checks supports review throughput. No supplier or exponent changes.", + "budget_minutes": 60, + "stop_rule": "Stop at the first complete-command improvement outside observed timing ranges with unchanged stdout and full certificate objects.", + "outcome": "completed", + "evidence": "PROOF.md, generated BENCHMARK.json and CHECKS.json, complete registered replay, exact committed-byte and declared source-history preflight.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Should a successor checker adopt the signed table as its default representation?", + "why_it_matters": "The opt-in adapter improves complete replay without changing frozen historical evidence.", + "first_step": "Bind a default-adoption change to a new explicit successor and measure its entire workflow on Linux.", + "blocked_by": "This contribution leaves every predecessor and default entry point unchanged." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372279", + "preserved_branch": "research/w10-1102h-frontier", + "preserved_head": "277ff2c230937460aae5d2b19d83be37d0d60a5b", + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "canonical_refresh_utc": "2026-11-03T11:11:20Z" +} diff --git a/research/rank8-rup-signed-values/VERIFY.json b/research/rank8-rup-signed-values/VERIFY.json new file mode 100644 index 0000000000..81766270bf --- /dev/null +++ b/research/rank8-rup-signed-values/VERIFY.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-rank8-decoder-rigidity/verify.py", + "research/complex-rank8-decoder-rigidity/proof-P104-11111111.drup", + "research/complex-rank8-decoder-rigidity/proof-P104-2222.drup", + "research/complex-rank8-decoder-rigidity/proof-P104-44.drup", + "research/complex-rank8-decoder-rigidity/proof-P111.drup", + "research/complex-rank8-decoder-rigidity/proof-P112-two-diag.drup", + "research/complex-rank8-decoder-rigidity/proof-P112.drup", + "research/complex-rank8-decoder-rigidity/proof-P120-two-diag.drup", + "research/complex-rank8-decoder-rigidity/proof-P120.drup" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Signed-table invariant, exact RUP parser/decision differential and every live source/proof corruption control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same explicit acceptance gates remain active under optimized Python." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py", + "--unit", + "P112" + ], + "timeout_seconds": 240, + "checks": "Complete original and candidate P112 CLI, every existing scientific/rejection check, exact stdout and full certificate equality." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py", + "--unit", + "P120" + ], + "timeout_seconds": 240, + "checks": "Complete original and candidate P120 CLI, every existing scientific/rejection check, exact stdout and full certificate equality." + } + ] +} diff --git a/research/rank8-rup-signed-values/adapter.py b/research/rank8-rup-signed-values/adapter.py new file mode 100644 index 0000000000..5c0aa66311 --- /dev/null +++ b/research/rank8-rup-signed-values/adapter.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Opt-in, byte-bound literal-table adapter for PR1212's complete CLI.""" +from __future__ import annotations + +import ast +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/complex-rank8-decoder-rigidity/verify.py" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def authenticated_source(root: Path = ROOT) -> tuple[Path, str]: + manifest = json.loads((HERE / "SOURCES.json").read_text()) + source_path = root / SOURCE + for entry in manifest["files"]: + if entry["usage"] == "input": + path = root / entry["path"] + require(path.is_file() and not path.is_symlink(), f"missing input: {path}") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + require(digest == entry["sha256"], f"input hash mismatch: {entry['path']}") + return source_path, source_path.read_text() + + +def signed_source(source: str) -> str: + """Change only the bounded, authenticated RUP function.""" + functions = [node for node in ast.parse(source).body + if isinstance(node, ast.FunctionDef) and node.name == "rup_check"] + require(len(functions) == 1, "expected exactly one RUP function") + function = functions[0] + lines = source.splitlines(keepends=True) + original = "".join(lines[function.lineno - 1:function.end_lineno]) + changed = original + replacements = ( + ("assign = [0] * (nvars + 1)", "assign = [0] * (2 * nvars + 1)", 1), + (" def value(lit):\n return assign[abs(lit)] * (1 if lit > 0 else -1)\n\n", "", 1), + ("v = value(lit)", "v = assign[lit]", 1), + ("v = value(l)", "v = assign[l]", 1), + ("assign[abs(l)] = 0", "assign[l] = assign[-l] = 0", 3), + ("assign[abs(lit)] = 1 if lit > 0 else -1", "assign[lit], assign[-lit] = 1, -1", 1), + ("assign[abs(unassigned)] = 1 if unassigned > 0 else -1", "assign[unassigned], assign[-unassigned] = 1, -1", 1), + ) + for before, after, count in replacements: + require(changed.count(before) == count, f"adapter replacement mismatch: {before}") + changed = changed.replace(before, after) + require("value(" not in changed and "assign[abs(" not in changed, + "unconverted literal access") + return "".join(lines[:function.lineno - 1]) + changed + "".join(lines[function.end_lineno:]) + + +def load_source(optimized: bool = True, root: Path = ROOT) -> dict: + path, source = authenticated_source(root) + if optimized: + source = signed_source(source) + namespace = {"__name__": "rank8_replay_source", "__file__": str(path)} + exec(compile(source, str(path), "exec"), namespace) + return namespace + + +def main() -> int: + try: + namespace = load_source() + return namespace["main"]() + except (OSError, ValueError, SyntaxError) as error: + print(f"FAIL_RANK8_SIGNED_VALUES: {error}", file=sys.stderr) + return 2 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/rank8-rup-signed-values/benchmark.py b/research/rank8-rup-signed-values/benchmark.py new file mode 100644 index 0000000000..54933225c2 --- /dev/null +++ b/research/rank8-rup-signed-values/benchmark.py @@ -0,0 +1,68 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Measure five alternating complete fresh-process runs per side and unit.""" +from __future__ import annotations + +import argparse +import hashlib +import importlib.util +import json +import platform +import statistics +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("signed_verify", HERE / "verify.py") +if spec is None or spec.loader is None: + raise RuntimeError("cannot load verification driver") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +def measure(unit: str, output: Path) -> dict: + elapsed = {"baseline": [], "candidate": []} + reference = None + checked = 0 + for index in range(5): + for engine in ("baseline", "candidate"): + path = output / f"{unit}-{index}-{engine}.json" + start = time.perf_counter_ns() + stdout, certificate = verify.run(engine, unit, path) + seconds = (time.perf_counter_ns() - start) / 1e9 + result = stdout, certificate + if reference is None: + reference = result + verify.require(result == reference, "benchmark output/certificate mismatch") + elapsed[engine].append(seconds) + checked += len(certificate["log"]) + verify.require(reference is not None, "empty workload") + medians = {engine: statistics.median(values) for engine, values in elapsed.items()} + return {"unit": unit, "seconds": elapsed, "medians": medians, + "ranges": {engine: [min(values), max(values)] for engine, values in elapsed.items()}, + "wall_time_reduction_percent": 100 * (1 - medians["candidate"] / medians["baseline"]), + "errors": 0, "scientific_checks_executed": checked, + "stdout_sha256": hashlib.sha256(reference[0]).hexdigest(), + "certificate_sha256": hashlib.sha256(json.dumps(reference[1], sort_keys=True).encode()).hexdigest()} + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--output-dir", type=Path, required=True) + args = parser.parse_args() + args.output_dir.mkdir(parents=True, exist_ok=False) + verify.adapter.authenticated_source() + result = {"python": sys.version, "platform": platform.platform(), + "timer": "perf_counter_ns around completed subprocess and output validation", + "runs_per_side_per_unit": 5, "order": "baseline,candidate repeated five times", + "units": [measure(unit, args.output_dir) for unit in ("P112", "P120")]} + result["files"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.glob("*.py"))} + (args.output_dir / "BENCHMARK.json").write_text(json.dumps(result, indent=2) + "\n") + print(json.dumps(result, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/rank8-rup-signed-values/verify.py b/research/rank8-rup-signed-values/verify.py new file mode 100644 index 0000000000..bb72d693d8 --- /dev/null +++ b/research/rank8-rup-signed-values/verify.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check the new representation and complete retained CLI equivalence.""" +from __future__ import annotations + +import argparse +import hashlib +import importlib.util +import itertools +import json +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("signed_adapter", HERE / "adapter.py") +if spec is None or spec.loader is None: + raise RuntimeError("cannot load local adapter") +adapter = importlib.util.module_from_spec(spec) +spec.loader.exec_module(adapter) +require = adapter.require + + +def representation_controls() -> int: + reads = 0 + for size in range(1, 7): + for state in itertools.product((-1, 0, 1), repeat=size): + values = [0] * (2 * size + 1) + for index, value in enumerate(state, 1): + values[index], values[-index] = value, -value + for literal in range(-size, size + 1): + if literal: + expected = state[abs(literal) - 1] * (1 if literal > 0 else -1) + require(values[literal] == expected, "signed value invariant") + reads += 1 + for index in range(1, size + 1): + values[index] = values[-index] = 0 + require(not any(values), "trail reset invariant") + return reads + + +def differential_controls() -> int: + old = adapter.load_source(False)["rup_check"] + new = adapter.load_source(True)["rup_check"] + count = 0 + # Every normalized two-variable clause and every ordered formula of <=2 clauses. + clauses = [tuple(sign * (i + 1) for i, sign in enumerate(signs) if sign) + for signs in itertools.product((-1, 0, 1), repeat=2)] + proofs = [" ".join(map(str, (*clause, 0))) for clause in clauses] + proofs += ["", "c comment", "d 1 0", "x 0", "1", "0 0", "3 0", "1 1 0"] + formulas = [()] + [(clause,) for clause in clauses] + formulas += list(itertools.product(clauses, repeat=2)) + for formula in formulas: + for first in proofs: + for second in ("0", "1 0", "-1 0"): + for limit in (None, 1): + lines = [first, second] + require(old(formula, 2, lines, limit) == new(formula, 2, lines, limit), + "RUP decision/parser/count mismatch") + count += 1 + return count + + +def admission_controls(scratch: Path) -> int: + path, source = adapter.authenticated_source() + changed = source.replace("v = value(l)", "v = broken(l)", 1) + try: + adapter.signed_source(changed) + except ValueError: + pass + else: + raise ValueError("changed replacement site accepted") + manifest = json.loads((HERE / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + controls = 1 + with tempfile.TemporaryDirectory(dir=scratch, prefix="source-controls-") as name: + root = Path(name) + for row in inputs: + destination = root / row["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes((adapter.ROOT / row["path"]).read_bytes()) + for row in inputs: + destination = root / row["path"] + original = destination.read_bytes() + destination.write_bytes(original + b"\ncorruption\n") + try: + adapter.authenticated_source(root) + except ValueError: + controls += 1 + else: + raise ValueError(f"changed input accepted: {row['path']}") + destination.write_bytes(original) + missing = root / inputs[-1]["path"] + missing.unlink() + try: + adapter.authenticated_source(root) + except ValueError: + controls += 1 + else: + raise ValueError("missing proof accepted") + require(path.is_file(), "source disappeared") + return controls + + +def command(engine: str, unit: str, output: Path) -> list[str]: + path = adapter.ROOT / adapter.SOURCE if engine == "baseline" else HERE / "adapter.py" + return [sys.executable, "-I", "-B", str(path), "--live", unit, "--out", str(output)] + + +def run(engine: str, unit: str, output: Path) -> tuple[bytes, dict]: + completed = subprocess.run(command(engine, unit, output), capture_output=True, + timeout=150, check=False) + require(completed.returncode == 0, + f"{engine}/{unit} exit {completed.returncode}: {completed.stderr[-2000:]!r}") + require(not completed.stderr, f"unexpected stderr: {completed.stderr!r}") + payload = json.loads(output.read_text()) + require(payload["fails"] == [], "retained scientific check failed") + require(b"PASS_COMPLEX_RANK8_DECODER_RIGIDITY:" in completed.stdout, + "incomplete retained replay") + return completed.stdout, payload + + +def complete_equivalence(unit: str, scratch: Path) -> dict: + adapter.authenticated_source() + with tempfile.TemporaryDirectory(dir=scratch, prefix=f"complete-{unit}-") as name: + root = Path(name) + before, left = run("baseline", unit, root / "baseline.json") + after, right = run("candidate", unit, root / "candidate.json") + require(before == after and left == right, "complete output/certificate mismatch") + return {"unit": unit, "checks": len(left["log"]), "fails": 0, + "stdout_sha256": hashlib.sha256(before).hexdigest(), + "certificate_sha256": hashlib.sha256(json.dumps(left, sort_keys=True).encode()).hexdigest()} + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--unit", choices=("P112", "P120")) + args = parser.parse_args() + scratch = Path(tempfile.gettempdir()) + result = {"status": "PASS_RANK8_RUP_SIGNED_VALUES", "no_new_kappa": True} + if args.unit: + result["complete"] = complete_equivalence(args.unit, scratch) + else: + result["literal_reads"] = representation_controls() + result["differential_cases"] = differential_controls() + result["admission_controls"] = admission_controls(scratch) + result["files"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print(json.dumps(result, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())