diff --git a/research/nonlinear-support-integer-products/README.md b/research/nonlinear-support-integer-products/README.md new file mode 100644 index 0000000000..516e3357c6 --- /dev/null +++ b/research/nonlinear-support-integer-products/README.md @@ -0,0 +1,207 @@ +# Faster complete nonlinear support replay with integer Gaussian products + +This contribution was produced by Nick Petalas. Apache-2.0. + +The complete finite support caller from Chris R / Clear1nsight's +[PR5210](https://github.com/CrocSwap/integer-mult-bounds/pull/5210) takes +24.54% less median wall time in the retained local measurement, from +98.860 ms to 74.598 ms. Complete RESULT/MATRICES files and the original +wrapper report remain byte-identical. This is an empirical tooling improvement +with a scoped arithmetic equivalence proof. No new kappa, predecessor theorem +audit, native supplier or multiplication theorem is claimed. + +The new runner authenticates all 46 pinned source-package files, invokes the +original evidence authentication, copies the original logical inputs into +private scratch, and executes the unchanged finite checker's main function. +Its only scientific substitution is the matrix-product function. It compares +both output files against both frozen modes and checks all copied input bytes +after use. Source files and their notices remain unchanged. + +## Representation and proof + +For each operand A, choose e equal to the maximum binary denominator exponent +among its real and imaginary Fraction components. Write A=2^(-e) A_int, where +A_int has Gaussian-integer entries. For B=2^(-f) B_int, compute + +```text +AB = 2^(-e-f) (A_int B_int) +(a+ib)(c+id) = (ac-bd) + i(ad+bc). +``` + +Every shift is exact because the denominators divide 2^e or 2^f. The ordinary +matrix product is a finite sum of these exact terms. Reconstructing Fraction +components with denominator 2^(e+f) returns the same canonical fractions as +the original implementation. Omitting zero terms changes no sum. Reusing the +caller's immutable zero tuple changes no value or aliasing behavior. + +`products.py` accepts square matrices of dimension 1 through 16, Fraction +numerators of at most 256 bits and dyadic denominator exponents at most 64. +It validates every noncanonical-zero entry. A shared zero is skipped only after +its immutable tuple and Fraction components have been validated. Odd denominators +and larger inputs are explicitly rejected. The product is exact on this accepted +domain; an arbitrary next multiplication need not fit the same input bounds. +The unchanged finite caller's complete execution fits those bounds. + +Induct on the finite caller's product calls. Source inputs are identical; each +replacement returns the same dense list of Gaussian Fraction pairs. Intervening +original operations, branches, controls and serializations receive equal values. +This proves equivalence for this authenticated complete finite caller. It does +not extend the predecessor's written all-width theorem or establish a general +Gaussian-rational product service. + +The first dense normalization prototype was slower under profiling because +conversion dominated the saved Fraction arithmetic. A sparse normalization +prototype then had no measurable arithmetic improvement in five complete runs. +The accepted version skips a validated shared zero before conversion and preserves +that zero on output. Optimization stopped at its first verified improvement. + +## Complete-caller measurements + +Eighteen fresh processes per mode used all six execution orders three times. +There were zero failures, byte-identical complete reports and 277 products in +every adapted run. The integer runner beat the original in all 18 matched rounds +and the reference adapter in 17 of 18. Its slow outlier is retained below. + +| Complete caller | Median ms | Minimum ms | Maximum ms | +| --- | ---: | ---: | ---: | +| Unchanged original wrapper | 98.860 | 97.538 | 131.133 | +| New runner, original Fraction product | 86.495 | 85.847 | 89.032 | +| New runner, integer product | 74.598 | 73.881 | 94.632 | + +The overall improvement combines integer arithmetic with executing the same +finite main inside the authenticated runner rather than in another child +interpreter. The original-product reference adapter isolates the arithmetic +change: its median decreases a further 13.75% with integer products. The +24.54% headline must not be attributed to arithmetic alone. + +Interpreter startup, imports, source authentication, input copying, all checks, +output comparison, serialization and scratch cleanup are inside the parent wall +timer. No result cache is used. A separate profiled reference execution assigns +0.129 of 0.207 seconds to the 277 product calls. Profiled times are excluded from +the sample. Fraction arithmetic and zero comparisons explain that hotspot; +remaining checks and startup limit the complete improvement. + +Environment: CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. Host load was +uncontrolled. Initial load averages were 6.09/4.17/2.73, with another Python +process using one core; final averages were 1.55/2.68/2.43. These are local +observations, not a portable speed guarantee. + +The timing sample binds implementation commit 662e18c310b2fe3e7594bee9290350cab6eacaf6. +A later fix makes only temporary mutation-control copies writable when replaying +from a read-only export. The timed runner and arithmetic bytes are unchanged. + +## Reproduce + +From the worktree root, with this interpreter or another CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonlinear-support-integer-products +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonlinear-support-integer-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nonlinear-support-integer-products/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonlinear-support-integer-products --check-source-history +``` + +Expected markers are `PASS_NONLINEAR_SUPPORT_INTEGER_PRODUCTS`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The verifier compares all 277 actual products and all 70,912 entries with the +retained product function. It also checks 146 additional product fixtures, +including capacity boundaries, ten invalid inputs, a changed source file and +an actual incorrect Gaussian multiplication sign. The retained sign control +rejects the latter. Additional fixtures are execution cases, not distinct-matrix +counts. Complete RESULT/MATRICES match both frozen modes, and the original +wrapper report agrees. Explicit exceptions preserve checks under -O. + +To benchmark, choose a fresh external output path and keep temporary files there: + +```sh +TMPDIR=/path/to/scratch /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonlinear-support-integer-products/benchmark.py --rounds 18 --output /path/to/scratch/new-measurement.json +``` + +The benchmark generates its receipt from completed executions and binds all +four Python files by SHA256. The verifier emits a generated receipt bound to +package hashes. No receipt is handwritten. Default replay leaves the checkout +unchanged. CI checks exact conformance, not wall-time gains. + +## Scope, attribution and limits + +Scientific base is canonical main 2485805a6d47f36ea83ddde6327d453ac82d44dc, +priority revision 8, selected conditional kappa 781451/250000000. The current +selected-binding control passed. The historical card is refined to this +implementation question; selected scientific replay is outside scope. + +Credit Chris R / Clear1nsight for PR5210's finite checker, portable evidence +wrapper, controls, complete output fixtures, reviewed written theorem and its +retained coded-native, released-operator and nonlinear-control predecessors. +The source package retains all prior attribution and notices. This package +does not certify that theorem's proof. Common-denominator matrix arithmetic +and sparse multiplication are classical; their bounded adapter and complete +caller integration are the new implementation contribution. + +Live handoffs, active Discussions, open PR bodies, recent account work, main +README terms, merged object searches and reservations were checked before the +advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294906). +The cached task helper had no usable remote snapshot and covered only 95 of +8,722 main note paths. Live queries and direct main searches supplement it. +Unpublished work and arbitrary historical diffs remain outside coverage. + +Independent human and formal proof-kernel review are unclaimed. No 17-axis +native replay, uniform compiler, physical caller, precision/stock bill, selected +cold replay, Lean or Docker check was run. Larger matrices, odd denominators +and performance on another host remain outside scope. + +## Open next questions + +Can one larger native/caller checker use this representation with a useful +complete runtime gain? First profile a different literal caller and specify its +matrix, denominator and coefficient bounds before adapting products. This small +calibration saves milliseconds; a larger caller contract and complete measurement +are missing. No further optimization of this fixture is reserved. + +## Implementation bounds + +Arithmetic loops are bounded by dimension 16, with at most 4,096 nonzero term +pairs per product. Input normalization reads at most 1,024 Fraction components. +Cleared components have at most 320 bits; output common numerators have magnitude +below 2^645 before reduction. Local values and immutable zero tuples are the +only shared arithmetic state. There is no recursion, floating arithmetic or +generated scientific code. + +Power of Ten rule 3 has a managed-runtime deviation: Python/Fraction allocate +within fixed dimension and bit-size bounds during this finite command. There +is no physical-tape claim. Revisit fixed buffers before a production backend. +The scientific fixture has 277 calls; subprocesses have 30-second timeouts, +registered commands 60-second timeouts. All functions are below 60 physical lines. +Rules 8/9 have a scoped dispatch deviation for loading two pinned source modules +and substituting one named product function. Targets and synchronous lifetimes +are fixed. Tests mutate only their own temporary source copies. Warning-strict +normal/optimized execution and in-memory compilation provide diagnostics; +no separate external static analyzer is claimed. + +Build the Lever led to the rerunnable adapter and complete-caller benchmark. +Prove It Works led to full intermediate products, complete output comparisons +and actual source/sign mutations rather than a digest-only proxy. + +## Raw complete-process wall times + +Times are milliseconds. Every run completed the entire caller. + +| Round | Original | Reference adapter | Integer adapter | +| --- | ---: | ---: | ---: | +| 1 | 97.957208 | 86.273416 | 73.999417 | +| 2 | 99.736500 | 86.360958 | 74.599750 | +| 3 | 98.120917 | 86.035208 | 74.374542 | +| 4 | 98.671291 | 85.846917 | 74.596083 | +| 5 | 105.044458 | 89.031625 | 74.966250 | +| 6 | 98.532666 | 86.961042 | 74.582958 | +| 7 | 98.868167 | 86.272125 | 94.631791 | +| 8 | 131.133375 | 86.792583 | 75.544000 | +| 9 | 100.199166 | 86.043750 | 75.397125 | +| 10 | 98.602959 | 87.586875 | 74.114208 | +| 11 | 99.399917 | 86.800584 | 74.520916 | +| 12 | 125.302208 | 85.972416 | 74.286583 | +| 13 | 104.901917 | 87.156875 | 73.880958 | +| 14 | 98.217625 | 87.272709 | 74.977250 | +| 15 | 98.463583 | 86.629209 | 74.477583 | +| 16 | 99.568250 | 86.309792 | 74.947125 | +| 17 | 97.538417 | 86.324250 | 74.883292 | +| 18 | 98.852792 | 88.388750 | 75.118583 | diff --git a/research/nonlinear-support-integer-products/SOURCES.json b/research/nonlinear-support-integer-products/SOURCES.json new file mode 100644 index 0000000000..2f3c894f60 --- /dev/null +++ b/research/nonlinear-support-integer-products/SOURCES.json @@ -0,0 +1,294 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/.gitattributes", + "usage": "input", + "git_blob": "ad1d31d8e2bb7ed68388441b61d6367083775650", + "sha256": "745b2bf6e11d5ebbed7715dca52b8f5ed8d1a3309a13e7a94be8399bf0a9a20a" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/EVIDENCE.json", + "usage": "input", + "git_blob": "c867e8e5f38ca696d437a517138838e217dbbe18", + "sha256": "e2759cf096a8e80ea1493dd4f7ed716ba509f5b0fd02ff16e01a8550a6ab4671" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/HISTORY.md", + "usage": "input", + "git_blob": "30d6075beaa3647f19fd9d38f5a3413d865516cd", + "sha256": "3ce6913c4a8be2f86c0991fee3fd3d0153c1caf33efc1cbb8816403213328d78" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/NOTICE", + "usage": "input", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/README.md", + "usage": "input", + "git_blob": "d586643c285e93ccfa0292239bbab4a12dda0edf", + "sha256": "c9fddb95e7e3001a16a13601869e824c4130766dbd6353c20f1d15dd0bcd5cb6" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/SOURCE-NOTICE", + "usage": "input", + "git_blob": "985b6b1bc76dacd54a9cbe9897f3b659ae93c3a4", + "sha256": "317b1c5e040bab50ebfc3d0cdb3a47fc30e2f872a00895f563d7931749b1cc7b" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/SOURCES.json", + "usage": "input", + "git_blob": "a238d5894ce36d4114905c1ea1f85c0e55307059", + "sha256": "15e8fa676f198064d2a94097e85f612754a38bcfe032cbb96cc22dcabe57090b" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/TASK.json", + "usage": "input", + "git_blob": "e455298329b6f47e8f043e7b857191faefa26192", + "sha256": "25fb472e34753cfe1badc29dac62499d2e259ed35ac5b62732ce3ae76cbfcc41" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/VERIFY.json", + "usage": "input", + "git_blob": "56a932e8e8f3f4242e05afd206b5a68df2bee6d0", + "sha256": "2c564b69e77fb1f125f0e9b85be93c192c185f722571ab502a43955d31bc9cdf" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/FREEZE.json", + "usage": "input", + "git_blob": "fa301cbc03a63acbb9f08bc5839569137cedbf1e", + "sha256": "090145aee55d41069406b642942f5c9feca79c6908846998df8358da9064f043" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/MATRICES-OPTIMIZED.json", + "usage": "input", + "git_blob": "7933c196ec5c86a3b1197e66dc42b9d7477a9de9", + "sha256": "02bfc8bd2d1fd9a38de2213d8729aca10feee634de00290f83a94f2bfb19f611" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/MATRICES.json", + "usage": "input", + "git_blob": "7933c196ec5c86a3b1197e66dc42b9d7477a9de9", + "sha256": "02bfc8bd2d1fd9a38de2213d8729aca10feee634de00290f83a94f2bfb19f611" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/RESULT-OPTIMIZED.json", + "usage": "input", + "git_blob": "e0fbc46dbb868aedf11bddc2913885b23ee020fc", + "sha256": "4639a2721e1e90f0ab4104ed07a2395701e12e3bbcabcb760317d3a63dab7e9e" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/RESULT.json", + "usage": "input", + "git_blob": "e0fbc46dbb868aedf11bddc2913885b23ee020fc", + "sha256": "4639a2721e1e90f0ab4104ed07a2395701e12e3bbcabcb760317d3a63dab7e9e" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/REVIEW.md", + "usage": "input", + "git_blob": "1f971549d4c11b479412d9915b6cafa18db1f378", + "sha256": "db09dfb39e4dd5bdecc00bcef32d4db77adf9c11e7f073d119c418395fc0f3de" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/SHA256SUMS", + "usage": "input", + "git_blob": "401a248bc0eedc16908b6ddb52bdcb77e5a13869", + "sha256": "180502cb8356bd9c8d92bf8f06da25d89f21efeb18a8135723b5bd847256edc4" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/SOURCE-FACTS.md", + "usage": "input", + "git_blob": "80ee1eadc150c1edaff5a09ad0568a0e438ab483", + "sha256": "c6e2546054ac68cbec6a579bf7558a523d1a8843c160a70250b24a10220f90fe" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/finite-check/check_support.py", + "usage": "input", + "git_blob": "9cff7d7616d88d97664cbadebad325d161eabd1f", + "sha256": "91115f8380c01d6e788acf27870991b80a6c6ee02d5363396408e4e08dad149c" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/AUTHOR-INPUTS.json", + "usage": "input", + "git_blob": "c788fcfc76c63b5899e2c872851d4b0628365a72", + "sha256": "228c3da4d04e20607bdefabd86d682a8d6dd4c09e35c6c0a786bc1e18d3facd4" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/AUTHOR-REPORT.md", + "usage": "input", + "git_blob": "3d6499a9fe72fe4ce47303595364048f3e78a05b", + "sha256": "19932a49cda97acb2e3f4933f95d4bed5598e441d7593132bd07d15a63c23731" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/CAPTURES.json", + "usage": "input", + "git_blob": "a2ceca100ea4febcf43622d4a9bbadc37e0507b1", + "sha256": "7b4206e960c709bec809731f8de1698b65d3335ebb207d5ae4f90cc9c04e0ca3" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/INDEPENDENT-REVIEW.md", + "usage": "input", + "git_blob": "92f63e0553a033f1a7ee2f73ceba07315b0247ed", + "sha256": "3a255cfb2efb874fcf3cc111dacd145901e2b1018a7cfa60f12d251d3239b4e5" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/REVIEW-SOURCES.json", + "usage": "input", + "git_blob": "d31a79799738d9704e3a415a840ebc239dde388f", + "sha256": "769e777c6dce6567a77c6aa4f89fd0120955b56e2554001d912d26669b492306" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/01-PAID-SHEAR-SCREEN.md", + "usage": "input", + "git_blob": "296523437fa0e1acb940f3cf9ad28247c7cc8057", + "sha256": "81fefcf4a1be0be04076e7cba0e27ba4afe732d4810a13b0a76dbe827967c10c" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/03-operator-valued-gather-rank-boundary.md", + "usage": "input", + "git_blob": "d5dd564d8e9b760b76fcfd4ca2c2a630fe469402", + "sha256": "847dccf3cc3a0938b67a22e3074cd06e825f7881e0a90dfad6c29f3963d41f58" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/04-PROOF.md", + "usage": "input", + "git_blob": "6ddce7b794a8676bab5514f29e88c90117b26c88", + "sha256": "96c617b306d50fce2b0f4f88afe1f6103d11326b402c2e4980c522c9c48092db" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/05-REPORT.md", + "usage": "input", + "git_blob": "8a200e2535e9ac5eba891f914f0d319923977011", + "sha256": "363f66bb655dd9100438aa4ae405025baafeddcaaaad0b8d0a43eecaa43ee784" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/06-REVIEW.md", + "usage": "input", + "git_blob": "f06f34d3334c6c1fcb60de41e29b180b2e26a4a9", + "sha256": "23b5aa5df049cb4a8fe3349c054e27d84ca151e29e263c658670639bad082428" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/07-REPORT.md", + "usage": "input", + "git_blob": "ddc6e82c07f65dae97a0b1384c2f0360fc3fabbe", + "sha256": "b8b785a815852069b27ee6b18337b6ecd64127c7a22985d0e4221a2fc11bd53a" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/08-RESULT.json", + "usage": "input", + "git_blob": "72aa4afa0490342a9902ac4a24da12e5ad787601", + "sha256": "b11a56c453c6f174780edd0cd19c638da7d1552ac9f3f0ff6f8340d8ada382ae" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/09-operator-valued-paid-theorem-fit.md", + "usage": "input", + "git_blob": "60529c988b10f148dae7f8ddea4126c7a68d2958", + "sha256": "660225cc59b75eaff65f241a10373f3a4f312981dc386b5833d653dba3d14460" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/RAW-GIT-5126-PROOF.md", + "usage": "input", + "git_blob": "1ebf18af5b8b6e064d6433460f4e6a0c6b832e2b", + "sha256": "495a1cd85cc45020adf2205f196b57dc4f65f1eb763fc4951facdb4ccbafc768" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/FILES.json", + "usage": "input", + "git_blob": "786a79bd99537a23bf0e3fd494a40f9fe6d0eb8f", + "sha256": "d6b03962432cbb2880dff5825daf6eae9637f8ce614c82de15aaa07ffb90571d" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/RESULT.json", + "usage": "input", + "git_blob": "0eb6ef3ce91e62287dd89d2725aa0b680ef12d20", + "sha256": "8bdf9491dc7e9c8ac9883e6be3845d3aa9b05930b0c1699057baf7fb33c7df09" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/REVIEW.md", + "usage": "input", + "git_blob": "f6db55e8b1218d4902ecec3e41db681fd21c8a1f", + "sha256": "0b0fe1c33eea85ccd92a3423a705fd086c6f2669f1a47f37fba9c1ca4ae91973" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/SOURCES.json", + "usage": "input", + "git_blob": "85bfcd8f694e7341ae875f36bb8fe6a37b1ab165", + "sha256": "0689d9a2bd640fab5b3e71765800064ff8689484d39b975b7834aadbf579ea0e" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/FIRST-DRAFT.md", + "usage": "input", + "git_blob": "a847cb3716f046bc44a4a3fe4b708e9405fd6d2a", + "sha256": "669b9b2a3c1797c80d46ed44c119104cbbc36b893877cc8612dcc8b3e50d64fb" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PHYSICAL.md", + "usage": "input", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-PROOF.md", + "usage": "input", + "git_blob": "08b35b275ac258bac7cde0e289761011acd56d8e", + "sha256": "c20b2f13e875d9e1fb6d0743693f9deccc4f7d68dcdc55ec241324ed3d7de7bc" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-SOURCE-CHECKER.py", + "usage": "input", + "git_blob": "9b9f57090ddeb1a80a7af467bc133662a435c105", + "sha256": "025ba8f3f63fa4f4d7155a32f0f51de210693f6b425b047312d5f232e96fdc5f" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-SOURCES.json", + "usage": "input", + "git_blob": "ef42d1e3d12649d233dca75399afe8af01f62b21", + "sha256": "e810407fc34de1f3af196fc86e91e680075ff982bbc6fe19d6ebb02f2a0c0d9c" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/REVIEWED-PROOF.md", + "usage": "input", + "git_blob": "277a32368a8df3e63077c2783fe4eb89bec5ab64", + "sha256": "76bea47531ed557c0c9cb210c4324d6000c74415bf13e5747b7036567853f6ef" + }, + { + "path": "research/nonlinear-monomial-control-ceiling/verify.py", + "usage": "input", + "git_blob": "500e06d1193693108bc4eedc1177a0f12a8eea31", + "sha256": "d090adc098a2e4f0a03201bff5803828e7f474cbda6219e286ad6b7701836241" + } + ] +} diff --git a/research/nonlinear-support-integer-products/TASK.json b/research/nonlinear-support-integer-products/TASK.json new file mode 100644 index 0000000000..d9f8375b40 --- /dev/null +++ b/research/nonlinear-support-integer-products/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Accelerate the complete PR5210 finite support caller using bounded scaled-integer Gaussian products, with byte-identical complete outputs.", + "scope_change_reason": "Select one previously unoptimized finite caller and change its arithmetic representation; no predecessor scientific audit or theorem expansion.", + "bottleneck_link": "Reduce exact finite calibration cost while retaining source authentication and every existing control. This is verifier engineering, not a supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Stop optimizing at the first verified complete-caller improvement; preserve failed conversion evidence and publish only the bounded adapter.", + "outcome": "completed", + "evidence": "README.md records the complete 18-round timing table and proof. verify.py compares all 277 products, 70912 entries, complete RESULT/MATRICES and the original wrapper report. benchmark.py reruns the fresh-process comparison.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual larger native/caller checker use this representation with a useful complete runtime gain?", + "why_it_matters": "The present small finite caller saves milliseconds and establishes no full supplier throughput gain.", + "first_step": "Profile one different caller and specify its denominator, coefficient-size and matrix-dimension bounds before adapting its products.", + "blocked_by": "A source-specific bounded contract and complete-caller measurement are not supplied here." + } + ] +} diff --git a/research/nonlinear-support-integer-products/VERIFY.json b/research/nonlinear-support-integer-products/VERIFY.json new file mode 100644 index 0000000000..2d67847239 --- /dev/null +++ b/research/nonlinear-support-integer-products/VERIFY.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/nonlinear-monomial-control-ceiling/.gitattributes", + "research/nonlinear-monomial-control-ceiling/EVIDENCE.json", + "research/nonlinear-monomial-control-ceiling/HISTORY.md", + "research/nonlinear-monomial-control-ceiling/LICENSE", + "research/nonlinear-monomial-control-ceiling/NOTICE", + "research/nonlinear-monomial-control-ceiling/README.md", + "research/nonlinear-monomial-control-ceiling/SOURCE-NOTICE", + "research/nonlinear-monomial-control-ceiling/SOURCES.json", + "research/nonlinear-monomial-control-ceiling/TASK.json", + "research/nonlinear-monomial-control-ceiling/VERIFY.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/FREEZE.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/MATRICES-OPTIMIZED.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/MATRICES.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/RESULT-OPTIMIZED.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/RESULT.json", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/REVIEW.md", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/SHA256SUMS", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/SOURCE-FACTS.md", + "research/nonlinear-monomial-control-ceiling/evidence/finite-check/check_support.py", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/AUTHOR-INPUTS.json", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/AUTHOR-REPORT.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/CAPTURES.json", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/INDEPENDENT-REVIEW.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/REVIEW-SOURCES.json", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/01-PAID-SHEAR-SCREEN.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/03-operator-valued-gather-rank-boundary.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/04-PROOF.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/05-REPORT.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/06-REVIEW.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/07-REPORT.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/08-RESULT.json", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/09-operator-valued-paid-theorem-fit.md", + "research/nonlinear-monomial-control-ceiling/evidence/paid-control/captures/RAW-GIT-5126-PROOF.md", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/FILES.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/RESULT.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/REVIEW.md", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/SOURCES.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/CODE.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/FIRST-DRAFT.md", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/NORMALIZERS.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PHYSICAL.md", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-PROOF.md", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-SOURCE-CHECKER.py", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/PREDECESSOR-SOURCES.json", + "research/nonlinear-monomial-control-ceiling/evidence/proof-review/frozen/REVIEWED-PROOF.md", + "research/nonlinear-monomial-control-ceiling/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "146 additional exact products, ten invalid-input controls, all 277 retained products and 70912 entries, complete frozen RESULT/MATRICES and original wrapper report, actual changed-source and complex-sign CLI rejection controls. Timings are not a CI predicate." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "146 additional exact products, ten invalid-input controls, all 277 retained products and 70912 entries, complete frozen RESULT/MATRICES and original wrapper report, actual changed-source and complex-sign CLI rejection controls. Timings are not a CI predicate." + } + ] +} diff --git a/research/nonlinear-support-integer-products/benchmark.py b/research/nonlinear-support-integer-products/benchmark.py new file mode 100644 index 0000000000..30c23fc0a4 --- /dev/null +++ b/research/nonlinear-support-integer-products/benchmark.py @@ -0,0 +1,81 @@ +"""Measure complete fresh-process callers; timing is local evidence only. + +Produced by Nick Petalas. Apache-2.0. +""" +import argparse +from hashlib import sha256 +from itertools import permutations +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def measure(command, expected, counts): + started = time.perf_counter() + completed = subprocess.run(command, cwd=ROOT, capture_output=True, timeout=30) + elapsed = time.perf_counter() - started + if completed.returncode: + raise ValueError("Caller failed: " + completed.stderr.decode()) + if expected is not None and completed.stdout != expected: + raise ValueError("Complete caller output differs") + if counts and json.loads(completed.stderr) != {"products": 277, "compared_entries": 0}: + raise ValueError("Caller work count differs") + return elapsed, completed.stdout + + +def run(rounds): + prefix = [sys.executable, "-I", "-W", "error", "-B"] + commands = { + "original": prefix + ["research/nonlinear-monomial-control-ceiling/verify.py"], + "reference": prefix + ["research/nonlinear-support-integer-products/runner.py", "--mode", "reference"], + "integer": prefix + ["research/nonlinear-support-integer-products/runner.py"], + } + orders = tuple(permutations(commands)) + rows = [] + expected = None + for number in range(rounds): + for mode in orders[number % len(orders)]: + elapsed, output = measure(commands[mode], expected, mode != "original") + if expected is None: + expected = output + rows.append({"round": number, "mode": mode, "seconds": elapsed}) + summary = {} + for mode in commands: + values = [row["seconds"] for row in rows if row["mode"] == mode] + summary[mode] = {"median_seconds": statistics.median(values), + "minimum_seconds": min(values), "maximum_seconds": max(values)} + hashes = {str(p.relative_to(ROOT)): sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.glob("*.py"))} + return {"schema": 1, "rows": rows, "summary": summary, "commands": commands, + "errors": 0, "rounds_per_mode": rounds, "products_per_adapted_caller": 277, + "complete_stdout_sha256": sha256(expected).hexdigest(), "implementation_sha256": hashes, + "python": platform.python_version(), "platform": platform.platform(), + "cpu_count": os.cpu_count(), "load_average_at_end": os.getloadavg(), + "scope": "Fresh complete processes include interpreter startup, all source authentication, all finite checks, output comparison and private scratch cleanup. Shared-host load is uncontrolled. No portable speed guarantee."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=18) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + if not 6 <= args.rounds <= 60: + raise ValueError("rounds must be between six and sixty") + if args.output.exists(): + raise ValueError("output must be new") + result = run(args.rounds) + with args.output.open("x") as output: + output.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(json.dumps(result["summary"], sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/nonlinear-support-integer-products/products.py b/research/nonlinear-support-integer-products/products.py new file mode 100644 index 0000000000..d3e826af44 --- /dev/null +++ b/research/nonlinear-support-integer-products/products.py @@ -0,0 +1,79 @@ +"""Exact Gaussian-dyadic matrix products with one denominator per operand. + +Produced by Nick Petalas. Apache-2.0. +""" +from fractions import Fraction + +MAX_DIMENSION = 16 +MAX_NUMERATOR_BITS = 256 +MAX_DENOMINATOR_BITS = 64 +ZERO = (Fraction(0), Fraction(0)) + + +def scaled(matrix, zero): + """Validate a bounded square matrix and clear its dyadic denominators.""" + size = len(matrix) + if not 1 <= size <= MAX_DIMENSION: + raise ValueError("matrix dimension") + exponent = 0 + nonzero = [] + for row in matrix: + if len(row) != size: + raise ValueError("square matrix required") + entries = [] + for column, entry in enumerate(row): + if entry is zero: + continue + if len(entry) != 2: + raise ValueError("Gaussian pair required") + if any(type(value) is not Fraction for value in entry): + raise ValueError("Fraction components required") + if not entry[0].numerator and not entry[1].numerator: + continue + for value in entry: + denominator = value.denominator + if denominator & (denominator - 1): + raise ValueError("non-dyadic component") + bits = denominator.bit_length() - 1 + if bits > MAX_DENOMINATOR_BITS: + raise ValueError("denominator capacity") + if abs(value.numerator).bit_length() > MAX_NUMERATOR_BITS: + raise ValueError("numerator capacity") + exponent = max(exponent, bits) + entries.append((column, entry)) + nonzero.append(entries) + rows = [] + for row in nonzero: + converted = [] + for column, (real, imaginary) in row: + re = real.numerator << (exponent - (real.denominator.bit_length() - 1)) + im = imaginary.numerator << (exponent - (imaginary.denominator.bit_length() - 1)) + converted.append((column, (re, im))) + rows.append(converted) + return rows, exponent + + +def product(left, right, zero=ZERO): + """Return the ordinary matrix product, with exact Fraction output pairs.""" + if type(zero) is not tuple or len(zero) != 2 or any( + type(value) is not Fraction or value.numerator for value in zero): + raise ValueError("zero pair required") + a, first = scaled(left, zero) + b, second = scaled(right, zero) + size = len(a) + if len(b) != size: + raise ValueError("matrix dimensions differ") + denominator = 1 << (first + second) + output = [[zero for _ in range(size)] for _ in range(size)] + for i, row in enumerate(a): + real = [0] * size + imaginary = [0] * size + for k, (ar, ai) in row: + for j, (br, bi) in b[k]: + real[j] += ar * br - ai * bi + imaginary[j] += ar * bi + ai * br + for j in range(size): + if real[j] or imaginary[j]: + output[i][j] = (Fraction(real[j], denominator), + Fraction(imaginary[j], denominator)) + return output diff --git a/research/nonlinear-support-integer-products/runner.py b/research/nonlinear-support-integer-products/runner.py new file mode 100644 index 0000000000..e467ae7885 --- /dev/null +++ b/research/nonlinear-support-integer-products/runner.py @@ -0,0 +1,130 @@ +"""Run the complete retained finite caller using either exact product engine. + +The fixture, checks, outputs and frozen predecessor files remain unchanged. +Produced by Nick Petalas. Apache-2.0. +""" +import argparse +import contextlib +from hashlib import sha256 +import importlib.util +import io +import json +from pathlib import Path +import shutil +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/nonlinear-monomial-control-ceiling" + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + if spec is None or spec.loader is None: + raise ValueError("Python module unavailable") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + path = ROOT / row["path"] + if path.is_symlink() or sha256(path.read_bytes()).hexdigest() != row["sha256"]: + raise ValueError("Source pin mismatch: " + row["path"]) + owner = load(SOURCE / "verify.py", "retained_portable_wrapper") + return owner.authenticate() + + +def prepare(destination): + review = SOURCE / "evidence/proof-review" + logical = { + "outputs/nonlinear-monomial-control-ceiling-20261023/PROOF.md": "REVIEWED-PROOF.md", + "outputs/released-operator-intersection-20261023/PROOF.md": "PREDECESSOR-PROOF.md", + "outputs/released-operator-intersection-20261023/SOURCES.json": "PREDECESSOR-SOURCES.json", + "outputs/released-operator-intersection-20261023/frozen/PHYSICAL.md": "PHYSICAL.md", + } + for name, source in logical.items(): + target = destination / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(review / "frozen" / source, target) + work = destination / "outputs/nonlinear-monomial-support-check-20261023" + work.mkdir() + shutil.copyfile(SOURCE / "evidence/finite-check/check_support.py", work / "check_support.py") + return work, logical + + +def execute(mode, work): + checker = load(work / "check_support.py", "retained_finite_checker") + integer = load(HERE / "products.py", "scaled_gaussian_products") + reference = checker.product + counts = {"products": 0, "compared_entries": 0} + + def observed(left, right): + counts["products"] += 1 + result = reference(left, right) if mode == "reference" else integer.product(left, right, checker.ZERO) + if mode == "differential": + expected = reference(left, right) + if result != expected: + raise ValueError("Complete product disagreement") + counts["compared_entries"] += checker.N * checker.N + return result + + checker.product = observed + printed = io.StringIO() + with contextlib.redirect_stdout(printed): + checker.main() + return json.loads(printed.getvalue()), counts + + +def outputs(work, logical, destination): + finite = SOURCE / "evidence/finite-check" + for stem in ("RESULT", "MATRICES"): + data = (work / (stem + ".json")).read_bytes() + for suffix in ("", "-OPTIMIZED"): + if data != (finite / (stem + suffix + ".json")).read_bytes(): + raise ValueError("Complete generated output differs: " + stem + suffix) + review = SOURCE / "evidence/proof-review/frozen" + for name, source in logical.items(): + if (destination / name).read_bytes() != (review / source).read_bytes(): + raise ValueError("Private source capture changed") + return json.loads((work / "RESULT.json").read_text()), (work / "MATRICES.json").read_bytes() + + +def run(mode): + manifest = authenticate() + with tempfile.TemporaryDirectory(prefix="nonlinear-integer-") as temporary: + destination = Path(temporary) + work, logical = prepare(destination) + compact, counts = execute(mode, work) + result, matrices = outputs(work, logical, destination) + review = SOURCE / "evidence/proof-review" + finite = SOURCE / "evidence/finite-check" + report = { + "status": "PASS_PORTABLE_NONLINEAR_FINITE_SUPPORT_ONLY", + "immutable_evidence_files": len(manifest["files"]), + "written_proof_sha256": sha256((review / "frozen/REVIEWED-PROOF.md").read_bytes()).hexdigest(), + "independent_review_sha256": sha256((review / "REVIEW.md").read_bytes()).hexdigest(), + "finite_result_sha256": sha256((finite / "RESULT.json").read_bytes()).hexdigest(), + "finite_matrices_sha256": sha256(matrices).hexdigest(), + "positive_examples": compact["positive_examples"], + "terminal_sandwiches": result["terminal_nonmonomial_count"], + "scope": "Finite exact16x16 support examples and controls only. Independently reviewed written proof supplies sufficiently-large-width fixed finite complete-product support theorem. No17-axis/all-width phase/native/compiler/caller or kappa replay.", + } + return report, counts + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mode", choices=("integer", "reference", "differential"), default="integer") + args = parser.parse_args() + report, counts = run(args.mode) + print(json.dumps(report, indent=2, sort_keys=True)) + print(json.dumps(counts, sort_keys=True), file=sys.stderr) + + +if __name__ == "__main__": + main() diff --git a/research/nonlinear-support-integer-products/verify.py b/research/nonlinear-support-integer-products/verify.py new file mode 100644 index 0000000000..3f867caa50 --- /dev/null +++ b/research/nonlinear-support-integer-products/verify.py @@ -0,0 +1,131 @@ +"""Verify the bounded product adapter and its complete retained caller. + +Produced by Nick Petalas. Apache-2.0. +""" +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import products +import runner + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def reference(a, b): + size = len(a) + result = [[(F(0), F(0)) for _ in range(size)] for _ in range(size)] + for i in range(size): + for j in range(size): + real, imaginary = F(0), F(0) + for k in range(size): + ar, ai = a[i][k] + br, bi = b[k][j] + real += ar * br - ai * bi + imaginary += ar * bi + ai * br + result[i][j] = real, imaginary + return result + + +def fixtures(): + zero = products.ZERO + values = ((F(0), F(0)), (F(1), F(0)), (F(0), F(1)), + (F(-1, 2), F(3, 4)), (F(5, 8), F(-1, 16))) + matrices = [] + for shift in range(12): + matrices.append([[values[(shift + i * 2 + j * 3) % len(values)] + for j in range(2)] for i in range(2)]) + for a in matrices: + for b in matrices: + need(products.product(a, b) == reference(a, b), "mixed dyadic product") + boundary = (F((1 << 256) - 1, 1 << 64), F(-1, 1 << 64)) + need(products.product([[boundary]], [[boundary]]) == + reference([[boundary]], [[boundary]]), "capacity-boundary product") + diagonal = [[zero for _ in range(16)] for _ in range(16)] + for i in range(16): + diagonal[i][i] = values[1 + i % 4] + need(products.product(diagonal, diagonal) == reference(diagonal, diagonal), + "maximum-dimension product") + return 146 + + +def boundaries(): + zero = products.ZERO + cases = [([], [], zero), ([[zero]] * 17, [[zero]], zero), + ([[zero, zero]], [[zero]], zero), ([[()]], [[zero]], zero), + ([[(0, 0)]], [[zero]], zero), + ([[(F(1, 3), F(0))]], [[zero]], zero), + ([[(F(1, 1 << 65), F(0))]], [[zero]], zero), + ([[(F(1 << 256), F(0))]], [[zero]], zero), + ([[zero]], [[zero, zero], [zero, zero]], zero), + ([[zero]], [[zero]], (F(1), F(0)))] + for left, right, canonical_zero in cases: + try: + products.product(left, right, canonical_zero) + except (TypeError, ValueError): + continue + raise ValueError("invalid product accepted") + return len(cases) + + +def mutation_controls(): + with tempfile.TemporaryDirectory(prefix="integer-controls-") as temporary: + root = Path(temporary) + package = root / "research" / HERE.name + source = root / "research" / runner.SOURCE.name + shutil.copytree(HERE, package) + shutil.copytree(runner.SOURCE, source) + checker = source / "evidence/finite-check/check_support.py" + checker.chmod(checker.stat().st_mode | 0o200) + original = checker.read_bytes() + checker.write_bytes(original + b"\n") + command = [sys.executable, "-I", "-W", "error", "-B", str(package / "runner.py")] + if sys.flags.optimize: + command.insert(2, "-O") + changed = subprocess.run(command, capture_output=True, timeout=30) + need(changed.returncode != 0 and b"Source pin mismatch" in changed.stderr, + "changed source was not invalidated") + checker.write_bytes(original) + adapter = package / "products.py" + adapter.chmod(adapter.stat().st_mode | 0o200) + original_adapter = adapter.read_text() + needle = "real[j] += ar * br - ai * bi" + need(original_adapter.count(needle) == 1, "mutation site changed") + adapter.write_text(original_adapter.replace(needle, "real[j] += ar * br + ai * bi")) + changed = subprocess.run(command, capture_output=True, timeout=30) + need(changed.returncode != 0 and b"Q inverse is actual adjoint" in changed.stderr, + "wrong Gaussian product sign was not rejected by retained control") + return 2 + + +def main(): + products_checked = fixtures() + invalid = boundaries() + report, counts = runner.run("differential") + need(counts == {"products": 277, "compared_entries": 70912}, "complete work count") + command = [sys.executable, "-I", "-W", "error", "-B", str(runner.SOURCE / "verify.py")] + if sys.flags.optimize: + command.insert(2, "-O") + original = subprocess.run(command, capture_output=True, timeout=30, check=True) + need(json.loads(original.stdout) == report, "unchanged complete wrapper report") + mutations = mutation_controls() + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print(json.dumps({"status": "PASS_NONLINEAR_SUPPORT_INTEGER_PRODUCTS", + **counts, "additional_products": products_checked, + "invalid_inputs_rejected": invalid, "mutations_rejected": mutations, + "complete_report": report, "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()