diff --git a/research/packed-dyadic-transpose/BENCHMARK.json b/research/packed-dyadic-transpose/BENCHMARK.json new file mode 100644 index 0000000000..de316a93ef --- /dev/null +++ b/research/packed-dyadic-transpose/BENCHMARK.json @@ -0,0 +1,356 @@ +{ + "code_sha256": { + "PROOF.md": "6542e8f305ab7f65b429a6de819df3ccf822a393d94314986f53b4aac48ef0ff", + "benchmark.py": "6590c8c851cbd9f1bb2b5f04aff81a46ae1cbbe80d106bc13238a523dc541dec", + "packed.py": "d725ca8b349959d6961911b85dd5e35e6cb9823d94c97c49ec5c391449a75cf5", + "verify.py": "669802f0521c7ed8d1781c6302502e576ebbb6c0cbdc99b6240e12b7c3618c20" + }, + "cpu_count": 18, + "errors": 0, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "load_after": [ + 5.84326171875, + 4.2919921875, + 3.3154296875 + ], + "load_before": [ + 5.56884765625, + 4.212890625, + 3.2822265625 + ], + "order": "dense,packed repeated five times", + "pairs": 5, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "profile": { + "dense": { + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "top": [ + { + "calls": 1, + "function": "reverse_columns", + "inclusive_seconds": 0.84525275, + "self_seconds": 0.42496577700000004 + }, + { + "calls": 20650, + "function": "", + "inclusive_seconds": 0.344353854, + "self_seconds": 0.18178822900000002 + }, + { + "calls": 5492230, + "function": "", + "inclusive_seconds": 0.16418927400000002, + "self_seconds": 0.16418927400000002 + }, + { + "calls": 22012, + "function": "__new__", + "inclusive_seconds": 0.055230937, + "self_seconds": 0.027610093000000002 + }, + { + "calls": 593547, + "function": "numerator", + "inclusive_seconds": 0.014518976000000001, + "self_seconds": 0.014518976000000001 + }, + { + "calls": 86084, + "function": "", + "inclusive_seconds": 0.007125123000000001, + "self_seconds": 0.007125123000000001 + }, + { + "calls": 22012, + "function": "", + "inclusive_seconds": 0.006653436, + "self_seconds": 0.006653436 + }, + { + "calls": 66036, + "function": "", + "inclusive_seconds": 0.010518061, + "self_seconds": 0.006153055 + } + ] + }, + "packed": { + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "top": [ + { + "calls": 44056, + "function": "step", + "inclusive_seconds": 0.11199083400000001, + "self_seconds": 0.106570706 + }, + { + "calls": 1, + "function": "source_events", + "inclusive_seconds": 0.105190875, + "self_seconds": 0.038724854 + }, + { + "calls": 24568, + "function": "__new__", + "inclusive_seconds": 0.051632917, + "self_seconds": 0.025851281 + }, + { + "calls": 1, + "function": "validate", + "inclusive_seconds": 0.021268917000000002, + "self_seconds": 0.016149868 + }, + { + "calls": 342148, + "function": "require", + "inclusive_seconds": 0.009716851, + "self_seconds": 0.009716851 + }, + { + "calls": 1, + "function": "plan", + "inclusive_seconds": 0.045311500000000005, + "self_seconds": 0.0071546100000000005 + }, + { + "calls": 86084, + "function": "", + "inclusive_seconds": 0.006753558000000001, + "self_seconds": 0.006753558000000001 + }, + { + "calls": 92270, + "function": "", + "inclusive_seconds": 0.010953938, + "self_seconds": 0.006717996 + } + ] + } + }, + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "samples": [ + { + "checkpoint_seconds": 0.4840470829512924, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 41369600, + "process_wall_seconds": 0.5316805420443416, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "dense" + }, + { + "checkpoint_seconds": 0.13006100000347942, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 46350336, + "process_wall_seconds": 0.17765537498053163, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "packed" + }, + { + "checkpoint_seconds": 0.4846877920208499, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 41009152, + "process_wall_seconds": 0.5281897919485345, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "dense" + }, + { + "checkpoint_seconds": 0.12933166697621346, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 46563328, + "process_wall_seconds": 0.1717405419331044, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "packed" + }, + { + "checkpoint_seconds": 0.48029700003098696, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 41402368, + "process_wall_seconds": 0.52419662498869, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "dense" + }, + { + "checkpoint_seconds": 0.13182870810851455, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 46448640, + "process_wall_seconds": 0.17697791696991771, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "packed" + }, + { + "checkpoint_seconds": 0.48608795809559524, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 41222144, + "process_wall_seconds": 0.5310359169961885, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "dense" + }, + { + "checkpoint_seconds": 0.13196008396334946, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 46465024, + "process_wall_seconds": 0.17785158299375325, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "packed" + }, + { + "checkpoint_seconds": 0.4790517500368878, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 41025536, + "process_wall_seconds": 0.5266580830793828, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "dense" + }, + { + "checkpoint_seconds": 0.12288341706153005, + "errors": 0, + "events": 25475, + "inputs": { + "research/p104-helper-subspace-splits/WORD.json.gz": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099", + "research/p104-helper-subspace-splits/local.py": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + "peak_rss_bytes": 46579712, + "process_wall_seconds": 0.1656619580462575, + "result": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "side": "packed" + } + ], + "scope": "complete transpose checkpoint, not the complete supplier replay", + "status": "PASS_PACKED_TRANSPOSE_BENCHMARK", + "summary": { + "checkpoint_seconds_speedup": 3.721692766765926, + "dense": { + "checkpoint_seconds": { + "max": 0.48608795809559524, + "median": 0.4840470829512924, + "min": 0.4790517500368878 + }, + "peak_rss_bytes": { + "max": 41402368, + "median": 41222144, + "min": 41009152 + }, + "process_wall_seconds": { + "max": 0.5316805420443416, + "median": 0.5281897919485345, + "min": 0.52419662498869 + } + }, + "packed": { + "checkpoint_seconds": { + "max": 0.13196008396334946, + "median": 0.13006100000347942, + "min": 0.12288341706153005 + }, + "peak_rss_bytes": { + "max": 46579712, + "median": 46465024, + "min": 46350336 + }, + "process_wall_seconds": { + "max": 0.17785158299375325, + "median": 0.17697791696991771, + "min": 0.1656619580462575 + } + }, + "process_wall_seconds_speedup": 2.9844954726092463 + } +} diff --git a/research/packed-dyadic-transpose/PROOF.md b/research/packed-dyadic-transpose/PROOF.md new file mode 100644 index 0000000000..7b2c65f79a --- /dev/null +++ b/research/packed-dyadic-transpose/PROOF.md @@ -0,0 +1,98 @@ +# Packed exact dyadic transpose endpoints + +This contribution was produced by Nick Petalas. Apache-2.0. + +The claim is an exact alternative implementation of a linear endpoint +checkpoint. It is not a new proof of the selected construction. Classical +Kronecker substitution supplies the integer evaluation method. The bounded +dyadic planning pass and its application to the retained checkpoint are the +new implementation. + +## Contract + +There are n roles. Initially the coefficient matrix is I_n. In chronological +order, ADD replaces row r by row r + q row s; COPY overwrites row r by +q row s; SCALE multiplies row r by q; INIT and CLEAR replace row r by zero. +Here q is dyadic. The requested endpoint is the transpose of this matrix, +with every one of its n squared entries specified. This treats INIT and CLEAR +as their linear maps only. Allocation, erasure legality, frames, native +operators and all non-linear semantics require the surrounding checks. + +Transposition reverses chronology. A transposed ADD adds q times row r to +row s. A transposed COPY does that addition and then zeros row r. Transposed +SCALE, INIT and CLEAR have their original row action. The dense source +checkpoint implements precisely these operations. MOVE is the identity +in this scalar projection and remains checked by the surrounding source +verifier. This backend does not replace that verifier. + +## Numerators and bounds + +Represent a row as c/2^e, with integral coefficient vector c and e >= 0. +For q = p/2^d an ADD to s uses level L = max(e_s,e_r+d) and numerator + + 2^(L-e_s) c_s + p 2^(L-e_r-d) c_r. + +SCALE replaces c_r by p c_r and e_r by e_r+d. Resetting a row sets c=0,e=0. +There is no cancellation-based denominator normalization. + +A first pass replaces each numerator row by an upper bound on its l1 norm. +It starts at one and performs exactly these updates with |p| and addition +of the nonnegative bounds. The triangle inequality proves its bound at +every event. It includes rows later discarded by COPY, INIT or CLEAR, so +the bound also controls all intermediate integer lengths. Parsing enforces +role, event, coefficient, exponent, growth and packed-storage limits before +the packed pass begins. + +At each endpoint row, align its numerator and its requested dyadic row to +one exponent. The sum of their l1 bounds bounds the l1 norm of their +difference. Let M be the maximum of these difference bounds and all +intermediate bounds, at least one. The implementation chooses + + b = bit_length(M) + 1, B = 2^b. + +Thus B > 2M. It also checks the fixed resource limit n squared times b. + +## Injectivity + +Encode an integer row c by E(c) = sum_j c_j B^j, allowing negative digits. +Encoding commutes exactly with every integer sum, shift and multiplication +above. Intermediate radix carries do not alter this identity. No digitwise +division, parity test on the packed integer, modular reduction, truncation +or machine-width arithmetic is used. + +If a nonzero endpoint difference d satisfies E(d)=0, take its least index k +with d_k nonzero. Dividing by B^k and reducing modulo B gives d_k=0 mod B. +But |d_k| <= ||d||_1 <= M < B, a contradiction. Hence encoded equality is +equivalent to equality of every endpoint coefficient. The larger choice +B>2M is conservative. A single evaluation here is deterministic exact +arithmetic, not a probabilistic polynomial fingerprint. + +The independent finite oracle instead executes chronological Fraction +matrices and explicitly transposes them. It checks all coefficients of +every stated small word, including overwrites, negative coefficients, +different denominators and zero rows. Incorrect endpoints and an explicit +unsafe-radix collision are rejection controls. The complete retained word +is a workload and source-syntax compatibility test, without repeating its +native, caller, compiler or exponent claims. + +## Scope and resources + +This implementation is bounded to 1024 roles, 60000 scalar events, +numerators below 2^20, denominator exponents at most 32 per coefficient, +4096 bits of planned growth and 128000000 packed coefficient bits. It +rejects instances beyond those bounds. At most n packed rows and a bounded +number of temporary packed arithmetic integers are live in the second pass. The +128000000-bit bound is 16 MB of coefficient payload, not a byte-exact heap +or RSS claim. Parsed events, Python objects and interpreter allocations are +additional bounded storage. No fixed-allocation native runtime is claimed. + +Power of Ten rule 3 has a managed-runtime deviation in packed.py, verify.py +and benchmark.py. CPython allocates arbitrary-precision integers and +containers during execution. Fixed input and growth limits, bounded fixture +counts and sequential benchmark processes control their size and lifetime. +Library allocation internals are not inspected. A fixed-pool implementation +would be required for a fixed-allocation runtime claim. Rules 8 and 9 use +ordinary Python functions and bounded standard-library dispatch. Benchmark +dispatch has exactly two targets. Warning-strict ordinary and optimized +execution and available static diagnostics check the new files. All new +functions fit within 60 physical lines. diff --git a/research/packed-dyadic-transpose/README.md b/research/packed-dyadic-transpose/README.md new file mode 100644 index 0000000000..172b9bb8ee --- /dev/null +++ b/research/packed-dyadic-transpose/README.md @@ -0,0 +1,144 @@ +# Exact packed dyadic transpose replay + +The complete transpose-checkpoint command is **2.98 times faster** on the +retained selected P104 word, from median 0.5282 to 0.1770 seconds over five +alternating fresh-process pairs. Its exact checkpoint covers all 571,536 +coefficients. This is an opt-in verifier-engineering result with a scoped +correctness proof, not a new kappa or an audit of the selected construction. + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Method and evidence + +[packed.py](packed.py) represents each dyadic row by one integer numerator +and a binary denominator exponent. A separate l1-bound pass chooses an +injective signed radix before the packed replay starts. Arithmetic then +updates whole rows using Python integers. [PROOF.md](PROOF.md) proves that +the final integer equalities are equivalent to every matrix coefficient +equality. This is deterministic exact arithmetic, without random probes, +modular fingerprints, machine-integer overflow or cached acceptance results. + +The new backend preserves the complete scalar projection of ADD, COPY, +SCALE, INIT and CLEAR. The surrounding source checker remains responsible +for frames, ownership, erasure legality and native semantics. Every source +file stays unchanged, and the official selected reproduction command stays +unchanged. No backend is automatically installed into an existing verifier. + +The direct check prints `PASS_PACKED_DYADIC_TRANSPOSE` in a generated +source-hash-bound JSON receipt. It checks: + +- All 4,681 words of length zero through four over the stated eight-event + alphabet, plus 160 deterministic forty-event words on one through eight + roles. The independent chronological Fraction oracle compares all 22,804 + literal coefficients, including overwrite and denominator interactions. +- All 4,841 corresponding incorrect endpoints are rejected. Fourteen + additional controls cover invalid domains, growth and memory limits, + unsafe-radix collisions and an altered full-word endpoint. +- The retained 25,475-event word, with 22,028 non-MOVE events, has 756 + columns and 571,536 endpoint coefficients. Its planned radix width is + 111 bits. Its complete endpoint-check summary equals the unchanged dense + checkpoint's summary. +- Both pinned inputs and the generated benchmark's code/input bindings + match. Recorded timings are checked for internal consistency; routine + correctness replay does not repeat the timing experiment. + +The complete retained word is a workload, not a new supplier-verification +deliverable. Its predecessor endpoint, helper, native, caller, compiler and +exponent claims are credited to their existing authors. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-dyadic-transpose/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/packed-dyadic-transpose/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/packed-dyadic-transpose +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/packed-dyadic-transpose --check-source-history +``` + +Substitute an equivalent CPython 3.12 path elsewhere. Sparse checkouts need +`research/packed-dyadic-transpose` and the two live inputs listed in +[VERIFY.json](VERIFY.json). Historical guidance and card pins in +[SOURCES.json](SOURCES.json) are provenance, not executable dependencies. + +Run the optional complete timing experiment separately: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/packed-dyadic-transpose/benchmark.py +``` + +Its generated report is [BENCHMARK.json](BENCHMARK.json). Each subprocess +authenticates and parses the same source bytes, loads both implementations, +and executes one complete checkpoint. The inner timer includes the packed +syntax conversion, growth planning, replay and endpoint comparison. The +outer timer additionally includes process startup, imports, authentication, +decompression, parsing and result serialization. Each completed result is +consumed and compared, and all ten samples have zero errors. + +## Measurement scope + +The host is macOS arm64, CPython 3.12.15, with 18 logical CPUs. Other work +was running; the five dense/packed pairs execute sequentially and alternate +to share that noise. No sample is discarded. The published ranges are: + +| Timed region | Dense median and range, seconds | Packed median and range, seconds | +| --- | --- | --- | +| Complete checkpoint command | 0.5282, 0.5242 to 0.5317 | 0.1770, 0.1657 to 0.1779 | +| Checkpoint function | 0.4840, 0.4791 to 0.4861 | 0.1301, 0.1229 to 0.1320 | + +The checkpoint function is 3.72 times faster and accounts for about 92% of +the baseline checkpoint command. Median process peak RSS rises from +41,222,144 to 46,465,024 bytes. Separate untimed profiles identify the +baseline's columnwise parity scans and row arithmetic as its main cost. +The packed path spends its largest self time in bounded integer row steps; +syntax/Fraction conversion and the bound pass also remain payable. + +These measurements concern one scalar endpoint checkpoint. They are not a +whole selected-replay speedup or a physical multiplication speedup. Ali +Romman's [PR5757](https://github.com/CrocSwap/integer-mult-bounds/pull/5757) +accelerates the complete selected replay's native quadratic states and +retains this original transpose checkpoint. Its different full-replay +timings are cited context and were not rerun here. No Linux timing claim +is made. + +## Limits and credit + +The implementation rejects more than 1,024 roles, 60,000 scalar events, +4,096 bits of planned numerator growth, or 128,000,000 packed coefficient +bits. These are explicit resource bounds, not a universal algorithmic +limitation. The managed-runtime allocation deviation is in PROOF.md. + +Credit Ali Romman for the PR5599 helper-subspace word, dense reverse-column +checkpoint and PR5544/5545 implementation lineage; Pierre-Loic Doulcet for +the retained PR5565 source changes; David Arias for the scalar word; Cinna +Davis for private reuse; Gareth Davidson for composition; and all retained +P104/native/controller/compiler contributors. Classical Kronecker +substitution and elementary transpose algebra are not claimed as new +mathematics. Sagar Thakrar's +[PR1781](https://github.com/CrocSwap/integer-mult-bounds/pull/1781) already +uses packed exact integer matrices and the signed-radix argument for +Clifford recipes, following the retained Lean comparator. That method is +credited predecessor work. This package applies a new trace-dependent +dyadic bound planner to the scalar transpose checkpoint, including COPY +and zero-row operations. The new work is the bounded backend, correctness argument, +independent behavior checks and checkpoint measurements. + +Independent human and formal proof-kernel review are unclaimed. No native +phase, physical caller, full supplier replay, rounded multiplier, stock, +compiler, tape or analytic obligation is discharged. Lean and Docker were +not run. The selected frontier is unchanged. + +## Open next questions + +Can this backend be installed at one complete successor replay's literal +transpose call site while retaining all surrounding controls? First bind +that call and compare the complete scientific output. This package supplies +no such integration or whole-replay measurement. That is the next question; +the first useful checkpoint improvement is shipped here without further +tuning. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228421) +records the original scope. The source base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priorities revision 8. The +autonomous-run playbook used an explicit first-improvement stop rule. diff --git a/research/packed-dyadic-transpose/SOURCES.json b/research/packed-dyadic-transpose/SOURCES.json new file mode 100644 index 0000000000..ca2c26fd70 --- /dev/null +++ b/research/packed-dyadic-transpose/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-helper-subspace-splits/local.py", + "usage": "input", + "git_blob": "e6e28bacdad7cb51400d827b9a6e02f2b605d357", + "sha256": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad" + }, + { + "path": "research/frontier1094-recipes-exact-seed76/README.md", + "usage": "provenance", + "git_blob": "4a4747e0c302e58cc8f4c5516d57dc8b81ce95d0", + "sha256": "a0635fd335cf2949a00f6a1eee8826188efbccd3051d4cc26dd8cee2fe725ce8" + } + ] +} diff --git a/research/packed-dyadic-transpose/TASK.json b/research/packed-dyadic-transpose/TASK.json new file mode 100644 index 0000000000..ccf189a1eb --- /dev/null +++ b/research/packed-dyadic-transpose/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Opt-in exact packed-integer backend for the complete dyadic transpose endpoint checkpoint, with a bound-planning pass and five alternating fresh-process benchmark pairs on the selected PR5599 word.", + "scope_change_reason": "Restrict the replay-runtime card to the complete transpose endpoint checkpoint. This excludes native-state and whole-supplier acceleration and preserves a bounded same-fixture comparison.", + "bottleneck_link": "Speeds a complete scalar endpoint checkpoint without removing any coefficient; native, caller, invoice and compiler checks stay external.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified backend speedup; no further tuning, new supplier audit or construction search.", + "outcome": "completed", + "evidence": "PROOF.md; 4841 chronological dense-oracle words and wrong-endpoint controls; all 571536 selected checkpoint coefficients; source-bound five-pair BENCHMARK.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this opt-in endpoint backend be wired into a complete successor replay without changing its surrounding checks?", + "why_it_matters": "Only complete integration can establish a whole-replay gain.", + "first_step": "Bind one literal source call site, retain its original controls and compare the complete scientific output.", + "blocked_by": "This package benchmarks the transpose checkpoint only; no full supplier replay is performed." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228421", + "playbook": "Autonomous local run", + "overlap": { + "entry_coverage": "Cached search fetched 393 open PRs and 5635 Discussion records with complete pagination; local notes searched 62 of 8136 and were incomplete. Separate main README and distinctive merged searches were read.", + "related_predecessor": "PR5757 accelerates native quadratic states and preserves the original reverse-column checkpoint. It does not supply this packed backend.", + "source": "original", + "limitations": "No arbitrary diff or unpublished-work coverage; no novelty certificate.", + "packed_predecessor": "Sagar Thakrar PR1781 already uses exact packed integer matrices and signed-radix injectivity for Clifford recipes. This contribution claims only a new dyadic trace-bound planner/backend and measured scalar-transpose application, not that method." + } +} diff --git a/research/packed-dyadic-transpose/VERIFY.json b/research/packed-dyadic-transpose/VERIFY.json new file mode 100644 index 0000000000..9adfe9a875 --- /dev/null +++ b/research/packed-dyadic-transpose/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-helper-subspace-splits/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent chronological Fraction oracle, complete selected transpose endpoint, incorrect endpoints, bounds, source and generated benchmark bindings." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical mathematical and source-bound checks with assertions disabled." + } + ] +} diff --git a/research/packed-dyadic-transpose/benchmark.py b/research/packed-dyadic-transpose/benchmark.py new file mode 100644 index 0000000000..70f04923c0 --- /dev/null +++ b/research/packed-dyadic-transpose/benchmark.py @@ -0,0 +1,178 @@ +"""Five alternating fresh-process checkpoint pairs; writes JSON to stdout. + +This contribution was produced by Nick Petalas. Apache-2.0. +""" + +import argparse +import cProfile +import hashlib +import json +import os +import platform +import resource +import runpy +import statistics +import subprocess +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def context(): + checks = runpy.run_path(str(HERE / "verify.py")) + pins = checks["authenticate"]() + word = checks["workload"]() + original = runpy.run_path( + str(checks["ROOT"] / "research/p104-helper-subspace-splits/local.py") + ) + return ( + checks, + pins, + word, + { + "dense": original["reverse_columns"], + "packed": checks["P"]["reverse_columns"], + }, + ) + + +def child(side): + _, pins, word, functions = context() + start = time.perf_counter() + result = functions[side](word) + elapsed = time.perf_counter() - start + peak = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss + if platform.system() != "Darwin": + peak *= 1024 + print( + json.dumps( + { + "side": side, + "checkpoint_seconds": elapsed, + "peak_rss_bytes": peak, + "result": result, + "events": len(word["program"]), + "inputs": pins, + "errors": 0, + }, + sort_keys=True, + ) + ) + + +def profiles(functions, word): + reports = {} + for side in ("dense", "packed"): + profiler = cProfile.Profile() + result = profiler.runcall(functions[side], word) + rows = [] + for entry in profiler.getstats(): + name = entry.code if isinstance(entry.code, str) else entry.code.co_name + rows.append( + { + "function": name, + "calls": entry.callcount, + "self_seconds": entry.inlinetime, + "inclusive_seconds": entry.totaltime, + } + ) + reports[side] = { + "result": result, + "top": sorted(rows, key=lambda x: x["self_seconds"], reverse=True)[:8], + } + return reports + + +def sample(side): + start = time.perf_counter() + completed = subprocess.run( + [ + sys.executable, + "-I", + "-W", + "error", + "-B", + str(HERE / "benchmark.py"), + "--side", + side, + ], + capture_output=True, + text=True, + timeout=120, + check=True, + ) + wall = time.perf_counter() - start + if completed.stderr: + raise ValueError("child diagnostics: " + completed.stderr) + result = json.loads(completed.stdout) + result["process_wall_seconds"] = wall + return result + + +def summarize(samples): + summary = {} + for side in ("dense", "packed"): + rows = [r for r in samples if r["side"] == side] + summary[side] = {} + for key in ("checkpoint_seconds", "process_wall_seconds", "peak_rss_bytes"): + values = [r[key] for r in rows] + summary[side][key] = { + "median": statistics.median(values), + "min": min(values), + "max": max(values), + } + for key in ("checkpoint_seconds", "process_wall_seconds"): + summary[key + "_speedup"] = ( + summary["dense"][key]["median"] / summary["packed"][key]["median"] + ) + return summary + + +def run(): + checks, pins, word, functions = context() + before = list(os.getloadavg()) + profiled = profiles(functions, word) + samples = [] + for _ in range(5): + for side in ("dense", "packed"): + samples.append(sample(side)) + expected = samples[0]["result"] + for row in samples: + checks["require"]( + row["errors"] == 0 and row["result"] == expected, + "every sample completed the same checkpoint", + ) + checks["require"](row["inputs"] == pins, "same exact inputs") + receipt = { + "status": "PASS_PACKED_TRANSPOSE_BENCHMARK", + "errors": 0, + "pairs": 5, + "order": "dense,packed repeated five times", + "python": sys.version, + "platform": platform.platform(), + "cpu_count": os.cpu_count(), + "load_before": before, + "load_after": list(os.getloadavg()), + "inputs": pins, + "samples": samples, + "summary": summarize(samples), + "profile": profiled, + "scope": "complete transpose checkpoint, not the complete supplier replay", + "code_sha256": { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in ("packed.py", "verify.py", "benchmark.py", "PROOF.md") + }, + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--side", choices=("dense", "packed")) + arguments = parser.parse_args() + if arguments.side: + child(arguments.side) + else: + run() diff --git a/research/packed-dyadic-transpose/packed.py b/research/packed-dyadic-transpose/packed.py new file mode 100644 index 0000000000..55a6725a11 --- /dev/null +++ b/research/packed-dyadic-transpose/packed.py @@ -0,0 +1,172 @@ +"""Bounded exact transpose endpoints using classical integer substitution. + +This contribution was produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction + +MAX_ROLES = 1024 +MAX_EVENTS = 60000 +MAX_BITS = 4096 +MAX_PACKED_BITS = 128000000 +KINDS = frozenset(("ADD", "COPY", "SCALE", "INIT", "CLEAR")) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(n, events, expected): + require(type(n) is int and 1 <= n <= MAX_ROLES, "role limit") + require( + isinstance(events, (tuple, list)) and len(events) <= MAX_EVENTS, "event limit" + ) + require(len(expected) == n, "expected row count") + for kind, r, s, numerator, shift in events: + require(kind in KINDS, "opcode") + require(type(r) is int and 0 <= r < n, "destination") + require(type(s) is int and 0 <= s < n, "source") + require( + type(numerator) is int and 0 < abs(numerator) < 2**20, "numerator limit" + ) + require(type(shift) is int and 0 <= shift <= 32, "denominator limit") + require(kind not in ("ADD", "COPY") or s != r, "distinct roles") + for row in expected: + require(isinstance(row, dict) and len(row) <= n, "expected row") + for column, value in row.items(): + require(type(column) is int and 0 <= column < n, "expected column") + require(type(value) in (int, Fraction), "expected coefficient") + q = Fraction(value) + d = q.denominator + require(d & (d - 1) == 0, "dyadic expected coefficient") + require( + max(abs(q.numerator).bit_length(), d.bit_length()) <= MAX_BITS, + "expected bit limit", + ) + + +def step(values, exponents, event, absolute=False): + """Transpose one event; with absolute coefficients, propagate an l1 bound.""" + kind, r, s, numerator, shift = event + if kind in ("INIT", "CLEAR"): + values[r], exponents[r] = 0, 0 + return + if absolute: + numerator = abs(numerator) + if kind == "SCALE": + require(exponents[r] + shift <= MAX_BITS, "exponent limit") + values[r] *= numerator + exponents[r] += shift + return + level = max(exponents[s], exponents[r] + shift) + require(level <= MAX_BITS, "exponent limit") + values[s] = (values[s] << (level - exponents[s])) + numerator * ( + values[r] << (level - exponents[r] - shift) + ) + exponents[s] = level + if kind == "COPY": + values[r], exponents[r] = 0, 0 + + +def expected_row(row, exponent): + level = max( + [exponent] + [Fraction(q).denominator.bit_length() - 1 for q in row.values()] + ) + coefficients = [] + for column, value in row.items(): + q = Fraction(value) + numerator = q.numerator << (level - q.denominator.bit_length() + 1) + coefficients.append((column, numerator)) + return coefficients, level + + +def plan(n, events, expected): + validate(n, events, expected) + bounds, exponents = [1] * n, [0] * n + largest = 1 + for event in reversed(events): + step(bounds, exponents, event, absolute=True) + largest = max(largest, bounds[event[1]], bounds[event[2]]) + require(largest.bit_length() <= MAX_BITS, "growth limit") + targets = [] + for row, bound, exponent in zip(expected, bounds, exponents, strict=False): + coefficients, level = expected_row(row, exponent) + difference_bound = (bound << (level - exponent)) + sum( + abs(q) for _, q in coefficients + ) + largest = max(largest, difference_bound) + targets.append((coefficients, level)) + width = largest.bit_length() + 1 + require(width <= MAX_BITS + 1, "comparison growth limit") + require(n * n * width <= MAX_PACKED_BITS, "packed memory limit") + return width, targets + + +def check_transpose(n, events, expected): + """Check all n squared endpoint coefficients, never a random fingerprint.""" + width, targets = plan(n, events, expected) + values = [1 << (width * i) for i in range(n)] + exponents = [0] * n + for event in reversed(events): + step(values, exponents, event) + for r, (coefficients, level) in enumerate(targets): + encoded = sum(q << (width * column) for column, q in coefficients) + actual = values[r] << (level - exponents[r]) + require(actual == encoded, "transpose endpoint row " + str(r)) + return { + "columns": n, + "coefficients": n * n, + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + } + + +def source_events(word): + """Project the retained P104 scalar syntax; frame/ownership checks stay external.""" + require( + type(word.get("public")) is int and 1 <= word["public"] <= 1016, "public roles" + ) + program = word.get("program") + require(isinstance(program, list) and len(program) <= MAX_EVENTS, "program limit") + n = word["public"] + 8 + events = [] + for e in program: + require(isinstance(e, list) and len(e) >= 2, "event shape") + kind, r = e[:2] + if kind == "MOVE": + require(len(e) == 5, "MOVE shape") + continue + if kind in ("INIT", "CLEAR"): + require(len(e) == 3, "lifetime shape") + events.append((kind, r, r, 1, 0)) + continue + require(kind in ("ADD", "COPY", "SCALE"), "scalar opcode") + require(len(e) == (4 if kind == "SCALE" else 5), "scalar shape") + require(type(e[-2]) in (int, str), "coefficient syntax") + require(len(str(e[-2])) <= 64, "coefficient text limit") + q = Fraction(e[-2]) + require(q.denominator & (q.denominator - 1) == 0, "dyadic coefficient") + events.append( + ( + kind, + r, + e[2] if kind != "SCALE" else r, + q.numerator, + q.denominator.bit_length() - 1, + ) + ) + live = word.get("live") + require(isinstance(live, list) and len(live) <= n, "live roles") + require( + all(type(r) is int and 0 <= r < word["public"] - 112 for r in live), + "live output bound", + ) + require(len(live) == len(set(live)), "duplicate live role") + expected = [{r: 1} if r < word["public"] else {} for r in range(n)] + for r in live: + expected[r][r + 112] = 1 + return n, events, expected + + +def reverse_columns(word): + return check_transpose(*source_events(word)) diff --git a/research/packed-dyadic-transpose/verify.py b/research/packed-dyadic-transpose/verify.py new file mode 100644 index 0000000000..596ad72ac9 --- /dev/null +++ b/research/packed-dyadic-transpose/verify.py @@ -0,0 +1,224 @@ +"""Exact behavior checks. Produced by Nick Petalas. Apache-2.0.""" + +import gzip +import hashlib +import io +import itertools +import json +import random +import runpy +import statistics +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P = runpy.run_path(str(HERE / "packed.py")) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + source = json.loads((HERE / "SOURCES.json").read_bytes()) + pins = {} + for row in source["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "input SHA256") + pins[row["path"]] = row["sha256"] + require(len(pins) == 2, "two exact workload inputs") + return pins + + +def workload(): + raw = (ROOT / "research/p104-helper-subspace-splits/WORD.json.gz").read_bytes() + require(len(raw) < 2000000, "compressed workload bound") + with gzip.GzipFile(fileobj=io.BytesIO(raw)) as stream: + payload = stream.read(8000001) + require(len(payload) <= 8000000, "expanded workload bound") + return json.loads(payload) + + +def dense_forward(n, events): + """Independent chronological Fraction oracle, then literal transpose.""" + rows = [[Fraction(i == j) for j in range(n)] for i in range(n)] + for kind, r, s, numerator, shift in events: + q = Fraction(numerator, 2**shift) + if kind in ("INIT", "CLEAR"): + rows[r] = [Fraction(0)] * n + elif kind == "SCALE": + rows[r] = [q * x for x in rows[r]] + elif kind == "COPY": + rows[r] = [q * x for x in rows[s]] + else: + require(kind == "ADD", "oracle opcode") + rows[r] = [x + q * y for x, y in zip(rows[r], rows[s], strict=False)] + return [{j: rows[j][i] for j in range(n) if rows[j][i]} for i in range(n)] + + +def reject(action): + try: + action() + except (ValueError, TypeError, KeyError): + return 1 + raise ValueError("invalid case accepted") + + +def check_case(n, events): + expected = dense_forward(n, events) + result = P["check_transpose"](n, events, expected) + require(result["coefficients"] == n * n, "complete coefficient count") + wrong = [dict(row) for row in expected] + wrong[-1][0] = wrong[-1].get(0, Fraction(0)) + 1 + reject(lambda: P["check_transpose"](n, events, wrong)) + return n * n + + +def finite_checks(): + alphabet = [ + ("ADD", 0, 1, 1, 0), + ("ADD", 1, 0, -1, 1), + ("SCALE", 0, 0, -1, 1), + ("SCALE", 1, 1, 3, 0), + ("COPY", 0, 1, 1, 1), + ("COPY", 1, 0, -3, 2), + ("INIT", 0, 0, 1, 0), + ("CLEAR", 1, 1, 1, 0), + ] + cases, coefficients = 0, 0 + for length in range(5): + for events in itertools.product(alphabet, repeat=length): + coefficients += check_case(2, events) + cases += 1 + rng = random.Random(1027) + for n in range(1, 9): + for _ in range(20): + events = [] + for _ in range(40): + r, s = rng.randrange(n), rng.randrange(n) + kind = rng.choice(("ADD", "COPY", "SCALE", "INIT", "CLEAR")) + if r == s and kind in ("ADD", "COPY"): + kind = "SCALE" + events.append( + (kind, r, s, rng.choice((-3, -1, 1, 3)), rng.randrange(4)) + ) + coefficients += check_case(n, events) + cases += 1 + return { + "words": cases, + "literal_coefficients": coefficients, + "wrong_endpoint_rejections": cases, + } + + +def controls(): + check = P["check_transpose"] + identity = [{0: 1}, {1: 1}] + tests = [ + lambda: check(True, [], [{0: 1}]), + lambda: check(1025, [], []), + lambda: check(2, [("BAD", 0, 1, 1, 0)], identity), + lambda: check(2, [("ADD", 0, 0, 1, 0)], identity), + lambda: check(2, [("ADD", 0, 2, 1, 0)], identity), + lambda: check(2, [("SCALE", 0, 0, 1, 33)], identity), + lambda: check(2, [("ADD", 0, 1, 0, 0)], identity), + lambda: check(2, [], [{0: Fraction(1, 3)}, {1: 1}]), + lambda: check(2, [], [{0: True}, {1: 1}]), + lambda: check(2, [("SCALE", 0, 0, 2**19, 0)] * 216, identity), + lambda: check( + 1024, [("SCALE", 0, 0, 2**19, 0)] * 10, [{i: 1} for i in range(1024)] + ), + lambda: check(1, [("SCALE", 0, 0, 1, 0)] * 60001, [{0: 1}]), + ] + # A radix collision without coefficient bounds is not safe equality. + require(-16 + 1 * 16 == 0, "literal radix collision") + require( + reject(lambda: check(2, [], [{0: -15, 1: 1}, {1: 1}])) == 1, + "false equality rejected after safe radix planning", + ) + count = sum(reject(action) for action in tests) + 1 + require(check(1, [], [{0: 1}])["columns"] == 1, "one role") + return count + + +def benchmark_receipt(pins, expected): + recorded = json.loads((HERE / "BENCHMARK.json").read_bytes()) + require(recorded["status"] == "PASS_PACKED_TRANSPOSE_BENCHMARK", "benchmark status") + require(recorded["pairs"] == 5 and recorded["errors"] == 0, "benchmark runs") + require(recorded["inputs"] == pins, "benchmark input binding") + for name, digest in recorded["code_sha256"].items(): + require( + name in ("packed.py", "verify.py", "benchmark.py", "PROOF.md"), + "benchmark source name", + ) + require( + hashlib.sha256((HERE / name).read_bytes()).hexdigest() == digest, + "benchmark source binding", + ) + require(len(recorded["code_sha256"]) == 4, "complete benchmark sources") + samples = recorded["samples"] + require(len(samples) == 10, "ten samples") + for i, row in enumerate(samples): + require(row["side"] == ("dense", "packed")[i % 2], "alternating order") + require( + row["inputs"] == pins and row["result"] == expected and row["errors"] == 0, + "every sample completed", + ) + for side in ("dense", "packed"): + for key in ("checkpoint_seconds", "process_wall_seconds", "peak_rss_bytes"): + values = [r[key] for r in samples if r["side"] == side] + require( + all(type(v) in (float, int) and v > 0 for v in values), + "positive measured values", + ) + require( + recorded["summary"][side][key] + == { + "median": statistics.median(values), + "min": min(values), + "max": max(values), + }, + "derived sample statistics", + ) + return {"recorded_pairs": 5, "timing_repeated_by_this_check": False} + + +def run(): + pins = authenticate() + finite = finite_checks() + rejected = controls() + word = workload() + result = P["reverse_columns"](word) + n, events, expected = P["source_events"](word) + width, _ = P["plan"](n, events, expected) + original = runpy.run_path( + str(ROOT / "research/p104-helper-subspace-splits/local.py") + ) + require(result == original["reverse_columns"](word), "unchanged checkpoint summary") + bad = dict(word) + bad["program"] = word["program"] + [["ADD", 0, 1, "1", 0]] + rejected += reject(lambda: P["reverse_columns"](bad)) + receipt = { + "status": "PASS_PACKED_DYADIC_TRANSPOSE", + "finite": finite, + "controls": rejected, + "workload": result, + "radix_bits": width, + "events": len(word["program"]), + "scalar_events": len(events), + "inputs": pins, + "claim_type": "exact backend equivalence, no new kappa", + } + receipt["benchmark_receipt"] = benchmark_receipt(pins, result) + receipt["new_source_sha256"] = { + name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in ("packed.py", "verify.py", "PROOF.md") + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + run()