diff --git a/research/p104-fold-elimination/BENCHMARK.json b/research/p104-fold-elimination/BENCHMARK.json new file mode 100644 index 0000000000..f602ec06d2 --- /dev/null +++ b/research/p104-fold-elimination/BENCHMARK.json @@ -0,0 +1,216 @@ +{ + "schema": "p104-fold-benchmark/1", + "runs": [ + { + "mode": "baseline", + "seconds": 129.89114750013687, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "candidate", + "seconds": 89.69574729190208, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "baseline", + "seconds": 132.10526695800945, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "candidate", + "seconds": 91.40650762501173, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "baseline", + "seconds": 127.85968495812267, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "candidate", + "seconds": 89.58335066703148, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "baseline", + "seconds": 125.20299625000916, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "candidate", + "seconds": 88.87156916595995, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "baseline", + "seconds": 123.44024070887826, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + }, + { + "mode": "candidate", + "seconds": 86.47449304186739, + "word_sha256": "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b", + "events": 22821, + "step": { + "site": "H705", + "kappa": 0.003126477877758, + "base": 0.003125811557912, + "diff": 6.663e-07, + "variant": [ + "--relocate", + "770:13614:15597" + ], + "status": "FOLDED" + }, + "exit_code": 0 + } + ], + "summary": { + "baseline": { + "median_seconds": 127.85968495812267, + "range_seconds": [ + 123.44024070887826, + 132.10526695800945 + ] + }, + "candidate": { + "median_seconds": 89.58335066703148, + "range_seconds": [ + 86.47449304186739, + 91.40650762501173 + ] + } + }, + "errors": 0, + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "source_head": "445fb9124eb3fcb5d4f342c476b9ae3637f185aa", + "hashes": { + "benchmark.py": "3352e3d081228856eec45ba888d2b5b37f99bb5b04e011d8d0fe1251a2e6e684", + "iob_entry.py": "144922805173646cfdde95c19b6fd475fa5dcfe0bcd8f1c23667a7890179e58b", + "run.py": "5ccd43f7bd968736c28040b87d770a4a420915a501f9bb6efe13b8ed740ad630", + "runtime.py": "c7a1bcb240db5e89218f634eb5cd80713377eb26febfb91ce54956693b81f37d", + "solver.py": "2118d63937d4f220a53807170793b2223516aafe14b74fb25b04ac634e3b9e63", + "verify.py": "218519b64979f314ff321cc5229ddcacaadabff50ac2b9dbf513a44207cb0a01" + }, + "retained_manifest_sha256": "b9971dc880602974febf22b23efefe45c20fb8a317ef2eb7f4d03964ef28ac8d", + "timed_region": "Fresh process through completed first fold, including source authentication, both attempted variants, legality and output serialization." +} diff --git a/research/p104-fold-elimination/ENVIRONMENT.json b/research/p104-fold-elimination/ENVIRONMENT.json new file mode 100644 index 0000000000..fef82e4212 --- /dev/null +++ b/research/p104-fold-elimination/ENVIRONMENT.json @@ -0,0 +1,14 @@ +{ + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "numpy": "2.5.4", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "logical_cpus": 18, + "shared_host": true, + "load_average_during_series": [ + 3.14306640625, + 3.14501953125, + 2.90966796875 + ], + "checked_at_utc": "2026-10-29T13:23:20.335269+00:00" +} diff --git a/research/p104-fold-elimination/PROFILE.json b/research/p104-fold-elimination/PROFILE.json new file mode 100644 index 0000000000..965bd97997 --- /dev/null +++ b/research/p104-fold-elimination/PROFILE.json @@ -0,0 +1,190 @@ +{ + "schema": "p104-fold-profile/1", + "source_head": "445fb9124eb3fcb5d4f342c476b9ae3637f185aa", + "profile_sha256": "99db17280c6b5a84f3a3172bb0ed18edb3ab3dd85b8b20980b7080a3524a4a10", + "total_seconds": 83.32374433300002, + "total_calls": 7346560, + "entries": [ + { + "file": "~", + "line": 0, + "function": "", + "primitive_calls": 1, + "calls": 124, + "self_seconds": 0.000226369, + "cumulative_seconds": 83.32378641700001 + }, + { + "file": "iob2.py", + "line": 1, + "function": "", + "primitive_calls": 1, + "calls": 1, + "self_seconds": 0.002460706, + "cumulative_seconds": 83.323781041 + }, + { + "file": "iob2.py", + "line": 75, + "function": "main", + "primitive_calls": 1, + "calls": 1, + "self_seconds": 0.040390543, + "cumulative_seconds": 83.264762417 + }, + { + "file": "iob2.py", + "line": 380, + "function": "solve_with", + "primitive_calls": 2, + "calls": 2, + "self_seconds": 0.018040167000000003, + "cumulative_seconds": 75.640903625 + }, + { + "file": "rp.py", + "line": 167, + "function": "solve", + "primitive_calls": 2, + "calls": 2, + "self_seconds": 0.023911166, + "cumulative_seconds": 75.622842417 + }, + { + "file": "rp.py", + "line": 150, + "function": "rref", + "primitive_calls": 2, + "calls": 2, + "self_seconds": 75.45015759200001, + "cumulative_seconds": 75.598910167 + }, + { + "file": "iob2.py", + "line": 342, + "function": "linsys", + "primitive_calls": 3, + "calls": 3, + "self_seconds": 0.281283653, + "cumulative_seconds": 7.0969939580000005 + }, + { + "file": "iob2.py", + "line": 365, + "function": "mm", + "primitive_calls": 9, + "calls": 9, + "self_seconds": 5.876607252, + "cumulative_seconds": 5.879811544000001 + }, + { + "file": "~", + "line": 0, + "function": "", + "primitive_calls": 8820, + "calls": 8820, + "self_seconds": 0.08540684600000001, + "cumulative_seconds": 0.464110746 + }, + { + "file": "iob2.py", + "line": 374, + "function": "", + "primitive_calls": 3185355, + "calls": 3185355, + "self_seconds": 0.378593489, + "cumulative_seconds": 0.378593489 + }, + { + "file": "rp.py", + "line": 32, + "function": "replay", + "primitive_calls": 4, + "calls": 4, + "self_seconds": 0.01064989, + "cumulative_seconds": 0.219267958 + }, + { + "file": "routing.py", + "line": 65, + "function": "gcols", + "primitive_calls": 3, + "calls": 3, + "self_seconds": 0.202644393, + "cumulative_seconds": 0.218078666 + }, + { + "file": "iob2.py", + "line": 43, + "function": "sym_events", + "primitive_calls": 1, + "calls": 1, + "self_seconds": 0.016566320000000002, + "cumulative_seconds": 0.21751679200000001 + }, + { + "file": "rp.py", + "line": 24, + "function": "step", + "primitive_calls": 99742, + "calls": 99742, + "self_seconds": 0.19580799200000001, + "cumulative_seconds": 0.20605289000000002 + }, + { + "file": "legal.py", + "line": 66, + "function": "check", + "primitive_calls": 1, + "calls": 1, + "self_seconds": 0.037784635000000004, + "cumulative_seconds": 0.175833167 + }, + { + "file": "iob2.py", + "line": 51, + "function": "add", + "primitive_calls": 36854, + "calls": 36854, + "self_seconds": 0.031683457000000005, + "cumulative_seconds": 0.153815863 + }, + { + "file": "fractions.py", + "line": 613, + "function": "forward", + "primitive_calls": 134259, + "calls": 134259, + "self_seconds": 0.024357564, + "cumulative_seconds": 0.10362154300000001 + }, + { + "file": "numeric.py", + "line": 675, + "function": "flatnonzero", + "primitive_calls": 9392, + "calls": 9392, + "self_seconds": 0.010900678, + "cumulative_seconds": 0.091276432 + }, + { + "file": "fractions.py", + "line": 186, + "function": "__new__", + "primitive_calls": 91605, + "calls": 91605, + "self_seconds": 0.048266164, + "cumulative_seconds": 0.09003643400000001 + }, + { + "file": "~", + "line": 0, + "function": "", + "primitive_calls": 20907, + "calls": 20907, + "self_seconds": 0.058941859000000006, + "cumulative_seconds": 0.058941859000000006 + } + ], + "scope": "Untimed discovery profile of the first relocation variant, which correctly rejects as illegal. Separate from the repeated complete-fold benchmark." +} diff --git a/research/p104-fold-elimination/PROOF.md b/research/p104-fold-elimination/PROOF.md new file mode 100644 index 0000000000..c1a6d42266 --- /dev/null +++ b/research/p104-fold-elimination/PROOF.md @@ -0,0 +1,82 @@ +# Solver equivalence and scope + +The mathematical background is ordinary Gaussian elimination over a prime +field. The contribution is its application to the measured P104 fold bottleneck, +the opt-in substitution and the complete-command evidence. No priority claim +is made for the elimination algorithm. + +Let p = 2147483647. For an m by n integer matrix A and vector b, the retained +`rp.solve` returns None when Ax = b is inconsistent. Otherwise it selects pivot +columns from left to right and sets all free coordinates to zero. It obtains +that solution by fully reducing the augmented matrix. + +The new solver eliminates only below each pivot, then substitutes backwards. +Both algorithms perform the same row selection, normalization and elimination +on the unprocessed rows. Eliminating entries above a pivot has no effect on +those rows. Induction on the pivot index therefore gives the same pivot columns +and the same unprocessed submatrix in both algorithms. Rows below the last +pivot have zero coefficient entries. A nonzero right-hand entry on such a row +is exactly the inconsistency condition. The original augmented-matrix reduction +detects this by selecting the augmented column as a pivot. + +In the consistent case, restrict A to its selected pivot columns. These columns +are independent and span its column space. Thus there is exactly one solution +supported on those columns. Back substitution and full reduction both produce +that solution. Every other coordinate is zero in both outputs. This covers +rank deficiency, zero rows, zero columns and empty matrices. Neither algorithm +needs an inverse of a zero pivot. + +All calculations in the replacement use signed 64-bit integers after modular +reduction. A product of residues is less than p squared, which is below 2^62. +The elimination subtraction occurs after reducing its product, so its absolute +value is below p. During back substitution, at most 4096 reduced products are +summed, giving a sum below 4096p and hence below 2^43. There is no signed overflow +in these operations. Each matrix dimension is checked to be at most 4096 before +the working matrix is allocated. The supported interface accepts integer NumPy +arrays and copies its inputs; it rejects noninteger or incompatible arrays. + +The substitution changes only the function called as `rp.solve`. The source +coefficient construction, projection seed, candidate order, Newton iterations, +rational reconstruction, builder, legality check and pricer retain their exact +bytes. Equality of the returned solution, including None, therefore preserves +every later deterministic computation in this pinned command. The finite replay +checks the complete emitted word as JSON, rather than compressed container bytes. +All ten timed commands produce the same canonical word digest and fold status. + +This is not a proof that the retained toolkit's projection or legality oracle +certifies every mathematical obligation of a P104 supplier. Their scope is +inherited. No native-phase, physical caller, uniform compiler, precision, BIT, +outer or selected-frontier result is established here. + +## Resource and code constraints + +All new loops have finite bounds: at most 4096 pivot or substitution steps, +50 retained source entries, 1234 small-system fixtures, five rejection controls, +two integration commands and at most ten benchmark pairs. Each child command +has a timeout. Every new function is below 60 physical lines. New verification +conditions use explicit exceptions and remain active under optimization. + +Power of Ten rule 3 requires a managed-runtime deviation in `solver.py` and its +NumPy callers. Python and NumPy allocate arrays and temporary values during +elimination. The dimension cap bounds each array by 4096 by 4097 entries and +the implementation has no unbounded queue or retained history. A working array +uses less than 129 MiB; the source matrix and elimination temporaries add further +bounded arrays. This is a capacity argument, not a measured peak-RSS claim. +Replacing NumPy with a fixed-buffer implementation would be a separate change. + +Rule 9 requires one explicit integration deviation in `runtime.install`. +The opt-in adapter binds `rp.solve` to the replacement function in a fresh +process. Its only possible targets are the retained baseline and `solver.solve`. +The retained files are authenticated before import, and no predecessor file is +edited. The baseline/candidate complete-command comparisons exercise both +targets. A future toolkit-owned parameter for the solver could remove this +binding step. + +The unchanged predecessor closure has its original coding conventions. This +package does not refactor that code or claim it satisfies the new-code rules. +Warning-strict execution reports unclosed-profile-file ResourceWarnings in +`tkcommon._load_data_profiles`. The files are closed by their finalizers; the +warning is not suppressed. Rule 10's limitation is confined to this frozen +predecessor import, whose exact bytes must remain preserved. A toolkit-owned +change to scoped profile reads would remove it. New-code syntax and warning +checks remain enabled. diff --git a/research/p104-fold-elimination/README.md b/research/p104-fold-elimination/README.md new file mode 100644 index 0000000000..ee408b6f4e --- /dev/null +++ b/research/p104-fold-elimination/README.md @@ -0,0 +1,104 @@ +# Faster exact P104 fold solves + +This contribution was produced by Nick Petalas. It replaces the repeated +Gauss-Jordan solves in one actual P104 shadow-relay fold with forward elimination +and back substitution. The complete first fold still rejects its first variant, +accepts its second variant and emits the identical 22821-event word. The measured +complete-command results are in [BENCHMARK.json](BENCHMARK.json). + +The claim type is an empirical tooling improvement with a scoped solver +equivalence proof and finite regression evidence. No new kappa is claimed. +The output word and its construction are predecessor work. + +## Result and evidence + +Five alternating complete-command pairs give median wall time **127.86 seconds +before and 89.58 seconds after, a 29.94% reduction**. Baseline range is +123.44 to 132.11 seconds; candidate range is 86.47 to 91.41 seconds. All ten +commands succeed and emit the same complete word and fold report. + +[PROFILE.json](PROFILE.json) records an untimed discovery profile. The +retained solver consumes 75.6 of 83.3 profiled seconds. That profile is the first +relocation variant, which correctly rejects as illegal. It is excluded from +the repeated timings. [PROOF.md](PROOF.md) explains why the replacement returns +the identical canonical basic solution over the source prime field, including +inconsistent systems and free variables. + +[benchmark.py](benchmark.py) runs five alternating baseline/candidate pairs of +the complete first fold. Its timed region includes fresh-process startup, +source authentication, census and planning, both attempted variants, all retained +checks and output serialization. Every command must succeed and produce the +same full canonical word and fold status. The generated receipt binds the +implementation hashes, environment, samples and output. It is not a hand-written +receipt. Single-host timings do not predict another machine's speedup. + +[verify.py](verify.py) compares 1234 complete small systems with the retained +solver, checks the returned solutions and input preservation, rejects malformed +inputs and a changed source, and runs the complete accepted solver variant in +both modes. The registered checks repeat this with optimization enabled. + +## Reproduction + +Run from the repository root with CPython 3.12 and NumPy 2.5.4: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-fold-elimination +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-fold-elimination --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-fold-elimination/verify.py +``` + +To repeat the timings, choose an external scratch directory and extract the +retained closure there. The output directory passed to the benchmark must not +already exist: + +```sh +tar -xzf research/p104-fold-elimination/toolkit-closure.tar.gz -C "$fold_source_dir" +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-fold-elimination/benchmark.py "$fold_source_dir" "$fold_timing_dir" --pairs 5 +``` + +For a single accepted solve, use `run.py baseline SOURCE_DIR OUTPUT.json.gz` or +`run.py candidate SOURCE_DIR OUTPUT.json.gz`. Add `--whole-fold` to include the +preceding rejected variant and complete first-step driver. All outputs and +toolkit work files go beside the supplied output path. + +## Sources and limitations + +The source question is Open next question 2 of DreamingOfClouds' [PR6170](https://github.com/CrocSwap/integer-mult-bounds/pull/6170), +at `445fb9124eb3fcb5d4f342c476b9ae3637f185aa`. The measured bottleneck justified +elimination in place of the question's suggested rule caching. The package +retains a minimal 50-file closure, 491345 uncompressed bytes. Every retained +file has its original Git blob and SHA256 in [RETAINED.json](RETAINED.json). +The archive is authenticated before extraction, and source files are checked +before use. The original README and all retained headers preserve their credit. +The published source head is identified by its Git tree and downloaded blob +hashes; it is not added as a local ref or represented as admitted main-line work. + +DreamingOfClouds retains the toolkit, fold rule and PR6030/6143/6144 construction +credit. Ali Romman retains PR6167 and the retained-operand pass. The P104, +native, helper, caller, compiler and BIT predecessors retain their attribution +in the original README. Gaussian elimination is standard background; the new +contribution is the measured integration and its equivalence evidence. + +The solver supports dimensions at most 4096. The performance measurement covers +the first H705 fold on the shipped PR6030 word, not all sites, arbitrary words, +or the complete rebuild. The retained projection, legality oracle and prices +keep their existing scope. This is not a supplier audit, native replay, finite +certificate of a multiplication theorem or frontier update. All five selected +framework assumptions remain. Independent human and formal proof-kernel review +are unclaimed. + +Warning-strict controls expose retained `tkcommon.py` ResourceWarnings from +`json.load(open(f))` while loading profile files. These are unraisable file-finalizer +warnings in unchanged predecessor code. They are not suppressed, and the checks +are not described as warning-clean. New files use scoped file operations. + +## Open next questions + +- Does the same substitution help every accepted fold and the complete rebuild? + First compare each emitted word and acceptance status across that full path. + A separately budgeted run and larger-system coverage remain necessary. +- Can exact factorization reuse help successive Newton systems? First establish + an equality or controlled update relation between the two actual matrices. + No such relation is supplied here. + +The structured versions and blockers are in [TASK.json](TASK.json). diff --git a/research/p104-fold-elimination/RETAINED.json b/research/p104-fold-elimination/RETAINED.json new file mode 100644 index 0000000000..fe4c6cb6ae --- /dev/null +++ b/research/p104-fold-elimination/RETAINED.json @@ -0,0 +1,309 @@ +{ + "source_pr": 6170, + "source_author": "DreamingOfClouds", + "source_head": "445fb9124eb3fcb5d4f342c476b9ae3637f185aa", + "source_prefix": "research/p104-designer-toolkit-v2", + "archive_sha256": "dc34d853d26d153c34bfe5db64c8b770dea78275beecc058338e960fe5eef822", + "files": [ + { + "path": "README.md", + "git_blob": "0c1b92cd4abe071e650e836d8b93a7e573fa58c4", + "sha256": "4e8d4d7177ee23463f8d74202494152b14db864a19ffe33657c72b74bac67733", + "bytes": 20090 + }, + { + "path": "alignbuild/fold.py", + "git_blob": "90edf6bd98a16d4e15237be6dd48a1d4fd82d038", + "sha256": "9710214c15334186287e0f4ea1f39e1de042212348232ce0cd189719463d9a31", + "bytes": 8173 + }, + { + "path": "alignbuild/foldcensus.py", + "git_blob": "7531e565ee6b6684fe7b988e01b06414896ce4d7", + "sha256": "f0eda82cc2689643f8fab68960995c8bf6718951b13e40d82a296b874219695b", + "bytes": 4106 + }, + { + "path": "alignbuild/iob2.py", + "git_blob": "9b01d2cae873419595c36e651aa36ef07dceec1a", + "sha256": "a3e5598057697a3113cb4d786e13bd1f29ccf833d7115c7ef5bf1e67d37d75e5", + "bytes": 30364 + }, + { + "path": "alignbuild/life.py", + "git_blob": "72012e7f5b2fe6a707788f4df95ae6ff594523b3", + "sha256": "42654ef072b001f7488578973b9ac03672c2b515e3921d112c08d1b612ede96f", + "bytes": 4972 + }, + { + "path": "alignbuild/routing.py", + "git_blob": "81495742337e6692dbd22f02c461242f3b1e8d85", + "sha256": "dbd91a687f981de9b48e7168010ac7e51d7d5953bfd5f2615a379de77e20b5fa", + "bytes": 19896 + }, + { + "path": "alignbuild/rp.py", + "git_blob": "c9f9da0bf0f715c251c9bda2bb27e6fcaa02a4da", + "sha256": "ddb31097f1bb06e2143b78a56c05436500be76eca6a58a43dc1c175e273ecb04", + "bytes": 31341 + }, + { + "path": "alignbuild/sigside.py", + "git_blob": "ce76a5878882621561c04ebb4f3cb1bee59955ad", + "sha256": "b5e979fe2d3998a7e076d90da9f6cbf3a9f2f7568d09e0531808ca2e46167e8b", + "bytes": 16351 + }, + { + "path": "infra/legal.py", + "git_blob": "cca6f2a946b4bb6969659d7db8f65f115dae3dd0", + "sha256": "df7b743910bd534d710db50fc4460c5c976af0d1ba6007a1942a0c811e99a4d6", + "bytes": 13892 + }, + { + "path": "infra/price_exact.py", + "git_blob": "4e5a4e43920aee85d2ba1264dffd35b0935260e4", + "sha256": "cfa91630021afc62d1f0ab71c497fb7dd40f785241a498debc76d376fcb6935a", + "bytes": 6101 + }, + { + "path": "profiles/5551.json", + "git_blob": "ecca31a129167fca6b7ca7de24c6059fdc24e754", + "sha256": "12aa7a77381c275540b582bc798a39a896f5eb9d5cbaf44cc4d8f0ff77598fdd", + "bytes": 4905 + }, + { + "path": "profiles/5565.json", + "git_blob": "42b8f77cec34fc93f7962596db69f9055b58dadc", + "sha256": "ab68482e88106f72ce24c32a017f3f32451fd9dc2b5bb1ad16258b7b19e1c675", + "bytes": 4858 + }, + { + "path": "profiles/5580.json", + "git_blob": "b3751eaa63fadc03a48db7531a2045e8d6cb1adc", + "sha256": "22ea851fba99f06371ff8554a5372a9b07e42a325f1dd97c5f404900160f3bd9", + "bytes": 4877 + }, + { + "path": "profiles/5599.json", + "git_blob": "dbe4268a06cf7fd326ff3a3e87f23df66e356a24", + "sha256": "1b4f10714c3021351cbbad4c2206696a763076b34835a0b8c3e2355d60d99adb", + "bytes": 4950 + }, + { + "path": "profiles/5612.json", + "git_blob": "42fe0cbdaebe2d0de5432a2bc721bb47f34a88b4", + "sha256": "fefda04d1bbc3b633e63a7a33fded25d561449855784f007ac20d1aa45b5ce64", + "bytes": 5327 + }, + { + "path": "profiles/5613.json", + "git_blob": "4c6b4d7ec278bed0afa93f8b8eeb5b50363132f5", + "sha256": "a5fa16e2e031ba86586bc20241d87ec0a160a4d2c7a54feee18bdb1f712d2ca9", + "bytes": 5437 + }, + { + "path": "profiles/5644.json", + "git_blob": "176bdd865cd570f234aedb025c4e7cbce74eb614", + "sha256": "87ebae982d20df93744127816101e30c095e5bf126f1fd716138a3c802fbc923", + "bytes": 4985 + }, + { + "path": "profiles/5650.json", + "git_blob": "22d26f95648c8d3bfe846047af894d8bc310fb0b", + "sha256": "5483818e3a425c50883b8f3c1ddccf3248bb8da32e701f503feac9040765caaf", + "bytes": 4894 + }, + { + "path": "profiles/5660.json", + "git_blob": "9b4a06c8048a66e2443ff32eb0e2c8f13e447550", + "sha256": "15c2f40c9f3cde7f43ae82e057e834a2216f6f30a18d185c6d9409e6242d5b54", + "bytes": 4953 + }, + { + "path": "profiles/5678.json", + "git_blob": "5c941432a9890ca8f65542cb741e25179f7a57d0", + "sha256": "ca9c9ce675158684feae5bf36413fd2d084c7e5f426f5b74d8788a06da49c93d", + "bytes": 5025 + }, + { + "path": "profiles/5678_af814f6f.json", + "git_blob": "f2ca10f8f44567d2f105a34a90224606f10b5218", + "sha256": "ad6adf467f913bbde1384397fe56ef91ab16c07a52c8de4968f347245e558855", + "bytes": 5271 + }, + { + "path": "profiles/5713.json", + "git_blob": "f709daca7e4df003f0da3bbea0b5910ded328c07", + "sha256": "87a8ee3deff2bb55de0dbb142b47a45e241c801bfe38f3ca8f546abb091b2d36", + "bytes": 5077 + }, + { + "path": "profiles/5713_a5348f71.json", + "git_blob": "494f55da0f7b5336dae4104d958d0d5b8812a5e1", + "sha256": "1113c51e9abb230331fc7c506c87d28e275871b3a1bdf225d5480c714d8480f9", + "bytes": 5123 + }, + { + "path": "profiles/5718.json", + "git_blob": "ef5186172073d9c563480df6169acb9fac246221", + "sha256": "fc1b965f2253f350700360f3534a9a0f1e4f38339864d46825f4ae623ccd18fa", + "bytes": 5187 + }, + { + "path": "profiles/5718_a1534ac4.json", + "git_blob": "bf4d9a58b0ebfa0d92d02e952bfa5f477719077f", + "sha256": "d1ac62992aed776d6146de15b5d3b2c1db6955c1d0a8f186555a2a6f15997266", + "bytes": 5233 + }, + { + "path": "profiles/5739.json", + "git_blob": "ed1d8b39ecd4c32fe4f1047ad3720dd63e42b74f", + "sha256": "125782f8129a93cc56e14d298f6952b177999babb60132aa790cee7034ec8853", + "bytes": 5302 + }, + { + "path": "profiles/5739_b93d749a.json", + "git_blob": "dc6b854677cb982b6897982f25854e1e0c8ea9cb", + "sha256": "da7f2cf2fa0bbcdc41ae925c182a1df8314abc2ea0c0e1e549ed6cfa93e0a5ed", + "bytes": 5348 + }, + { + "path": "profiles/5751.json", + "git_blob": "d2d29f17613583c595cbc73324780620910f3592", + "sha256": "09e6c00220a9ef0d4b96e0d0b695a21c51352ef384202bb38383e250b48b9f19", + "bytes": 4972 + }, + { + "path": "profiles/5756.json", + "git_blob": "0caa12dde204e2faebf58571dc1bf5510bc9e799", + "sha256": "fa66d55a54f1a7eab96d83789e4ff2a12ae9f1e65426554b084dbd21a7802e5c", + "bytes": 4924 + }, + { + "path": "profiles/5774.json", + "git_blob": "c1d1ca518047ef5c2dde5294dd6d830fb30dab86", + "sha256": "26919f0d59cd72bcd09569acdc2069cfed585e6f7d7669ebaf1606f700ac397c", + "bytes": 5006 + }, + { + "path": "profiles/5786.json", + "git_blob": "c3f2a9ff4136f6c55b1a9ef489072e895851e2c5", + "sha256": "003db892be69196ba08d932a27d5ad0c1c591c5c81e52f766cf0c3a73744fd15", + "bytes": 5053 + }, + { + "path": "profiles/5796.json", + "git_blob": "38f11744464164bebe3b2ef5837a2ab0cf7f458b", + "sha256": "c435c2a37d46054fe8e47d876c12d93cf7b400ffbaed1c267f065ca195b9199d", + "bytes": 4976 + }, + { + "path": "profiles/5802.json", + "git_blob": "0260815740dd6cefed411053ba34d69116e7e9bb", + "sha256": "31e3cef05d43beed270ee94eb0e12137d70d801eb64b8d1e7c548e174b29b1b5", + "bytes": 5034 + }, + { + "path": "profiles/5802_9bab1ca9.json", + "git_blob": "84281c87c11981dabfba99bf6121d5a60c3e8c86", + "sha256": "d96249b1e783bb406ba90f865b6e82e4dddb824a7f62d4a8034ea867a235afce", + "bytes": 5080 + }, + { + "path": "profiles/5811.json", + "git_blob": "6c676af8275a4fb953676a916dde97071d01123f", + "sha256": "0ada18e84846fa8ce4f2903305baa3e202609640a685c2b9771bdeff198882a7", + "bytes": 5075 + }, + { + "path": "profiles/5811_883ab9ca.json", + "git_blob": "200db2840f3649e539715579fedba52402a41b11", + "sha256": "94c5bee590108978e66c895ec7dba088e9594a0e261cf22093c39a11ab51e3be", + "bytes": 5121 + }, + { + "path": "profiles/5812.json", + "git_blob": "988defaeeec8e132c2a25e93d6a8a4b888cb13b5", + "sha256": "e0b5bbecf0739a10fcabd3af3dbd1594ada7a95efbb1c57e8f2f3ea2e23877c6", + "bytes": 5064 + }, + { + "path": "profiles/5827.json", + "git_blob": "8da58bb2a8dd16979ff5f7d2aa38d940c36ca4a0", + "sha256": "0122df154c4bdbee6ca43987e41a5584a8194f8c6fc152479392a0aab49fad62", + "bytes": 4596 + }, + { + "path": "profiles/5827_05cd36e5.json", + "git_blob": "b3f6c165037223188eb5c7ea2d49b70774dba1c6", + "sha256": "2fbd7dd08d695eb16d7b3abacc4a757c11ee55e9d2fb46c286a3bdaa94edca95", + "bytes": 5080 + }, + { + "path": "profiles/5907.json", + "git_blob": "7c0ea4e73ac7aa6423b6b3990a4641cbb8073564", + "sha256": "971b7a6e733fd8ef06d57175dc1c720e9efb8362c9fd29c38bf77d1518fe5609", + "bytes": 5087 + }, + { + "path": "profiles/5907_c1cbd9e3.json", + "git_blob": "020b93addfd54c71be1994eedb5b4bb4f6b4dfe7", + "sha256": "b8ac3ca035ddf9ca5ce58213af7a075a017d5b837edb49f085d557078c433946", + "bytes": 5104 + }, + { + "path": "profiles/6030.json", + "git_blob": "aab3f4af31aba0dcfe525cc7a0ba73aaaf6425f6", + "sha256": "debcc649fa5bd9f553fb50ad99ce3b155772c6432440d65eeefc685e9adbb0ce", + "bytes": 5108 + }, + { + "path": "profiles/6030_772dd10a.json", + "git_blob": "f337f7971dd4119b8135f8b32bf45a5eda5f86b0", + "sha256": "e3070b2637bf8c13377ebcfade0a6e7c41dabb8e144c6a84a43a8b48b6506ccb", + "bytes": 5126 + }, + { + "path": "profiles/6143.json", + "git_blob": "a86e2e437a78f4d8d92956d0741e6adf762051dc", + "sha256": "9215ff0f581016d8667afc23931644e6241bd27ab1ec1c4a829f608b7d9521f0", + "bytes": 5090 + }, + { + "path": "profiles/6144.json", + "git_blob": "a9225c792d3089e0e8a5a111818bb452c526f552", + "sha256": "027e80d12d1af7db2730e26d84a9b1e6fed6255914a5c68565ef657c599344f7", + "bytes": 5094 + }, + { + "path": "profiles/6167.json", + "git_blob": "3abcffd767c2ebfab320bcc93be9e4c171cdbc8d", + "sha256": "88bcd134b6bfd134686460ebf1f79f11a60780f861aa2ee5aa6ee6dab8a35815", + "bytes": 5074 + }, + { + "path": "profiles/6167_564a076b.json", + "git_blob": "bbd79fc4a905b40f1e6c923f475063c9b4e13211", + "sha256": "fedacae1f3dc3be05d0f5265afa7a2d1f53c5fc2ae27e270f5101062a06d5fda", + "bytes": 5118 + }, + { + "path": "surgery/swlib.py", + "git_blob": "22bd2d2c811c3a06acdcaddf06e931b7066b0816", + "sha256": "d5b6f42a2065fe02c3256b48843b7e8af8ec04902147f3d501ab07020d0d5e90", + "bytes": 12813 + }, + { + "path": "tkcommon.py", + "git_blob": "e5151da7629e293b2c959933e3699146ef2b7840", + "sha256": "aba50b9328a550d62cc963a9df4f240c00d9000012f057f6247f970edf239259", + "bytes": 15832 + }, + { + "path": "words/6030.json.gz", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + "bytes": 119880 + } + ] +} diff --git a/research/p104-fold-elimination/SOURCES.json b/research/p104-fold-elimination/SOURCES.json new file mode 100644 index 0000000000..f53c427de7 --- /dev/null +++ b/research/p104-fold-elimination/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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" + } + ] +} diff --git a/research/p104-fold-elimination/TASK.json b/research/p104-fold-elimination/TASK.json new file mode 100644 index 0000000000..654a1fe452 --- /dev/null +++ b/research/p104-fold-elimination/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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": "Replace repeated Gauss-Jordan solves in the first PR6170 P104 shadow-relay fold with exact forward elimination and back substitution; preserve the canonical basic solution, every complete output word and source acceptance decision.", + "scope_change_reason": "The source open question suggests caching rule matrices. The measured bottleneck is modular elimination, so this contribution changes only the solver instead.", + "bottleneck_link": "Cheaper exact construction solves reduce time spent producing and testing candidate P104 words. This changes no supplier, native operator, invoice or selected bound.", + "budget_minutes": 60, + "stop_rule": "Freeze the first source-equivalent improvement; measure at least five alternating complete folds, package it, and leave further algorithm changes to Open next questions.", + "outcome": "completed", + "evidence": "PROFILE.json identifies elimination as the dominant cost. BENCHMARK.json is generated by five alternating complete baseline/candidate folds and binds every implementation hash. verify.py checks canonical solutions, invalid inputs, source corruption and both complete accepted solver variants. All ten final full-fold commands pass with identical words; medians 127.85968495812267 and 89.58335066703148 seconds, a reduction of 29.93620256739071 percent.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the same solver reduce time at every accepted fold site and across complete rebuilds?", + "why_it_matters": "The measured result is one actual first fold, not an end-to-end claim for every construction.", + "first_step": "Run the unchanged complete rebuild with the solver substitution and compare every emitted word and acceptance status.", + "blocked_by": "A separately budgeted benchmark of the remaining sites and larger system dimensions." + }, + { + "question": "Can exact elimination reuse factorizations across Newton rounds without changing candidate order?", + "why_it_matters": "The retained solver still rebuilds and eliminates a second system.", + "first_step": "Compare the two source-bound matrices, derive a certified update contract and include a complete invalidation test.", + "blocked_by": "No equality or low-rank relation between successive systems has been established." + } + ], + "upstream_checkpoint": { + "commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "priority_revision": 8, + "checked_at_utc": "2026-10-29T13:00:00Z" + }, + "source_question": { + "source": "PR #6170, Open next question 2", + "author": "DreamingOfClouds", + "head": "445fb9124eb3fcb5d4f342c476b9ae3637f185aa", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267663" + } +} diff --git a/research/p104-fold-elimination/VERIFY.json b/research/p104-fold-elimination/VERIFY.json new file mode 100644 index 0000000000..8df8ec409a --- /dev/null +++ b/research/p104-fold-elimination/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Canonical solver equivalence, source rejection and complete accepted fold variant in baseline and candidate modes." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same full checks with assertions disabled in the verifier interpreter." + } + ] +} diff --git a/research/p104-fold-elimination/benchmark.py b/research/p104-fold-elimination/benchmark.py new file mode 100644 index 0000000000..974f01ad02 --- /dev/null +++ b/research/p104-fold-elimination/benchmark.py @@ -0,0 +1,83 @@ +"""Time alternating complete first-step folds, checking every output word.""" + +import argparse +import gzip +import hashlib +import json +import platform +import statistics +import subprocess +import sys +import time +from pathlib import Path + +from runtime import PACKAGE, authenticate + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def canonical_word(path): + word = json.loads(gzip.decompress(path.read_bytes())) + data = json.dumps(word, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(data).hexdigest(), len(word["program"]) + + +def measure(mode, toolkit, scratch, index): + output = scratch / f"{index}-{mode}.json.gz" + command = [sys.executable, "-B", str(PACKAGE / "run.py"), mode, + str(toolkit), str(output), "--whole-fold"] + started = time.perf_counter() + result = subprocess.run(command, capture_output=True, text=True, timeout=570) + elapsed = time.perf_counter() - started + (scratch / f"{index}-{mode}.stdout").write_text(result.stdout) + (scratch / f"{index}-{mode}.stderr").write_text(result.stderr) + if result.returncode != 0: + raise RuntimeError(f"fold failed: {mode}, exit {result.returncode}") + report = json.loads(result.stdout.strip().splitlines()[-1]) + if len(report["steps"]) != 1 or report["steps"][0]["status"] != "FOLDED": + raise RuntimeError("complete fold did not accept its site") + fingerprint, events = canonical_word(output) + return {"mode": mode, "seconds": elapsed, "word_sha256": fingerprint, + "events": events, "step": report["steps"][0], "exit_code": 0} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("toolkit", type=Path) + parser.add_argument("scratch", type=Path) + parser.add_argument("--pairs", type=int, default=5) + args = parser.parse_args() + if not 5 <= args.pairs <= 10: + parser.error("use five to ten alternating pairs") + args.scratch.mkdir(parents=True, exist_ok=False) + manifest = authenticate(args.toolkit) + runs = [] + for index in range(args.pairs): + for mode in ("baseline", "candidate"): + run = measure(mode, args.toolkit, args.scratch, index) + if runs and any(run[key] != runs[0][key] + for key in ("word_sha256", "events", "step")): + raise RuntimeError("complete fold outputs differ") + runs.append(run) + print(mode, index, f"{run['seconds']:.6f}", flush=True) + summary = {} + for mode in ("baseline", "candidate"): + samples = [run["seconds"] for run in runs if run["mode"] == mode] + summary[mode] = {"median_seconds": statistics.median(samples), + "range_seconds": [min(samples), max(samples)]} + receipt = {"schema": "p104-fold-benchmark/1", "runs": runs, + "summary": summary, "errors": 0, "python": sys.version, + "executable": sys.executable, "platform": platform.platform(), + "source_head": manifest["source_head"], + "hashes": {path.name: digest(path) for path in + sorted(PACKAGE.glob("*.py"))}, + "retained_manifest_sha256": digest(PACKAGE / "RETAINED.json"), + "timed_region": "Fresh process through completed first fold, including source authentication, both attempted variants, legality and output serialization."} + (args.scratch / "BENCHMARK.json").write_text(json.dumps(receipt, indent=2) + "\n") + print(json.dumps(summary, sort_keys=True), flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/p104-fold-elimination/iob_entry.py b/research/p104-fold-elimination/iob_entry.py new file mode 100644 index 0000000000..d0920d83e4 --- /dev/null +++ b/research/p104-fold-elimination/iob_entry.py @@ -0,0 +1,18 @@ +"""Subprocess entry for the unmodified fold driver's solver invocation.""" + +import os +from pathlib import Path + +from runtime import install + + +def main(): + root = Path(os.environ["FOLD_TOOLKIT_ROOT"]).resolve() + install(root, os.environ["FOLD_SOLVER_MODE"]) + import iob2 + + iob2.main() + + +if __name__ == "__main__": + main() diff --git a/research/p104-fold-elimination/run.py b/research/p104-fold-elimination/run.py new file mode 100644 index 0000000000..1d35e8a5e9 --- /dev/null +++ b/research/p104-fold-elimination/run.py @@ -0,0 +1,46 @@ +"""Run the retained accepted solver variant, or the complete first fold step.""" + +import argparse +import os +import sys +from pathlib import Path + +from runtime import PACKAGE, install + +FLAGS = [ + "--flex", "--strip-sym", "--first-hop", "--root-frames-only", + "--f0", "--f0-wide", "--improve", "0", "--newton", "8", +] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("mode", choices=("baseline", "candidate")) + parser.add_argument("toolkit", type=Path) + parser.add_argument("output", type=Path) + parser.add_argument("--whole-fold", action="store_true") + args = parser.parse_args() + root = args.toolkit.resolve() + os.environ["TK_WORK"] = str(args.output.resolve().parent) + os.environ["TK_PROFILE"] = "6030_772dd10a" + os.environ["FOLD_TOOLKIT_ROOT"] = str(root) + os.environ["FOLD_SOLVER_MODE"] = args.mode + install(root, args.mode) + if args.whole_fold: + import fold + + fold.IOB = str(PACKAGE / "iob_entry.py") + sys.argv = ["fold.py", "6030", str(args.output), "--max", "1"] + fold.main() + else: + import iob2 + + iob2.main([ + "6030", str(args.output), "--root", "5", "--strip-regs", "705", + "--insert", "770:553:+0", "--insert", "770:1047:+0", + "--relocate", "770:13614:15597", *FLAGS, + ]) + + +if __name__ == "__main__": + main() diff --git a/research/p104-fold-elimination/runtime.py b/research/p104-fold-elimination/runtime.py new file mode 100644 index 0000000000..5087b374cc --- /dev/null +++ b/research/p104-fold-elimination/runtime.py @@ -0,0 +1,34 @@ +"""Load the exact retained toolkit without changing any predecessor source.""" + +import hashlib +import json +import sys +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent + + +def authenticate(root): + """Reject a missing or changed member of the retained source closure.""" + manifest = json.loads((PACKAGE / "RETAINED.json").read_text()) + for record in manifest["files"]: + path = root / record["path"] + data = path.read_bytes() + if hashlib.sha256(data).hexdigest() != record["sha256"]: + raise ValueError("changed retained source: " + record["path"]) + return manifest + + +def install(root, mode): + """Install the one explicit solver substitution, or retain the baseline.""" + if mode not in ("baseline", "candidate"): + raise ValueError("unknown solver mode") + authenticate(root) + sys.path.insert(0, str(root / "alignbuild")) + import rp + + if mode == "candidate": + from solver import solve + + rp.solve = solve + return rp diff --git a/research/p104-fold-elimination/solver.py b/research/p104-fold-elimination/solver.py new file mode 100644 index 0000000000..007cb3503b --- /dev/null +++ b/research/p104-fold-elimination/solver.py @@ -0,0 +1,71 @@ +"""Exact basic solutions over the toolkit's Mersenne field. + +The first independent columns are the pivots and all free variables are zero. +This is the same convention as the retained Gauss-Jordan solver. +""" + +import numpy as np + +P = 2147483647 +MAX_DIMENSION = 4096 + + +def eliminate(work, variables): + """Normalize pivots and eliminate below them; return their column indices.""" + rows = work.shape[0] + pivots = [] + for column in range(variables): + row = len(pivots) + if row == rows: + break + nonzero = np.flatnonzero(work[row:, column]) + if nonzero.size == 0: + continue + selected = row + int(nonzero[0]) + if selected != row: + work[[row, selected]] = work[[selected, row]] + inverse = pow(int(work[row, column]), P - 2, P) + work[row, column:] = work[row, column:] * inverse % P + if work[row, column] != 1: + raise ArithmeticError("pivot normalization failed") + below = row + 1 + np.flatnonzero(work[row + 1:, column]) + factors = work[below, column].copy() + work[below, column:] = ( + work[below, column:] + - factors[:, None] * work[row, column:][None, :] % P + ) % P + pivots.append(column) + return pivots + + +def solve(matrix, rhs): + """Return the canonical basic solution, or None for an inconsistent system. + + Integer matrices and vectors must have compatible shapes, with each matrix + dimension at most 4096. Inputs are copied and reduced modulo P. + """ + matrix = np.asarray(matrix) + rhs = np.asarray(rhs) + if matrix.ndim != 2 or rhs.ndim != 1: + raise ValueError("expected a matrix and a vector") + rows, variables = matrix.shape + if rhs.shape != (rows,) or max(rows, variables) > MAX_DIMENSION: + raise ValueError("incompatible or oversized system") + if matrix.dtype.kind not in "iu" or rhs.dtype.kind not in "iu": + raise ValueError("integer arrays required") + # Widen narrow types first; retain unsigned values until after reduction. + matrix_type = np.uint64 if matrix.dtype.kind == "u" else np.int64 + rhs_type = np.uint64 if rhs.dtype.kind == "u" else np.int64 + matrix = (matrix.astype(matrix_type, copy=False) % P).astype(np.int64, copy=False) + rhs = (rhs.astype(rhs_type, copy=False) % P).astype(np.int64, copy=False) + work = np.column_stack((matrix, rhs)) + pivots = eliminate(work, variables) + if np.any(work[len(pivots):, variables]): + return None + solution = np.zeros(variables, dtype=np.int64) + for row in range(len(pivots) - 1, -1, -1): + column = pivots[row] + terms = work[row, column + 1: variables] * solution[column + 1:] % P + # At most 4096 reduced summands; their sum fits signed int64. + solution[column] = (int(work[row, variables]) - int(terms.sum())) % P + return solution diff --git a/research/p104-fold-elimination/toolkit-closure.tar.gz b/research/p104-fold-elimination/toolkit-closure.tar.gz new file mode 100644 index 0000000000..cf2182cd3a Binary files /dev/null and b/research/p104-fold-elimination/toolkit-closure.tar.gz differ diff --git a/research/p104-fold-elimination/verify.py b/research/p104-fold-elimination/verify.py new file mode 100644 index 0000000000..88b2ebae82 --- /dev/null +++ b/research/p104-fold-elimination/verify.py @@ -0,0 +1,165 @@ +"""Check canonical solutions and complete accepted fold-variant equivalence.""" + +import gzip +import hashlib +import itertools +import json +import subprocess +import sys +import tarfile +import tempfile +import time +from pathlib import Path + +import numpy as np + +from runtime import PACKAGE, authenticate, install +from solver import P, solve + +EXPECTED_WORD = "6a3d8a88b41cec6d2e6d5a1315b16448478a32c60157c0f036d89b65e702f13b" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def extract(root): + manifest = json.loads((PACKAGE / "RETAINED.json").read_text()) + archive = PACKAGE / "toolkit-closure.tar.gz" + require(hashlib.sha256(archive.read_bytes()).hexdigest() + == manifest["archive_sha256"], "changed source archive") + with tarfile.open(archive) as source: + members = source.getmembers() + require(len(members) == len(manifest["files"]), "archive member count") + expected = {record["path"] for record in manifest["files"]} + require({member.name for member in members} == expected, "archive names") + for member in members: + require(member.isfile() and not member.name.startswith("/") + and ".." not in member.name.split("/"), "unsafe member") + source.extractall(root, filter="data") + return authenticate(root) + + +def check_system(original, matrix, rhs): + before_matrix, before_rhs = matrix.copy(), rhs.copy() + expected = original(matrix, rhs) + actual = solve(matrix, rhs) + require((actual is None) == (expected is None), "consistency disagreement") + if actual is not None: + require(np.array_equal(actual, expected), "canonical solution disagreement") + residual = ((matrix % P) * actual[None, :]) % P + require(np.array_equal(residual.sum(axis=1) % P, rhs % P), "bad solution") + require(np.array_equal(before_matrix, matrix) and np.array_equal(before_rhs, rhs), + "input mutation") + + +def integer_formats(original): + for dtype in (np.int8, np.int64, np.uint64): + for bound in (np.iinfo(dtype).min, np.iinfo(dtype).max): + matrix = np.array([[bound, 1], [1, 0]], dtype=dtype) + rhs = np.array([1, 2], dtype=dtype) + normalized = np.array([[int(value) % P for value in row] + for row in matrix], dtype=np.int64) + require(np.array_equal(solve(matrix, rhs), + original(normalized, rhs.astype(np.int64))), + "integer format boundary disagreement") + return 6 + + +def controls(root): + original = install(root, "baseline").solve + count = integer_formats(original) + for bits in itertools.product(range(2), repeat=8): + matrix = np.array(bits[:6], dtype=np.int64).reshape(2, 3) + check_system(original, matrix, np.array(bits[6:], dtype=np.int64)) + count += 1 + random = np.random.default_rng(20261029) + for rows in range(9): + for columns in range(9): + for trial in range(12): + matrix = random.integers(0, P, (rows, columns), dtype=np.int64) + if trial % 3 == 0: + matrix %= 3 + if trial % 4 == 0 and columns > 1: + matrix[:, columns - 1] = matrix[:, 0] + rhs = random.integers(0, P, rows, dtype=np.int64) + if trial % 2 == 0: + weights = random.integers(0, 100, columns) + rhs = (matrix * weights).sum(axis=1) % P + check_system(original, matrix, rhs) + count += 1 + invalid = [(np.zeros(2, dtype=np.int64), np.zeros(2, dtype=np.int64)), + (np.zeros((2, 2), dtype=np.int64), np.zeros(1, dtype=np.int64)), + (np.zeros((4097, 0), dtype=np.int64), np.zeros(4097, dtype=np.int64)), + (np.zeros((1, 1), dtype=float), np.zeros(1, dtype=np.int64))] + for matrix, rhs in invalid: + try: + solve(matrix, rhs) + except ValueError: + continue + raise ValueError("invalid solver input accepted") + changed = root / "alignbuild/rp.py" + saved = changed.read_bytes() + changed.write_bytes(saved + b"\n# mutation\n") + try: + try: + authenticate(root) + except ValueError: + return count, len(invalid) + 1 + raise ValueError("changed source accepted") + finally: + changed.write_bytes(saved) + + +def integration(root, scratch): + reports = [] + for mode in ("baseline", "candidate"): + output = scratch / f"{mode}.json.gz" + optimize = ["-O"] if sys.flags.optimize else [] + command = [sys.executable, *optimize, "-B", str(PACKAGE / "run.py"), mode, + str(root), str(output)] + started = time.perf_counter() + result = subprocess.run(command, capture_output=True, text=True, timeout=240) + elapsed = time.perf_counter() - started + (scratch / f"{mode}.log").write_text(result.stdout + result.stderr) + require(result.returncode == 0, "solver command failed") + require("RESULT: LEGAL " in result.stdout, "variant did not pass source checks") + word = json.loads(gzip.decompress(output.read_bytes())) + canonical = json.dumps(word, sort_keys=True, separators=(",", ":")).encode() + require(hashlib.sha256(canonical).hexdigest() == EXPECTED_WORD, + "complete output word changed") + reports.append({"mode": mode, "seconds": elapsed, + "events": len(word["program"]), "word_sha256": EXPECTED_WORD}) + return reports + + +def check_benchmark(): + receipt = json.loads((PACKAGE / "BENCHMARK.json").read_text()) + require(receipt["errors"] == 0 and len(receipt["runs"]) >= 10, "benchmark coverage") + for name, expected in receipt["hashes"].items(): + require(hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() == expected, + "benchmark implementation changed: " + name) + for index, run in enumerate(receipt["runs"]): + require(run["mode"] == ("baseline", "candidate")[index % 2], "run order") + require(run["word_sha256"] == EXPECTED_WORD and run["exit_code"] == 0 + and run["events"] == 22821, "benchmark output disagreement") + + +def main(): + check_benchmark() + with tempfile.TemporaryDirectory(prefix="p104-fold-") as directory: + scratch = Path(directory) + root = scratch / "toolkit" + root.mkdir() + manifest = extract(root) + cases, rejections = controls(root) + runs = integration(root, scratch) + print(json.dumps({"status": "PASS_P104_FOLD_ELIMINATION", + "canonical_systems": cases, "rejection_controls": rejections, + "retained_files": len(manifest["files"]), "runs": runs}, + sort_keys=True)) + + +if __name__ == "__main__": + main()