diff --git a/research/p104-causal-retimed-step/ENVIRONMENT.json b/research/p104-causal-retimed-step/ENVIRONMENT.json new file mode 100644 index 0000000000..13e51eb499 --- /dev/null +++ b/research/p104-causal-retimed-step/ENVIRONMENT.json @@ -0,0 +1,15 @@ +{ + "checked_at": "2026-11-10T13:42:11.195213+00:00", + "python": "3.14.7 (main, Aug 5 2026, 10:29:49) [Clang 21.0.0 (clang-2100.1.1.101)]", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "machine": "arm64", + "upstream_main": "17469fff78c22941280f04d39dc5a1faee09c840", + "priority_revision": 8, + "source_head": "2ee11a4460f23abf06d16b12f18c8ef9aca889f1", + "local_python312_available": false, + "replay": "python3 -I -B research/p104-causal-retimed-step/verify.py", + "evidence": "source-aware author checks; no independent human/kernel acceptance", + "final_replay_verified_at": "2026-11-10T13:45:22.716936+00:00", + "final_log_sha256": "5548b85bfc18ea37528cd3fb2688dde3772330d6cf8b9401d893a33c7292f7d7", + "final_log_file": "REPLAY.txt" +} diff --git a/research/p104-causal-retimed-step/INPUTS.json b/research/p104-causal-retimed-step/INPUTS.json new file mode 100644 index 0000000000..504f4e425b --- /dev/null +++ b/research/p104-causal-retimed-step/INPUTS.json @@ -0,0 +1,422 @@ +{ + "source_head": "2ee11a4460f23abf06d16b12f18c8ef9aca889f1", + "repository": "https://github.com/ToikY/integer-mult-bounds", + "archive_sha256": "25f3952808ade8642cdd66425d6963fe8639adafef1cab33e213f0736fd68287", + "source_canonical_sha256": "311069e5faeef999a0b3f2fd8ae9c256b67b40a368998c5c31cd38a500f385e3", + "files": [ + { + "path": "research/peer-move-retiming/BASELINE-EXPORT.json", + "size": 7436, + "sha256": "d8539c9f4d7625bb9f3d2f6f5603cda407696dda73f7d36f6bf6677b55c5e8ac", + "git_blob": "0970c8ac8be4b7e4689afc83bf940980e302bdb6" + }, + { + "path": "research/peer-move-retiming/LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "path": "research/peer-move-retiming/NOTICE", + "size": 375, + "sha256": "9245f74c7706c9568cc2bf7cf71301ab89100437cf9453e7762145061db8a711", + "git_blob": "a773fca904d7c867c89bcfd934f46168739eaff4" + }, + { + "path": "research/peer-move-retiming/README.md", + "size": 5076, + "sha256": "376cc000f3f046f9480d630bf57225ba788e8cb5359655e7bdb4def95bbd1423", + "git_blob": "7bf8370a1ccec52bdf15f91d259da86aa69a1fa7" + }, + { + "path": "research/peer-move-retiming/RESULT.json", + "size": 26218, + "sha256": "555310519298a04dc00dc72b34073e4ad868620e7abb7a009d520ced27a2c4ba", + "git_blob": "9310cd05b562329a5a49d1325c6a587ee2cdd7a1" + }, + { + "path": "research/peer-move-retiming/SOURCES.json", + "size": 11204, + "sha256": "026561d27985a431d431c16e5efc376e652b215d1442d81e0e612114ac95dc91", + "git_blob": "4215494303adf1fb4adf3a2cff03c762ca816ed3" + }, + { + "path": "research/peer-move-retiming/TASK.json", + "size": 7993, + "sha256": "a56a6dd92ffafdf016715e1292bf4351d51841298ee7b044624cf889a99c7c73", + "git_blob": "348f162a109a8d723a20d86f953ed61df4bfdc3a" + }, + { + "path": "research/peer-move-retiming/VERIFY.json", + "size": 2729, + "sha256": "9165f73c5f36e97af600d0e1fce86a1b996946ea4cc0d5333dbf1258b7aa74f2", + "git_blob": "c820490ab62fea4dc1ce96b284879f07451a4f39" + }, + { + "path": "research/peer-move-retiming/build_candidate.py", + "size": 4100, + "sha256": "d06f0f5599bbbf190a0602325ae26ed6008245cd4abb40ff72fa266d616169cb", + "git_blob": "9d6c19b264967b76b2558482be2002ca7653be97" + }, + { + "path": "research/peer-move-retiming/verify.py", + "size": 10160, + "sha256": "5ff920901617e935856276e6ac0d4d47d4ed6692b4cbf35e536718395fa4c542", + "git_blob": "efedf995cc96cac29177703669a63c890fff8fb6" + }, + { + "path": "research/shared-wire-split-composition/CONSTRUCTION-REVIEW.md", + "size": 5496, + "sha256": "038392a7c5f1705b1978bcc35f9dc889d4ccd457a1f32c384a500c81259e978b", + "git_blob": "3230ed0dfba7da6ef3fa8738ee36acc6d4cbb004" + }, + { + "path": "research/shared-wire-split-composition/CONSTRUCTION.md", + "size": 8275, + "sha256": "40249ccc0854393aa3a6ff14845879407ebeb0bc365f14c49ab155489addb436", + "git_blob": "863cb8543e1e413691da3161a6195ffcd9bdbf3a" + }, + { + "path": "research/shared-wire-split-composition/FULL-RESULT.json", + "size": 25225, + "sha256": "d9ba709fa5dcefffe3f3abdcf34600ce188224703cfd743e6db8b58ba4816cb7", + "git_blob": "ff3256f0d3ffbfc56b062f9ec0fdbbc7b30e76d5" + }, + { + "path": "research/shared-wire-split-composition/INDEPENDENT-NOTICE.md", + "size": 1238, + "sha256": "cadbc642ca84311d2c7a6cf704c7828cb4cf77e3c784b66e4c6e8a5c28002fb8", + "git_blob": "1bc9b4da2b8398954cd7a49356eb9d397785d0a6" + }, + { + "path": "research/shared-wire-split-composition/INDEPENDENT-REVIEW.md", + "size": 3674, + "sha256": "c24c7ee899c258420e281afe4e6dfcd890adf552b469822a38c13898bcd2a936", + "git_blob": "17c2ba3fde8d6cd442db7447e7868865df2e1849" + }, + { + "path": "research/shared-wire-split-composition/INDEPENDENT-SOURCES.json", + "size": 1921, + "sha256": "dced1457df5230466ba6202fd6d4595bc2b7fb2a65302806bf2720b1837ff350", + "git_blob": "95afd397782ada3dfcf0f4d9fa1fdb76ab6ea617" + }, + { + "path": "research/shared-wire-split-composition/LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "path": "research/shared-wire-split-composition/NATIVE-INPUTS.json", + "size": 1868, + "sha256": "9bb6c1567783661334d6c1d23f715ce5635cbbb513678819ab9e020a34c7e4c0", + "git_blob": "347b2c4df65e55aacf289addc96d6558e8e1eaf2" + }, + { + "path": "research/shared-wire-split-composition/NOTICE", + "size": 893, + "sha256": "da12736e2e824167ff56f2ecb623a5f88f75a270410360890f61dffc33bab249", + "git_blob": "a3687d65a00794277cdaad37558d24008cbc37f5" + }, + { + "path": "research/shared-wire-split-composition/README.md", + "size": 7160, + "sha256": "f8d540c9f505d5856416897c231bcb9186f873f6148b68b9f23fedac70313831", + "git_blob": "b7504b6fb223c50a27afae1838fb7b540fc6d505" + }, + { + "path": "research/shared-wire-split-composition/SOURCES.json", + "size": 584, + "sha256": "c66f8049a4e4bf9890d5f7d9f386de2c4897490f8f5e48edcc69a54b9333d103", + "git_blob": "75ea7c3d55c6496ff53688b4413e3ba7f6947eb8" + }, + { + "path": "research/shared-wire-split-composition/TASK.json", + "size": 8020, + "sha256": "60e22522e87684c068f32c8ec687305f2be934f2800e2f10a55483bff02506a1", + "git_blob": "8cf0755e451dcc397d7589a742b19f651fe29b0c" + }, + { + "path": "research/shared-wire-split-composition/VALIDATION.md", + "size": 2729, + "sha256": "582d71db76db5ac7bcfb2f9a962479d1a76d321c7536f08347f16fe01ec9d52e", + "git_blob": "6f7ebc4ecab2244b29249d4f54d11b65da4388fc" + }, + { + "path": "research/shared-wire-split-composition/VERIFY-INDEPENDENT.json", + "size": 627, + "sha256": "820992b885fffaee53854be2c0200b7d4bf96ec678c305b1eff3e6be1364b3e3", + "git_blob": "4a2fbb342e6fea656746da9b70487b25a282ce57" + }, + { + "path": "research/shared-wire-split-composition/VERIFY.json", + "size": 1249, + "sha256": "f27f759db9707cf5e8e4a331ca509401186c994ed661a9f4b480961642d5544f", + "git_blob": "9ec717f2201570493089eeb1089f5ea519abac54" + }, + { + "path": "research/shared-wire-split-composition/build_wire.py", + "size": 2825, + "sha256": "b0e1f38dd70f7c1a6f4d9ec8289c76747f558dc8e1ba44b22dd58ff82870e6bd", + "git_blob": "16703507fc62c664404a76b0a29843130ae2693a" + }, + { + "path": "research/shared-wire-split-composition/chart_delta.json", + "size": 65507, + "sha256": "881bc1bb93e1738aa9269f41af6db0ef80b377920aed6f91e79b9b6ed70e5deb", + "git_blob": "8717f47cc832fb4aaf53c262fd82dbb99c5860b1" + }, + { + "path": "research/shared-wire-split-composition/chart_delta.py", + "size": 2095, + "sha256": "865f1e526663cb6e53092db66b5fdabae5ed37a0afe7520bdbe1bb21d0266d38", + "git_blob": "47940a2319982559ca554efbdc320ad1f88622a8" + }, + { + "path": "research/shared-wire-split-composition/compose.py", + "size": 3577, + "sha256": "f057d659243575529cfd89a5534c8f333d0716897ee495bfe3de67eeb0970c20", + "git_blob": "681a55d6d7c22fec3b0ab382b8fa508f57bc3ee4" + }, + { + "path": "research/shared-wire-split-composition/data/bit-admission.json", + "size": 313909, + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8" + }, + { + "path": "research/shared-wire-split-composition/data/caller.json", + "size": 73501, + "sha256": "3828d53e80ea97e8b866320f081af20b6b93bfebd58b95b56b85a7afe151af5e", + "git_blob": "cf55f4271009a06ad192a070d330a4466b6d44fa" + }, + { + "path": "research/shared-wire-split-composition/data/extra_wire_spec.json", + "size": 1020, + "sha256": "b065bd6c3b0762bc90f5cd0a0c1fb6b9664edefc5a1becbff6734a72ab7698d8", + "git_blob": "e02c3da30e05f10d194f0fc8882ffe5dcef6e05b" + }, + { + "path": "research/shared-wire-split-composition/data/final.json.gz", + "size": 350722, + "sha256": "2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883", + "git_blob": "74563a7867d9d762b6588f65362369668841bb3e" + }, + { + "path": "research/shared-wire-split-composition/data/main_6936.json.gz", + "size": 349022, + "sha256": "273e81f176f001684b1fa3eb857992bf58b54748004fcfe806b83adb48d2cc00", + "git_blob": "d93e67ca7628bf5531ae6e369da4dd7b7907b88f" + }, + { + "path": "research/shared-wire-split-composition/data/split759.proof.json", + "size": 745, + "sha256": "35f8b64110957b6f51fd8dd0e53326c466e2ffeecf9254012f0e55a5275bea81", + "git_blob": "16fa0581235ecbc6657aeb5be4f4509319d2e6c5" + }, + { + "path": "research/shared-wire-split-composition/data/split759_450.proof.json", + "size": 1599, + "sha256": "78b25749911131b50bb4565b17a06d08ccf4b511ec05e598e7f146c96aed4174", + "git_blob": "2fb9b2e8b1b8915ff7e81d03057eeeba351139f2" + }, + { + "path": "research/shared-wire-split-composition/data/wh_6937.json.gz", + "size": 357887, + "sha256": "25326dac562fa07edd28a6daf302de0c27f5f2e82f610eaf3671d39575f8dbea", + "git_blob": "1481c9478010f12a656e99a1a43aa186fb326262" + }, + { + "path": "research/shared-wire-split-composition/frozen/clifford_exact.py", + "size": 6824, + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2" + }, + { + "path": "research/shared-wire-split-composition/frozen/native_verify.py", + "size": 12323, + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c" + }, + { + "path": "research/shared-wire-split-composition/frozen/physical.py", + "size": 7527, + "sha256": "4e995d1158033d83bf69b671f23dc7924d66edbbe07623ba063ba7421234ea20", + "git_blob": "5e0b17b9ef2151e3dee68378b71b3d0d47a56233" + }, + { + "path": "research/shared-wire-split-composition/frozen/verify_host3_odd.py", + "size": 4861, + "sha256": "e75ad2096ba2587d1dc9c8982b2c2eb7c6fd2636a80adcd943314ef2cf6fd258", + "git_blob": "2117502bedfc9fc0a7abade8243eb5a43d0b514e" + }, + { + "path": "research/shared-wire-split-composition/full_verify.py", + "size": 5478, + "sha256": "08134736288c3a1067d61185f195c645aa2624051b45c808b2447360d2d20ae0", + "git_blob": "e71fd90fcf14c172ae52ac423f485f3871e98653" + }, + { + "path": "research/shared-wire-split-composition/independent.py", + "size": 11970, + "sha256": "21f46a8340331abb1486b50bd4e04453f1968b0a5950d86ff7780dd368590874", + "git_blob": "1ae1d7c680ad86c0fa999f2e8f0c09e966fc07a0" + }, + { + "path": "research/shared-wire-split-composition/independent_construction.py", + "size": 7967, + "sha256": "1e8d66885afce4181ff6195c31aa3445886410b13faf1c8c7321f3ae7fc9554e", + "git_blob": "4c7025059dc1870c4360e8560e24cc3d7025f745" + }, + { + "path": "research/shared-wire-split-composition/interval_gate.py", + "size": 6886, + "sha256": "60a743d13f668ef86db4b8215b4d5d04430a671ba6f1fe06d9c1c4c3dfe86da5", + "git_blob": "e24dc46079b4c25152f5afc096dda2ce8ee58ff5" + }, + { + "path": "research/shared-wire-split-composition/native-accounting.json", + "size": 3740, + "sha256": "ec4f2657a6c172a16c68e958e865ef7bf5217a47814fb506e6e144d19daeaebc", + "git_blob": "a0941d3112499f028e4d9eada50dfb5820989db7" + }, + { + "path": "research/shared-wire-split-composition/precision_replay.py", + "size": 2676, + "sha256": "850d9098c5946ab27ef5228acc54d59df2196e72259d3e21588ec0c319c8f5ee", + "git_blob": "fafa1611dded2746f021714aad6837aed61041cb" + }, + { + "path": "research/shared-wire-split-composition/reproduce.py", + "size": 1765, + "sha256": "9b9fca18bf28c627ff29ba06048503af0cb5f27a4ffabeadffed50e0678c96c9", + "git_blob": "6f143887c1db760fba631cb77507522424e9a494" + }, + { + "path": "research/shared-wire-split-composition/retained/odd-native-common-grid/independent_bounds.py", + "size": 11449, + "sha256": "198521def614fe78fa728f1dde2b7fb820c0c0e0ac3ad0c9224dccbf51eac0d5", + "git_blob": "8fe729386f81e6973bbe7ecaa5dbb4bf86281908" + }, + { + "path": "research/shared-wire-split-composition/retained/query-only-precision-envelope/envelopes.py", + "size": 14441, + "sha256": "783da6b5b450fc07434946cb9ec86070dfee01df6b5fa1c385cb024def2c9a9f", + "git_blob": "70c8ca23763e30c924fb726b74b82f44d344c65f" + }, + { + "path": "research/shared-wire-split-composition/retained/query-only-precision-envelope/source_binding.py", + "size": 2424, + "sha256": "624c459311c58f3847b7713b818bfd340153abf42919f02ac9aa8892ed52a2bd", + "git_blob": "9f0e0a8cbaf48266cf9c6aa8b263505e9569390c" + }, + { + "path": "research/shared-wire-split-composition/split_build.py", + "size": 3918, + "sha256": "54f80d3c557175acfc2cf13059f00f004be3f18fb6c76946e05efe8ca8b5f33a", + "git_blob": "5ac9b60a6f9551cde4f59835fab7ed46a2403cc4" + }, + { + "path": "research/shared-wire-split-composition/verify.py", + "size": 542, + "sha256": "d2a291f8f4ea6dce51648ba44614d655b47e8e38d235458ac64924af7552b57b", + "git_blob": "022f5841a0355c5f5fdb2505c770b3d2411a1db7" + }, + { + "path": "research/shared-wire-stop-fusion/DEPENDENCIES.json", + "size": 4834, + "sha256": "29cfec445fff86d96daec032c0ee6f9a06d4f6025f2c1e7e70aca64b44c49c36", + "git_blob": "4ae6821773bb4a28113e8495b44f152e419a997b" + }, + { + "path": "research/shared-wire-stop-fusion/EDITS.json", + "size": 3432, + "sha256": "4da478b0201bfc0e7938469d91b7aafc6c4760c94e370ee8af3d8662d214cbb2", + "git_blob": "cbd31fd0840ce40bba74033c097353c51cb312ad" + }, + { + "path": "research/shared-wire-stop-fusion/LICENSE", + "size": 11357, + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + { + "path": "research/shared-wire-stop-fusion/NOTICE", + "size": 240, + "sha256": "c2f941730e39b08d2d77d628706731beccd0bb2519a66bc7275d280e7f27af5d", + "git_blob": "2ed927f94056318486974f34bf03785eb511f247" + }, + { + "path": "research/shared-wire-stop-fusion/PROOF.md", + "size": 3971, + "sha256": "03646d857a93250d94a9c2115917638774f110243d1def42ea940fb86be55829", + "git_blob": "f7441e2651b22ab8718094ed2e9f5d3808e29469" + }, + { + "path": "research/shared-wire-stop-fusion/README.md", + "size": 4068, + "sha256": "cd38248f772dd446a0bf54f0d80740a3bfc37f4ee08410b3446a791a9517ddde", + "git_blob": "1ba57075e4fbb504b834fb0cb2b80a1568865d2c" + }, + { + "path": "research/shared-wire-stop-fusion/RESULT.json", + "size": 29976, + "sha256": "98ff3277ca65dba06337363dcd80ae5d305bb580979d8ccedc1454b4fc987298", + "git_blob": "d6467b91de2865d0584030e39b13050de3ecb1de" + }, + { + "path": "research/shared-wire-stop-fusion/SOURCES.json", + "size": 5574, + "sha256": "8e38cc32e587a762b004317e8b3275e5eb93cafa43b3feac2d435fa27f6f9024", + "git_blob": "d924e61f797dd0e9ccef3af9d81d9b32a6e9c991" + }, + { + "path": "research/shared-wire-stop-fusion/TASK.json", + "size": 7480, + "sha256": "c1ab13f9d279a668371f9c43170df424bbb71feb8f2dbd6bd13ee1f7afdbbb61", + "git_blob": "ecdf6742b16446efac358aa8c3861f42ae62cfb5" + }, + { + "path": "research/shared-wire-stop-fusion/VALIDATION.md", + "size": 2414, + "sha256": "d5154e036f3346b87ad3b1537259a9472c72d3e9e714d0e5f96de113e59dc316", + "git_blob": "a80afde380241ff11ff486e78e8f75b50a30d049" + }, + { + "path": "research/shared-wire-stop-fusion/VERIFY.json", + "size": 2281, + "sha256": "6c2589e6a80563e622eab7b0b080ff2f917da39501b9e679b64048b25de0d38c", + "git_blob": "b594999d0ee8022967c0264528e1795c8a5cb86d" + }, + { + "path": "research/shared-wire-stop-fusion/audit_native.py", + "size": 10156, + "sha256": "c7d81ad6620de5e46abf97259f62da0138b58a02759c3189e57b8ab176db6bd5", + "git_blob": "a2a06f319dc0e0faa88808a2df282ca543e468ec" + }, + { + "path": "research/shared-wire-stop-fusion/audit_price.py", + "size": 4197, + "sha256": "585295aa55846e594c705941002c36ea0b9b6cbfe3a49e6594e1d2e70751b704", + "git_blob": "f05fb5522dbb0c2c856a0af41f63228df2d2737d" + }, + { + "path": "research/shared-wire-stop-fusion/build_candidate.py", + "size": 7032, + "sha256": "a124347129fe86db5947dca4830dabe93e79bdaa16cecfba1b41d555dd048011", + "git_blob": "873acbab4a3f8cd3ada031dea8dd5f83c1815274" + }, + { + "path": "research/shared-wire-stop-fusion/slide_stops.py", + "size": 7724, + "sha256": "64a69bcd5689e17a081187a17ef2913adece970da653afa606b47cf130f1aa04", + "git_blob": "16ac095ea503fe3c98e2d7118e512339b6d77ae7" + }, + { + "path": "research/shared-wire-stop-fusion/verify.py", + "size": 10945, + "sha256": "64c98e5a919fd1bff519a305d3e8df45a7e95ec73a7dd04072d61c95ea5516b2", + "git_blob": "0f7942e6b8501e8fda783807df4aa01310839e10" + } + ] +} diff --git a/research/p104-causal-retimed-step/LICENSE b/research/p104-causal-retimed-step/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-causal-retimed-step/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/p104-causal-retimed-step/NOTICE b/research/p104-causal-retimed-step/NOTICE new file mode 100644 index 0000000000..b2fe2f69be --- /dev/null +++ b/research/p104-causal-retimed-step/NOTICE @@ -0,0 +1,3 @@ +Prepared for dillona with substantial OpenAI Codex assistance. Apache-2.0. + +The helper split and basis constructor retain Ali Romman's authorship and CubeJerry's counted-inventory adaptation. The source archive preserves ToikY's #7003/#7004, CubeJerry's #7000/#7001 and DreamingOfClouds' native construction, with all original notices. Cinna Davis, Pierre-Loic Doulcet, Mason Hale, Jacob Alan Sussman, zxv, thu-nmrc and the retained native, compiler, precision and analytic authors keep their original attribution. New work is the exact role1123 retiming/split composition and its source-bound verification/packaging; no original predecessor mechanism or independent human review is claimed. diff --git a/research/p104-causal-retimed-step/README.md b/research/p104-causal-retimed-step/README.md new file mode 100644 index 0000000000..dcec946860 --- /dev/null +++ b/research/p104-causal-retimed-step/README.md @@ -0,0 +1,70 @@ +# Conditional κ = 0.00363216151: retime and split helper 1123 + +This construction changes the complete invoice of [#7004](https://github.com/CrocSwap/integer-mult-bounds/pull/7004), raising its conditional claim from **0.00363206219** to **0.00363216151**, a gain of **0.00000009932**. It retimes one paid helper transition and splits the resulting independent rank-nine helper into ranks eight and one. The caller and BIT source stay byte-for-byte those of #7004. This is an author-checked conditional construction, not supplier admission or a new unconditional multiplication theorem. The selected frontier is unchanged. + +## Exact edit and arbitrary-input argument + +The scientific baseline is ToikY's #7004 at `2ee11a4460f23abf06d16b12f18c8ef9aca889f1`, canonical word SHA256 `311069e5faeef999a0b3f2fd8ae9c256b67b40a368998c5c31cd38a500f385e3`. All indices are zero-based. Canonical main was refreshed at `17469fff78c22941280f04d39dc5a1faee09c840`, priority revision 8. + +Helper 1123 has no scalar contact between the source indices 37910 and 56194; its only event there is `MOVE(1123,242,127,false)` at 44017. The spaces at frames 242, 245 and 127 strictly nest, with dimensions 4, 8 and 9. Replace this MOVE by 242→245→127 at cut 43057, immediately before source event 43057. This replaces one rank-five payment by ranks four and one. Frame transports preserve normalized scalar coordinates, and there are no intervening contacts with helper 1123, so this retiming preserves the entire normalized map. + +At this cut the exact prefix row of role 1123 is the independent input `x1123`. The exact suffix sends the cut direction `e1123 + e843` to final direction `e1123`, with no other public or owned output. Roles 1123 and 843 are both physically at frame 245 after the retiming. These are complete rational row/column equalities, not sampled tests. + +Insert `ADD(843,1123,-1,245)` followed by `ADD(843,1480,+1,245)`. The new independent public helper 1480 starts at frame 245. Relabel every later use of1123 as1480. Helper 1123 now stops at245, and 1480 finishes at127. Replacing the old cut coordinate by the fresh input changes the suffix input by `(x1480−x1123)(e1123+e843)`, hence changes only the renamed successor output by `x1480−x1123`. All other outputs are unchanged, helper 1123 returns its old input, and 1480 returns its own arbitrary input. No boundary basis change is needed. The exact generic split checker also verifies both unit pairings and the nested productive targets. + +`construct.py` uses Ali Romman's split constructor as adapted by CubeJerry, with the pivot chosen to be the retimed helper itself. `split.py` preserves predecessor attribution and additionally excludes the second main plane from the helper group. Owned labels shift by one to accommodate the new public helper; their logical lifetimes, ascent inventory and peak remain fixed. + +## Complete accounting and evidence + +Per LOCAL the paid delta is `{1:+1,4:+1,5:−1}` and the target delta is `{1:+1,8:+1,9:−1}`. Across the unchanged eighteen LOCALs these counts multiply by eighteen. Rank surplus stays 1520 and no empty-root target is credited. For `p=1−κ`, the net margin gain is + +``` +18 (8^p + 5^p − 9^p − 4^p) > 0, 0 < p < 1. +``` + +Strict concavity proves the inequality: the increment from4 to5 exceeds that from8 to9. The rank-one target and payment cancel; neither is omitted. This is a new complete paid/target profile, rather than more digits of the predecessor root. + +The emitted word has71,258 events and1,481 public fields:400 main fields and1,081 independent helpers. It adds exactly one MOVE and two ADDs. The source caller remains3,095 events with76 roles. Owned labels51, lifetimes54, peak43, rises23 and rise mass56 remain fixed. The conservative ordinary bill is826,738,944 < 10^9. The second rational engine certifies the raw crossing in `(0.00363216151546863865247146187645487, 0.00363216151546863865247146187645488)`. The primary separately certifies a containing bracket. The claim leaves about5.47e-12 fixed-invoice headroom; extra decimal digits of this root are not a construction gain. Tested price is0.00363216151007, compiler gap10^-14 and written logarithm power2229. Full counts, the exact compiler threshold and all margins are in `RESULT.json`. The raw fixed-invoice ceiling is certified by two rational interval engines and a negative derivative bound; this changed hosted/owned-ascent model is outside the historical nine-local-word packing-cap model. + +The checker authenticates all source members by size, SHA256 and Git blob; rebuilds #7004 and the candidate; checks the exact cut prefix/suffix; runs an exact all-input adjoint and a separate integer-grid forward replay; checks every introduced chart pair and four named boundary pairs, including absolute phase and every one of512 columns; replays the unchanged formal caller; reconstructs both complete invoices; checks the ordinary tariff, E-free paired BIT binding, common grid and source precision envelopes, strictification, compiler and 54+4 outer predicates; and runs the full width 512 physical control. Mutations of the cut direction, contact window, corrections and successor frame reject. The source invoice rejects the new claim. + +The two interval and endpoint implementations are distinct, but their reuse here is source-aware attribution, **not independent human or proof-kernel review**. Finite physical replay is finite evidence. No baseline all-history, Lean or Docker suites were run. + +## Reproduce + +The scientific verifier is standalone and needs only Python and the committed package; it extracts authenticated source code into temporary storage and does not need Git or network. + +```sh +python3 -I -B research/p104-causal-retimed-step/verify.py +python3.12 -B scripts/research_package.py --package research/p104-causal-retimed-step +``` + +The generic registered command targets Python 3.12. Local evidence records the interpreter actually used; a registered 3.12 execution must not be inferred from a direct3.14 replay. Optimized mode is deliberately rejected because retained source engines use assertions. `--out UNUSED_PATH` emits a new receipt; ordinary replay compares every retained result field. Gzip equality compares the complete decompressed JSON bytes. + +To reproduce the optional finite discovery screen: + +```sh +python3 research/p104-causal-retimed-step/source.py --output /tmp/base7004.json.gz +python3 research/p104-causal-retimed-step/discover.py /tmp/base7004.json.gz /tmp/screen7004.json +``` + +`SCREEN-HITS.json` and `SCREEN-LOG.txt` retain three nominations, all using the same paid carrier; they are not three independent gains. The certificate uses one nomination with pivot1123 to remove unnecessary basis swaps. The earlier #6931 screen is retained as exploratory round-one evidence, not the baseline of the new claim. + +## Scope and remaining obligations + +All five framework assumptions remain: `native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`, `analytic_recovery`. Also retain #7004's exact odd-scalar child returns, owned ascent, hosted/per-port and one-field-idle caller, LAMBDA/ordinary tariff and paired BIT contracts. The new edit itself adds only integer ADDs and no owned rise. Full fixed-tape/rounded provider admission and the #6998 physical-tariff bridge remain open. The large uniform word and rounded multiplier are not materialized. + +The base source archive includes the exact #7004/#7003/#7000 files and all their notices; `INPUTS.json` binds every member to its original Git blob. `SOURCES.json` separately records current-main task and selected-record provenance. Existing frozen packages and the selected record are unchanged. + +## Credit + +New source-bound paid-retiming/split composition, simplified pivot, packaging and checks: prepared for dillona with substantial OpenAI Codex assistance; no subagents. Apache-2.0. + +Ali Romman supplied independent-helper split and basis methods (#5599); Jerry Chen/CubeJerry supplied paid retiming (#6805/#6916), shared wires, the #7000 composition and paired QUERY-only BIT source; DreamingOfClouds supplied #6931/#6936/#6937 and the native-word chain; ToikY supplied #7003 five fusions and #7004 peer retiming. Retain the original notices and credit to Pierre-Loic Doulcet, Cinna Davis, Mason Hale, Jacob Alan Sussman, zxv, thu-nmrc and all other native/compiler/precision/analytic predecessors named there. No predecessor mechanism is claimed as newly invented. + +## Open next questions + +- Can the other two screened cuts compose without paying this carrier repeatedly? First construct a joint exact prefix/suffix certificate and full invoice. They share role 1123, so independent gains cannot be assumed. +- Can the actual rounded providers be admitted under one physical tariff? Continue #6998 with this exact word; the inherited provider and framework obligations remain open. + +Structured questions and blockers are in `TASK.json`. Live overlap covered398 open and6,175 closed/merged PR bodies plus7,013 Discussion records. This coverage is not a novelty certificate. The canonical claim and final artifact link are maintained on [the handoff board](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19519779). diff --git a/research/p104-causal-retimed-step/REPLAY.txt b/research/p104-causal-retimed-step/REPLAY.txt new file mode 100644 index 0000000000..07384c7ce5 --- /dev/null +++ b/research/p104-causal-retimed-step/REPLAY.txt @@ -0,0 +1,19 @@ +PASS source reconstruction, exact split prefix/suffix, complete adjoint and frame law +caller 0 terms 77 +caller 500 terms 1044 +caller 1000 terms 761 +caller 1500 terms 1868 +caller 2000 terms 2524 +caller 2500 terms 384 +caller 3000 terms 151 +PASS complete invoice, ordinary bill, BIT binding, two exact price engines, compiler and 54+4 outer gates +events 71258 public 1481 owned roles 51 paid {1: 4068, 2: 830, 3: 811, 4: 238, 5: 323, 6: 17, 7: 12, 8: 6} owned UP {1: 10, 2: 4, 3: 1, 4: 6, 5: 1, 6: 1} helpers {1: 14, 2: 18, 3: 44, 4: 215, 5: 68, 6: 42, 7: 18, 8: 68, 9: 594} +endpoint bad rows 0 odd certificate S 1125 +PASS_HOST3 decoupled ports 96 hosted ports 8 +gate interpreter agrees with the library on 4 exact state vectors +replayed 71258 events, 2968 chart pairs, 23s +prime 1000000009 seed 11: helper rows bad 0 (of 1081), X rows bad 0, Y rows bad 0, X2 rows bad 0, Y2 rows bad 0 (of 104 ports; 96 with second mains) +tableau on 104 ports: XX!=D 0 YY!=D 0 YX!=Q^-1D 0 XY!=QD 0 | controls matching (must be 0): 0 0 +PASS_PHYSICAL 31s +PASS exact Gaussian columns, prefix precision and physical finite replay +PASS_P104_RETIMED_HELPER_STEP 363216151/100000000000 diff --git a/research/p104-causal-retimed-step/RESULT.json b/research/p104-causal-retimed-step/RESULT.json new file mode 100644 index 0000000000..a1ba81ab2d --- /dev/null +++ b/research/p104-causal-retimed-step/RESULT.json @@ -0,0 +1,685 @@ +{ + "caller": { + "bad_outputs": [], + "caller_denominator_height_bound": 163, + "caller_mass_bound": "16246698892210214036146399419475929893435/256", + "caller_mass_ceiling_bits": 126, + "max_terms": 2713 + }, + "charts": { + "new_pairs": [], + "rechecked_pairs": [ + { + "columns": 512, + "pair": [ + 3, + 127 + ], + "rank": 9 + }, + { + "columns": 512, + "pair": [ + 3, + 245 + ], + "rank": 8 + }, + { + "columns": 512, + "pair": [ + 242, + 245 + ], + "rank": 4 + }, + { + "columns": 512, + "pair": [ + 245, + 127 + ], + "rank": 1 + } + ], + "wrong_phase_rejected": true + }, + "controls": { + "intervening_contact": true, + "missing_cut_correction": true, + "missing_successor_correction": true, + "wrong_successor_frame": true, + "wrong_suffix": true + }, + "diagnostic_crossing": "0.00363216151546863865247146187645487883791756114780064932979940593460", + "forward": { + "coefficient_positions": 2347024, + "fractional_bits": 24, + "grid": 1125, + "rows": 1532 + }, + "gain": { + "claim_gain": "2483/25000000000", + "claim_vs_old_raw_upper": "155178479630868527251831/1562500000000000000000000000000", + "new_margin_at_old_upper": [ + "128911501346101330353504937703846068701716076797157180912414757713560202179233/3125000000000000000000000000000000000000000000000000000000000000000000000000000", + "2062584021537621285656079003261537099227457228754514894598636123416963255925911/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "raw_gain_interval": [ + "9931969560240832890304829/100000000000000000000000000000000", + "9931969560240832890304831/100000000000000000000000000000000" + ] + }, + "gate": { + "BIT_margin": "13452848993/100000000000000", + "BIT_pin": "376669/100000000", + "H": "14181100000000000000", + "alpha": [ + 0.9999999999929418, + 0.9999999999929418 + ], + "claim": "363216151/100000000000", + "compiler_gap": "1/100000000000000", + "delta": [ + 0.8766117957561398, + 0.8766117957561398 + ], + "derivative_upper": -408369.1406327504, + "gamma": [ + 0.9497767721663171, + 0.9497767721663171 + ], + "input_lift": { + "derivative_upper_on_required_interval": "-2299831290525933154178526076272396899996972093654613095735772838275432653960006518819/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "interval_kappa_cap": "376669/100000000", + "margins": { + "363216151/100000000000": [ + "123940354011462409047328172773492783463310970803374991522724449982508324772549/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "123940354011462409047328172773492783463310970803374991522724449982508324774483/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "363216151007/100000000000000": [ + "123940354013749480098937581821883419883567079785065036754052255835288640303623/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "123940354013749480098937581821883419883567079785065036754052255835288640305571/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "source_BIT_wide_crude_bound_would_be": "-2299831290525933154178526076272396899996972093654613095735772838275432653960006518819/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + }, + "minimum_log_power": 2228, + "moment_margin_float": { + "181608075773431932623573093823/50000000000000000000000000000000": [ + -2.1270352965627786e-27, + -2.1270352965627786e-27 + ], + "363216151007/100000000000000": [ + 2.24228305655477e-06, + 2.24228305655477e-06 + ], + "72643230309372773049429237529/20000000000000000000000000000000": [ + 2.026387817805486e-27, + 2.026387817805486e-27 + ] + }, + "moment_margins": { + "181608075773431932623573093823/50000000000000000000000000000000": [ + "-106351764828138928485644202505269480848829953308749161/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "-10635176482813892848564420250526948084882995328777187/5000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "363216151007/100000000000000": [ + "22422830565547698070683742903128310817596484619113951518045932334956417897/10000000000000000000000000000000000000000000000000000000000000000000000000000000", + "112114152827738490353418714515641554087982423095569757590229661674802933269/50000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "72643230309372773049429237529/20000000000000000000000000000000": [ + "101319390890274304722102620381234768647664247131931423/50000000000000000000000000000000000000000000000000000000000000000000000000000000", + "20263878178054860944420524076246953729532849430594649/10000000000000000000000000000000000000000000000000000000000000000000000000000000" + ] + }, + "outer": { + "BIT_just_below_effective_rejected": true, + "functional_count": 4, + "minimum_margin": "1/1000000000000000", + "strict_count": 54 + }, + "raw_bracket": [ + "72643230309372773049429237529/20000000000000000000000000000000", + "181608075773431932623573093823/50000000000000000000000000000000" + ], + "tested": "363216151007/100000000000000", + "written_log_power": 2229 + }, + "grid": { + "dyadic_height": 24, + "maximum_scaled_mass": "1636346757402225/16384", + "odd_divisions": { + "ADD": 4079, + "SCALE": 64 + }, + "odd_grid_lcm": 1125, + "opcodes": { + "ADD": 61182, + "CLEAR": 54, + "COPY": 1, + "INIT": 54, + "MOVE": 6305, + "SCALE": 3662 + }, + "owned_lifetimes": 54, + "owned_peak": 43, + "owned_rise_mass": 56, + "owned_rises": { + "1": 10, + "2": 4, + "3": 1, + "4": 6, + "5": 1, + "6": 1 + }, + "paid": { + "1": 4068, + "2": 830, + "3": 811, + "4": 238, + "5": 323, + "6": 17, + "7": 12, + "8": 6 + } + }, + "independent_raw_bracket": [ + "363216151546863865247146187645487/100000000000000000000000000000000000", + "22701009471678991577946636727843/6250000000000000000000000000000000" + ], + "invoice": { + "P": { + "1": 73640, + "16": 416, + "2": 14940, + "24": 416, + "3": 14598, + "32": 416, + "4": 4284, + "40": 416, + "48": 416, + "5": 5814, + "56": 416, + "6": 306, + "64": 416, + "7": 216, + "8": 812 + }, + "S": 1520, + "T": { + "1": 252, + "145": 208, + "17": 416, + "2": 324, + "25": 416, + "3": 792, + "33": 416, + "4": 3870, + "41": 416, + "49": 416, + "5": 1224, + "57": 416, + "6": 756, + "65": 416, + "7": 324, + "73": 416, + "8": 1224, + "9": 11108 + }, + "empty_root_credits": 0, + "no_E_credit_crossing": "0.0036321615154686386524714618764548788379175611621391009317566121035", + "raw_crossing": "0.0036321615154686386524714618764548788379175611621391009317566121035" + }, + "limitations": [ + "Source-aware attributed engine reuse, not independent human or kernel review.", + "All inherited five assumptions and #7004 additional exact odd-return, owned-ascent, caller, BIT and physical-tariff contracts remain.", + "No materialized uniform rounded multiplier or selected-frontier change." + ], + "native": { + "bad_inputs": [], + "events": 71258, + "helpers": { + "1": 14, + "2": 18, + "3": 44, + "4": 215, + "5": 68, + "6": 42, + "7": 18, + "8": 68, + "9": 594 + }, + "lifetimes": 54, + "owned_peak": 43, + "paid": { + "1": 4068, + "2": 830, + "3": 811, + "4": 238, + "5": 323, + "6": 17, + "7": 12, + "8": 6 + }, + "public": 1481, + "rises": { + "1": 10, + "2": 4, + "3": 1, + "4": 6, + "5": 1, + "6": 1 + } + }, + "ordinary": { + "caller_items": { + "A": { + "envelope": 124674048, + "field_boundary": 94848, + "idle_routes": 185472000, + "output_routes": 229056000, + "query_routes": 1152000, + "thin": 6144 + }, + "B": { + "envelope": 19893760, + "field_boundary": 7904, + "idle_routes": 20064000, + "output_routes": 19088000, + "query_routes": 96000, + "thin": 512 + } + }, + "caller_total": 599605216, + "conservative_total": 826738944, + "init_clear_allowance": 216, + "lambda_paid_rank1_would_reduce_S_by": 14480, + "lambda_second_charge": 14480000, + "margin_to_billion": 173261056, + "odd_divisions": { + "ADD": 4079, + "SCALE": 64 + }, + "per_input_conversion": 2772432, + "raw_upper": 809486512, + "route_items": { + "first_main_adapter": 416, + "first_main_boundary": 208, + "helper_boundary": 2162, + "moves": 6305, + "owned_lifetime": 216, + "second_main_adapter": 384, + "second_main_boundary": 192 + }, + "routing": 9883000, + "scalar_upper": 1777072 + }, + "physical_checks": [ + "verify_host3_odd.py", + "physical.py" + ], + "precision": { + "common_grid": { + "caller": { + "denominator_height": 163, + "maximum_mass": "16246698892210214036146399419475929893435/256", + "pre_joint_height": 154, + "pre_joint_mass": "758143798823020519902612486795530419693/64" + }, + "context_c": 356, + "context_height": 178, + "context_mass_bits": 161, + "word": { + "coefficient_visits": 14087599, + "dyadic_height": 24, + "mass_witness": [ + 63462, + "stored add" + ], + "maximum_scaled_mass": "1636346757402225/16384", + "numerator_bits": 24, + "odd_scale_lcm": 1125 + } + }, + "helper_census_substitutions": [ + [ + "word[\"public\"] - len(mains) == 1061", + "word[\"public\"] - len(mains) == 1081" + ], + [ + "fresh_arbitrary_helpers=18 * 1061", + "fresh_arbitrary_helpers=18 * 1081" + ] + ], + "method": "attributed source-engine reuse", + "negative_grid_controls": { + "S1125_f23": "integer grid rejection at event 61563: denominator 64", + "S225_f24": "integer grid rejection at event 1118: denominator 250", + "S375_f24": "integer grid rejection at event 36836: denominator 48" + }, + "rounded_envelope": { + "caller": { + "bounds": { + "E_joint_entrance": { + "exact": "326155049787256155157832340134847384764735276402770643581716325768728878950947843136976592484023494309280943080837466608094361777686262992724431/272008309413291564308889600000000000000000", + "strict_power_of_two": 340, + "witness": { + "cut": 2958, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": 39 + } + }, + "Gamma_context": { + "exact": "15259614246461931659309736794620779902271844611676764249617727159004313420763133791821646997906736780301475877948165376397954674876208172804609281/78338393111027970520960204800000000000000000", + "strict_power_of_two": 337, + "witness": { + "cut": 3095, + "factor": "1", + "kind": "public-return", + "register": 75 + } + }, + "M_caller": { + "exact": "1683307283016999532839217702665847040", + "strict_power_of_two": 121, + "witness": { + "cut": 3050, + "event": 3049, + "factor": "1", + "kind": "stored", + "register": 38 + } + }, + "M_context": { + "exact": "41102872446205142735437430546015485583317579504067280376414699764384004216484558713313700184037785492405232261959967253420952372895326637533644385181/816024928239874692926668800000000000000000", + "strict_power_of_two": 355, + "witness": { + "cut": 2959, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": null + } + }, + "M_joint_entrance": { + "exact": "363421601940370671219209686545270656", + "strict_power_of_two": 119, + "witness": { + "cut": 2958, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": 39 + } + }, + "Sigma_caller": { + "exact": "8157752610051527181179756772539507154773732211062280276520908864921502503903079232267543142300963208377043381922666561628163303615708477177007431/1468844870831774447268003840000000000000000", + "strict_power_of_two": 342, + "witness": { + "cut": 3050, + "event": 3049, + "factor": "1", + "kind": "stored", + "register": 38 + } + }, + "Sigma_context": { + "exact": "4721668704341998520596051155693512848854283472358493166554227780252302280372962450092195935022594418370312782024308506417981800625991445906866329439027040661265159185978631113089391200231778900135287524480718081027894584990957588722419044055641932024450294493/28411591829712752729879633148004541902111328635453440000000000000000000000000000000000", + "strict_power_of_two": 576, + "witness": { + "cut": 2959, + "event": 2958, + "factor": "1", + "kind": "stored", + "register": null + } + } + }, + "fresh_arbitrary_helpers": 19458, + "helper_allocation_premise": "distinct (stage, helper) public inputs as in frozen caller proof", + "independent_adjoint": { + "E_joint_entrance": { + "entrance_mass": "363421601940370671219209686545270656", + "joint_coefficient": "59336854494143543914675236360327/2", + "primitive_coefficient": "22622085086540611235550148326673690", + "residual_mass": "326155049787256155157832340134847384764735276402770643581716325768728878950947843136976592484023494309280943080837466608094361777686262992724431/272008309413291564308889600000000000000000" + }, + "Gamma_context": { + "entrance_mass": "59038824075417799032780136585499589", + "joint_coefficient": "308461849925427171118076353794753/64", + "primitive_coefficient": "117600608836679351835159084859338679/32", + "residual_mass": "15259614246461931659309736794620779902271844611676764249617727159004313420763133791821646997906736780301475877948165376397954674876208172804609281/78338393111027970520960204800000000000000000" + }, + "M_caller": { + "entrance_mass": "1683307283016999532839217702665847040", + "joint_coefficient": "274838256141142176415070287809505/2", + "primitive_coefficient": "104781665096099932454228246133920343", + "residual_mass": "8157752610051527181179756772539507154773732211062280276520908864921502503903079232267543142300963208377043381922666561628163303615708477177007431/1468844870831774447268003840000000000000000" + }, + "M_joint_entrance": { + "entrance_mass": "363421601940370671219209686545270656", + "joint_coefficient": "59336854494143543914675236360327/2", + "primitive_coefficient": "22622085086540611235550148326673690", + "residual_mass": "326155049787256155157832340134847384764735276402770643581716325768728878950947843136976592484023494309280943080837466608094361777686262992724431/272008309413291564308889600000000000000000" + }, + "Sigma_caller": { + "entrance_mass": "1683307283016999532839217702665847040", + "joint_coefficient": "274838256141142176415070287809505/2", + "primitive_coefficient": "104781665096099932454228246133920343", + "residual_mass": "8157752610051527181179756772539507154773732211062280276520908864921502503903079232267543142300963208377043381922666561628163303615708477177007431/1468844870831774447268003840000000000000000" + } + }, + "joint_entries": [ + { + "entrance_defect": "1", + "entrance_mass": "3328", + "event": 21, + "stage": 1 + }, + { + "entrance_defect": "148410063514995949252033673132766658208788044686637910905148510954763664307089800586773642570352084559802399438531/1468844870831774447268003840000000000000000", + "entrance_mass": "34560", + "event": 66, + "stage": 2 + }, + { + "entrance_defect": "6381632731144825817837447944708966302977885921525430168921385971054836629550678705390943720806693556071503175856833/7344224354158872236340019200000000000000000", + "entrance_mass": "267520", + "event": 117, + "stage": 3 + }, + { + "entrance_defect": "48826910896433667303919078460680230550691266701903872687793860104117237131738365301990298876375809580174989415276699/7344224354158872236340019200000000000000000", + "entrance_mass": "2019072", + "event": 168, + "stage": 4 + }, + { + "entrance_defect": "368502187707734941992799610388659612332420714956921932777483752700678113879113090288014086997179354281989357805872473/7344224354158872236340019200000000000000000", + "entrance_mass": "15211776", + "event": 219, + "stage": 5 + }, + { + "entrance_defect": "185067349203199948717285990396560022786358691724237474898720193160590256874632460771771868297672042086073592099848157/489614956943924815756001280000000000000000", + "entrance_mass": "114566912", + "event": 270, + "stage": 6 + }, + { + "entrance_defect": "167258141581400434807041949620628023801304126361840925590102371846018620278332820484324965913788829993297304167224437/58753794833270977890720153600000000000000", + "entrance_mass": "862823680", + "event": 321, + "stage": 7 + }, + { + "entrance_defect": "52485367372141832448930960537076061442196100791474183829516676047663115421152635796147725164134956894098678363835926681/2448074784719624078780006400000000000000000", + "entrance_mass": "6498041600", + "event": 372, + "stage": 8 + }, + { + "entrance_defect": "395274324295395606266221720786098788106678616702078605439396208037340790696936834593205743207902610561905792047787395683/2448074784719624078780006400000000000000000", + "entrance_mass": "48937594112", + "event": 423, + "stage": 9 + }, + { + "entrance_defect": "34770148088268771123885638240582467875882832798105186097975646756192312883635055738114843067268783193395527948401954360792704172352873/3672112177079436118170009600000000000000000", + "entrance_mass": "2869851357661739006410624", + "event": 2166, + "stage": 10 + }, + { + "entrance_defect": "2132061314240615153963022002271372481864552242078141748512146215488581108009961703114733286845760670076951136425489377727664288518017871/7344224354158872236340019200000000000000000", + "entrance_mass": "87987819921824138957327936", + "event": 2299, + "stage": 11 + }, + { + "entrance_defect": "59294726363064922404621789792393824053641347426002118217890063537432213876174398198493395557775819597868637128324929668718040101528150267/7344224354158872236340019200000000000000000", + "entrance_mass": "2447027986812579413618418560", + "event": 2399, + "stage": 12 + }, + { + "entrance_defect": "1370442949490220658284117798109508244525287414980873980398868445818548753467187197511759787995515100799139475942763201402065488274011582831/7344224354158872236340019200000000000000000", + "entrance_mass": "56556669663990103089614108160", + "event": 2497, + "stage": 13 + }, + { + "entrance_defect": "10503316835277737472467818262779767183093496908140860501618685681379718399672322257229321506679835314668301329992249271337971462823973420583/2448074784719624078780006400000000000000000", + "entrance_mass": "1300380918848168161545814930560", + "event": 2593, + "stage": 14 + }, + { + "entrance_defect": "144898222987395514294262086496985033238868757250241227280238023537123096707514660972862498923684998083317696241648829159740394798890927477167/1468844870831774447268003840000000000000000", + "entrance_mass": "29898949589421721863235314186112", + "event": 2687, + "stage": 15 + }, + { + "entrance_defect": "5552604434653404492326202146632648555645888894235076265544038364510221964471332433289643606116031191526468069698683364912645155967416428143859/2448074784719624078780006400000000000000000", + "entrance_mass": "687449590445880987173716162586496", + "event": 2779, + "stage": 16 + }, + { + "entrance_defect": "383003665621269193739885837364643137711582807262865470870613812148300568329922033877861317165489937513749433651046163289153038121700357422298831/7344224354158872236340019200000000000000000", + "entrance_mass": "15806139033147704339825284871898752", + "event": 2869, + "stage": 17 + }, + { + "entrance_defect": "326155049787256155157832340134847384764735276402770643581716325768728878950947843136976592484023494309280943080837466608094361777686262992724431/272008309413291564308889600000000000000000", + "entrance_mass": "363421601940370671219209686545270656", + "event": 2958, + "stage": 18 + } + ], + "physical_main_inputs": 3952, + "sites": { + "ADD": 2108, + "IDLE_ONE": 100, + "J": 18, + "LAMBDA": 226, + "QUERY": 8, + "SCALE": 180, + "SWAP": 455, + "noninteger_scalar": 297 + } + }, + "native": { + "bounds": { + "Gamma": { + "exact": "148410063514995949252033673132766658208788044686637910905148510954760838249558320252737098930963924559802399438531/3672112177079436118170009600000000000000000", + "strict_power_of_two": 235, + "witness": { + "cut": 71258, + "factor": "1", + "kind": "public-return", + "register": 1443 + } + }, + "M": { + "exact": "14476760998861861302944912510523645403533698246699472098415457537799148383517648848570009175350261608286421932685203/104451190814703960694613606400000000000000000", + "strict_power_of_two": 237, + "witness": { + "cut": 71222, + "factor": "1", + "kind": "stored", + "register": 1443 + } + }, + "Sigma": { + "exact": "148410063514995949252033673132766658208788044686637910905148510954760838249558320252737098930963924559802399438531/3672112177079436118170009600000000000000000", + "strict_power_of_two": 235, + "witness": { + "cut": 71222, + "factor": "1", + "kind": "stored", + "register": 1443 + } + } + }, + "census": { + "denominator_bits": 19, + "events": 71258, + "lifetimes": 54, + "max_denominator": 393216, + "max_numerator": 14729531, + "numerator_bits": 24, + "opcodes": { + "ADD": 61182, + "CLEAR": 54, + "COPY": 1, + "INIT": 54, + "MOVE": 6305, + "SCALE": 3662 + }, + "owned_labels": 51, + "peak_owned": 43, + "public": 1481, + "scalars": { + "dyadic": 60702, + "integer": 38904, + "noninteger": 25941, + "odd": 4143 + } + }, + "independent_adjoint": { + "Gamma": { + "active_residual_sites": 24531, + "entrance_mass": "14476760998861861302944912510523645403533698246699472098415457537799148383517648848570009175350261608286421932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788044686637910905148510954760838249558320252737098930963924559802399438531/3672112177079436118170009600000000000000000" + }, + "M": { + "active_residual_sites": 24531, + "entrance_mass": "14476760998861861302944912510523645403533698246699472098415457537799148383517648848570009175350261608286421932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788044686637910905148510954760838249558320252737098930963924559802399438531/3672112177079436118170009600000000000000000" + }, + "Sigma": { + "active_residual_sites": 24531, + "entrance_mass": "14476760998861861302944912510523645403533698246699472098415457537799148383517648848570009175350261608286421932685203/104451190814703960694613606400000000000000000", + "residual_mass": "148410063514995949252033673132766658208788044686637910905148510954760838249558320252737098930963924559802399438531/3672112177079436118170009600000000000000000" + } + } + } + }, + "scope": "Exact children for common grid. Total RDiv plus complete-fibre unitary contracts for rounded envelopes. Neither is a physical provider admission.", + "threshold": { + "H": 14181100000000000000, + "Kstar_bits": 14073, + "LP": 2229, + "scaled4096_Kstar_bits": 14085 + } + }, + "source_head": "2ee11a4460f23abf06d16b12f18c8ef9aca889f1", + "status": "PASS_P104_RETIMED_HELPER_STEP", + "word_canonical_sha256": "10b24ef20650bce0423c66abf5bd43a837e6d5dbe50c9ac973f17eae295ad62b" +} diff --git a/research/p104-causal-retimed-step/ROUND1-HITS.json b/research/p104-causal-retimed-step/ROUND1-HITS.json new file mode 100644 index 0000000000..f778973dee --- /dev/null +++ b/research/p104-causal-retimed-step/ROUND1-HITS.json @@ -0,0 +1,137 @@ +[ + { + "frame": 245, + "pivot": 228, + "cut": 39129, + "ranks": [ + 8, + 1 + ], + "gain": 0.0022742988813790888, + "paths": [ + { + "role": 1123, + "lo": 34017, + "hi": 45911, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 40126 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.008983403392178069, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + }, + { + "frame": 245, + "pivot": 232, + "cut": 39047, + "ranks": [ + 8, + 1 + ], + "gain": 0.0022742988813790888, + "paths": [ + { + "role": 1123, + "lo": 34017, + "hi": 45911, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 40126 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.008983403392178069, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + }, + { + "frame": 245, + "pivot": 438, + "cut": 37209, + "ranks": [ + 8, + 1 + ], + "gain": 0.0022742988813790888, + "paths": [ + { + "role": 1123, + "lo": 34017, + "hi": 45911, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 40126 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.008983403392178069, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + } +] diff --git a/research/p104-causal-retimed-step/ROUND1-LOG.txt b/research/p104-causal-retimed-step/ROUND1-LOG.txt new file mode 100644 index 0000000000..c4b68ec1ce --- /dev/null +++ b/research/p104-causal-retimed-step/ROUND1-LOG.txt @@ -0,0 +1,32 @@ +windows 17652 +forward 0 systems 0 saved 0 sec 0.0 +forward 5000 systems 0 saved 0 sec 0.17 +forward 10000 systems 0 saved 0 sec 0.36 +forward 15000 systems 0 saved 0 sec 0.48 +forward 20000 systems 37 saved 0 sec 0.61 +forward 25000 systems 2599 saved 397 sec 1.58 +forward 30000 systems 10562 saved 4101 sec 9.81 +forward 35000 systems 22370 saved 8371 sec 20.38 +forward 40000 systems 33139 saved 10536 sec 41.35 +forward 45000 systems 36076 saved 11716 sec 48.14 +forward 50000 systems 36369 saved 11870 sec 48.64 +forward 55000 systems 36474 saved 11929 sec 48.84 +forward 60000 systems 36474 saved 11929 sec 49.57 +prefix done 36474 saved 11929 sec 49.74415183067322 +reverse 60000 pairs 0 hits 0 sec 49.77 +reverse 55000 pairs 0 hits 0 sec 49.87 +reverse 50000 pairs 0 hits 0 sec 50.09 +reverse 45000 pairs 7 hits 0 sec 50.5 +reverse 40000 pairs 14230 hits 0 sec 72.34 +reverse 35000 pairs 41083 hits 3 sec 114.26 +reverse 30000 pairs 46573 hits 3 sec 132.06 +reverse 25000 pairs 53634 hits 3 sec 150.5 +reverse 20000 pairs 53634 hits 3 sec 152.22 +reverse 15000 pairs 53634 hits 3 sec 153.08 +reverse 10000 pairs 53634 hits 3 sec 153.55 +reverse 5000 pairs 53634 hits 3 sec 153.72 +reverse 0 pairs 53634 hits 3 sec 153.77 +paired 53634 hits 3 seconds 153.76695775985718 +{'frame': 245, 'pivot': 228, 'cut': 39129, 'ranks': [8, 1], 'gain': 0.0022742988813790888, 'paths': [{'role': 1123, 'lo': 34017, 'hi': 45911, 'frame': 245, 'old': 242, 'new': 127, 'moves': [40126], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.008983403392178069, 'private': False}]} +{'frame': 245, 'pivot': 232, 'cut': 39047, 'ranks': [8, 1], 'gain': 0.0022742988813790888, 'paths': [{'role': 1123, 'lo': 34017, 'hi': 45911, 'frame': 245, 'old': 242, 'new': 127, 'moves': [40126], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.008983403392178069, 'private': False}]} +{'frame': 245, 'pivot': 438, 'cut': 37209, 'ranks': [8, 1], 'gain': 0.0022742988813790888, 'paths': [{'role': 1123, 'lo': 34017, 'hi': 45911, 'frame': 245, 'old': 242, 'new': 127, 'moves': [40126], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.008983403392178069, 'private': False}]} diff --git a/research/p104-causal-retimed-step/SCREEN-HITS.json b/research/p104-causal-retimed-step/SCREEN-HITS.json new file mode 100644 index 0000000000..5f88aaf112 --- /dev/null +++ b/research/p104-causal-retimed-step/SCREEN-HITS.json @@ -0,0 +1,137 @@ +[ + { + "frame": 245, + "pivot": 228, + "cut": 43057, + "ranks": [ + 8, + 1 + ], + "gain": 0.002291760020324496, + "paths": [ + { + "role": 1123, + "lo": 37910, + "hi": 56194, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 44017 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.009052822470384747, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + }, + { + "frame": 245, + "pivot": 232, + "cut": 42897, + "ranks": [ + 8, + 1 + ], + "gain": 0.002291760020324496, + "paths": [ + { + "role": 1123, + "lo": 37910, + "hi": 56194, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 44017 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.009052822470384747, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + }, + { + "frame": 245, + "pivot": 438, + "cut": 40897, + "ranks": [ + 8, + 1 + ], + "gain": 0.002291760020324496, + "paths": [ + { + "role": 1123, + "lo": 37910, + "hi": 56194, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 44017 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "cost": 0.009052822470384747, + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } + } +] diff --git a/research/p104-causal-retimed-step/SCREEN-LOG.txt b/research/p104-causal-retimed-step/SCREEN-LOG.txt new file mode 100644 index 0000000000..c26ca2cade --- /dev/null +++ b/research/p104-causal-retimed-step/SCREEN-LOG.txt @@ -0,0 +1,36 @@ +windows 17982 +forward 0 systems 0 saved 0 sec 0.0 +forward 5000 systems 0 saved 0 sec 0.51 +forward 10000 systems 0 saved 0 sec 1.12 +forward 15000 systems 0 saved 0 sec 1.63 +forward 20000 systems 12 saved 0 sec 1.92 +forward 25000 systems 72 saved 13 sec 2.08 +forward 30000 systems 4109 saved 634 sec 3.16 +forward 35000 systems 13439 saved 3833 sec 11.01 +forward 40000 systems 25855 saved 7066 sec 20.69 +forward 45000 systems 35575 saved 9129 sec 47.52 +forward 50000 systems 37186 saved 9746 sec 49.56 +forward 55000 systems 37345 saved 9840 sec 49.97 +forward 60000 systems 37391 saved 9869 sec 50.33 +forward 65000 systems 37391 saved 9869 sec 51.11 +forward 70000 systems 37391 saved 9869 sec 51.66 +prefix done 37391 saved 9869 sec 51.71154475212097 +reverse 70000 pairs 0 hits 0 sec 51.72 +reverse 65000 pairs 0 hits 0 sec 51.78 +reverse 60000 pairs 0 hits 0 sec 51.96 +reverse 55000 pairs 0 hits 0 sec 52.19 +reverse 50000 pairs 0 hits 0 sec 52.61 +reverse 45000 pairs 159 hits 0 sec 57.48 +reverse 40000 pairs 39148 hits 3 sec 120.28 +reverse 35000 pairs 41395 hits 3 sec 130.29 +reverse 30000 pairs 43553 hits 3 sec 149.07 +reverse 25000 pairs 43583 hits 3 sec 152.37 +reverse 20000 pairs 43583 hits 3 sec 153.51 +reverse 15000 pairs 43583 hits 3 sec 154.33 +reverse 10000 pairs 43583 hits 3 sec 154.85 +reverse 5000 pairs 43583 hits 3 sec 154.99 +reverse 0 pairs 43583 hits 3 sec 155.03 +paired 43583 hits 3 seconds 155.02822494506836 +{'frame': 245, 'pivot': 228, 'cut': 43057, 'ranks': [8, 1], 'gain': 0.002291760020324496, 'paths': [{'role': 1123, 'lo': 37910, 'hi': 56194, 'frame': 245, 'old': 242, 'new': 127, 'moves': [44017], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.009052822470384747, 'private': False}]} +{'frame': 245, 'pivot': 232, 'cut': 42897, 'ranks': [8, 1], 'gain': 0.002291760020324496, 'paths': [{'role': 1123, 'lo': 37910, 'hi': 56194, 'frame': 245, 'old': 242, 'new': 127, 'moves': [44017], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.009052822470384747, 'private': False}]} +{'frame': 245, 'pivot': 438, 'cut': 40897, 'ranks': [8, 1], 'gain': 0.002291760020324496, 'paths': [{'role': 1123, 'lo': 37910, 'hi': 56194, 'frame': 245, 'old': 242, 'new': 127, 'moves': [44017], 'old_paid': [5], 'new_paid': [4, 1], 'cost': 0.009052822470384747, 'private': False}]} diff --git a/research/p104-causal-retimed-step/SOURCES.json b/research/p104-causal-retimed-step/SOURCES.json new file mode 100644 index 0000000000..b06c2f774e --- /dev/null +++ b/research/p104-causal-retimed-step/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ] +} diff --git a/research/p104-causal-retimed-step/TASK.json b/research/p104-causal-retimed-step/TASK.json new file mode 100644 index 0000000000..e908c586a8 --- /dev/null +++ b/research/p104-causal-retimed-step/TASK.json @@ -0,0 +1,145 @@ +{ + "task_id": "p104-side-correction", + "scope_status": "changed", + "scope_change_reason": "Move from the historical selected #5599 card to exact #7004 after tracing current live successors. Retiming one paid role opens an additional legal helper split; its complete invoice must beat #7004 rather than an obsolete predecessor.", + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "priority_revision": 8, + "selection_seed": "3380be319a1b0ac8eeb6146e9db8d49c", + "concrete_question": "Does a contact-free paid retiming on exact #7004 open a dyadic independent-helper split beating kappa .00363206219?", + "domain": "Group (3,127), existing strictly nested frames, one contact-free retimed role; complete exact rational prefix/suffix and source/candidate words; final edit uses integer ADDs. All #7004 contracts retained.", + "success": "Changed complete profile, exact arbitrary-input and chart replay, complete caller/pricing/ordinary bill and all outer inequalities.", + "stop": "Reject if complete paid retiming costs consume split credit or ordinary budget fails.", + "predecessors": [ + "Ali Romman #5599 helper split and dyadic basis methods", + "Jerry Chen / CubeJerry #6805/#6916 paid retiming", + "DreamingOfClouds #6931 word and caller", + "retained source lineage in #6931 NOTICE", + "DreamingOfClouds #6936/#6937; CubeJerry #7000/#7001; ToikY #7003/#7004" + ], + "evidence_status": "Author/source-aware complete direct CPython3.14.7 replay passed twice; frozen receipt comparison passed. Generic3.12 execution unrun locally; no human/kernel acceptance.", + "overlap": "Live coverage: 398 open, 6175 closed PR bodies, 7013 Discussion records; #6931 successor chain traced through #7004. Canonical main refreshed unchanged at 17469fff78.", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "predecessor_head": "2ee11a4460f23abf06d16b12f18c8ef9aca889f1", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19519779", + "schema_version": 1, + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "actual_scope": "Does a contact-free paid retiming on exact #7004 open a dyadic independent-helper split beating kappa .00363206219?", + "bottleneck_link": "Improve the complete paid-minus-productive moment with the same #7004 physical caller and no new ownership or scalar alphabet.", + "stop_rule": "One verified source-bound new complete claim; do not expand the same family after this result.", + "evidence": "WITNESS.json, WORD.json.gz, RESULT.json and verify.py; exact source bytes in inputs/pr7004.tar.", + "author": "Prepared for dillona with substantial OpenAI Codex assistance", + "outcome": "completed", + "open_questions": [ + { + "question": "Can the other two screened cuts be jointly realized without paying the same carrier repeatedly?", + "why_it_matters": "The three nominations share role1123 and are not independent gains.", + "first_step": "Construct a joint exact prefix/suffix witness and complete changed invoice before search expansion.", + "blocked_by": "Joint capacity, target independence and correction compatibility remain unproved." + }, + { + "question": "Does the inherited supplier admit actual rounded children under one physical tariff?", + "why_it_matters": "The finite exact-word result does not settle fixed-tape supplier admission.", + "first_step": "Continue predecessor #6998 provider/tariff binding with these exact source pins.", + "blocked_by": "Inherited five assumptions and odd-return/owned-ascent/provider contracts." + } + ], + "round1_source": { + "source_head": "e084df3698c6329eb2129c417d5ea8694a7e8d09", + "path": "research/p104-causal-split-native/data/word.json.gz", + "sha256": "c162203fa84964b525882a5b62f1460ff6996acdf27dd178c53c6c1d27830d7f", + "scope": "exploratory nominations only, not the scientific baseline", + "screen_exponent_kappa": ".00360410481" + } +} diff --git a/research/p104-causal-retimed-step/VALIDATION.md b/research/p104-causal-retimed-step/VALIDATION.md new file mode 100644 index 0000000000..a769924740 --- /dev/null +++ b/research/p104-causal-retimed-step/VALIDATION.md @@ -0,0 +1,15 @@ +# Validation and limits + +Local environment: CPython 3.14.7, macOS arm64; exact details in ENVIRONMENT.json. Scientific baseline is #7004 head2ee11a4460f23abf06d16b12f18c8ef9aca889f1. Canonical main refreshed at entry, pivot and submission:17469fff78c22941280f04d39dc5a1faee09c840, priorities revision8, selected record unchanged. + +Final stdout is retained in REPLAY.txt; its SHA256 is recorded in ENVIRONMENT.json. + +Executed: + +- Direct complete verifier with a new receipt output: passed source rebuild, rational cut and all-input endpoint/adjoint, exact forward common-grid, formal caller, full invoice and ordinary bill, BIT binding, two rational price engines, compiler and 54+4 outer gates, precision envelopes, four exact512-column chart/phase checks, five construction mutations, relaxed native replay and full512-component physical replay. The initial status spelling was corrected without changing scientific data. +- Final direct command against frozen RESULT.json: passed, ending PASS_P104_RETIMED_HELPER_STEP. Command: `python3 -I -B research/p104-causal-retimed-step/verify.py`. +- `python3 -B scripts/research_package.py --package research/p104-causal-retimed-step --check-only`: passed metadata and exact provenance pins; not a mathematical acceptance check. + +The local interpreter has no Python 3.12, so the repository's registered 3.12 execution is unrun locally. The registered manifest supplies the complete command for hosted replay. Optimized mode is rejected deliberately because borrowed source engines use assertions. No Lean, Docker, whole selected multiplier or all-history replay was run. + +Exact endpoint replay and finite physical replay are distinct evidence. The original source engines retain their attribution and assumptions; these checks do not constitute independent human/kernel review or full supplier admission. In particular, all five framework assumptions plus #7004's exact odd-return, owned-ascent, caller, paired BIT and physical-tariff contracts remain. diff --git a/research/p104-causal-retimed-step/VERIFY.json b/research/p104-causal-retimed-step/VERIFY.json new file mode 100644 index 0000000000..f1330ca857 --- /dev/null +++ b/research/p104-causal-retimed-step/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Regenerate exact predecessor and successor; rational prefix/suffix and forward/adjoint all-input checks, every new Gaussian column/phase, complete invoice and ordinary bill, two rational price engines, precision source engines, BIT binding, compiler and 54+4 outer gates, full width-512 physical replay and mutation controls. Source engines reject optimized mode explicitly." + } + ] +} diff --git a/research/p104-causal-retimed-step/WITNESS.json b/research/p104-causal-retimed-step/WITNESS.json new file mode 100644 index 0000000000..a7359edd58 --- /dev/null +++ b/research/p104-causal-retimed-step/WITNESS.json @@ -0,0 +1,43 @@ +{ + "frame": 245, + "pivot": 1123, + "cut": 43057, + "ranks": [ + 8, + 1 + ], + "paths": [ + { + "role": 1123, + "lo": 37910, + "hi": 56194, + "frame": 245, + "old": 242, + "new": 127, + "moves": [ + 44017 + ], + "old_paid": [ + 5 + ], + "new_paid": [ + 4, + 1 + ], + "private": false + } + ], + "a": { + "1123": "1" + }, + "b": { + "1123": "1", + "843": "1" + }, + "c": { + "1123": "1" + }, + "d": { + "1123": "1" + } +} diff --git a/research/p104-causal-retimed-step/WORD.json.gz b/research/p104-causal-retimed-step/WORD.json.gz new file mode 100644 index 0000000000..704a49dbf9 Binary files /dev/null and b/research/p104-causal-retimed-step/WORD.json.gz differ diff --git a/research/p104-causal-retimed-step/construct.py b/research/p104-causal-retimed-step/construct.py new file mode 100644 index 0000000000..1d816292f3 --- /dev/null +++ b/research/p104-causal-retimed-step/construct.py @@ -0,0 +1,36 @@ +"""Retiming within one contact-free interval, then a checked helper split. +OpenAI Codex for dillona; Ali Romman and CubeJerry's split method. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from split import split +from support import L + +def prepare(word, hit): + paths=hit['paths']; L.need(len(paths)==1,'Exactly one paid retiming') + p=paths[0];r=p['role'];a,b,f=p['old'],p['new'],hit['frame'];cut=hit['cut'] + L.need(p['frame']==f and p['lo']<=cut<=p['hi'],'Cut in declared interval') + actual=[i for i in range(p['lo'],p['hi']) if word['program'][i][1]==r] + L.need(actual==p['moves'],'Every role event in interval is a relocated MOVE') + L.need(all(not(e[0]in('ADD','COPY')and e[2]==r)for e in word['program'][p['lo']:p['hi']]),'No intervening source read') + path=[word['program'][i]for i in actual] + L.need(path and all(e[0]=='MOVE' and e[1]==r and e[4]==p['private']for e in path),'Only MOVE events') + L.need(path[0][2]==a and path[-1][3]==b and all(x[3]==y[2]for x,y in zip(path,path[1:])),'Complete path') + spaces=[L.span(x)for x in word['frames']] + L.need(spaces[a]<=spaces[f]<=spaces[b] or spaces[b]<=spaces[f]<=spaces[a],'Nested intermediate frame') + remove=set(actual);program=[];split_cut=None + for i in range(len(word['program'])+1): + if i==cut: + if a!=f:program.append(['MOVE',r,a,f,p['private']]) + split_cut=len(program)-1 + if f!=b:program.append(['MOVE',r,f,b,p['private']]) + if i=maxgain-1e-12:continue + h=dict(role=r,lo=lo+1,hi=hi,frame=f,old=a,new=b,moves=mi,old_paid=paid,new_paid=[d1,d2],cost=cost,private=r>=n) + idx=len(windows);windows.append(h);starts[lo+1].append(idx);ends[hi+1].append(idx) +print('windows',len(windows),flush=True) +rows=[{r:Q(1)}if r=gain-1e-12 or len(used)!=1:continue + if not dyadic_program(basis(c,d,p,U)+basis(a,b,p,f)):continue + key=(f,p,tuple(sorted(c.items())),tuple(sorted(d.items())),tuple(sorted(a.items())),tuple(sorted(b.items()))) + if key in seen:continue + seen.add(key);hits.append(dict(frame=f,pivot=p,cut=cut,ranks=[dims[f],9-dims[f]],gain=gain-cost,paths=[windows[idx]for idx in used],a=a,b=b,c=c,d=d)) + if cut: + e=w['program'][cut-1];op,r=e[:2] + if op in('INIT','CLEAR'):cols[r]={} + elif op=='SCALE':cols[r]={k:v*Q(e[2])for k,v in cols[r].items()} + elif op in('ADD','COPY'): + add(cols[e[2]],cols[r],Q(e[3])) + if op=='COPY':cols[r]={} + if cut%5000==0:print('reverse',cut,'pairs',pairs,'hits',len(hits),'sec',round(time.time()-start,2),flush=True) +hits.sort(key=lambda h:-h['gain']) +(Path(sys.argv[2])).write_text(json.dumps(encode(hits),indent=2)+'\n') +print('paired',pairs,'hits',len(hits),'seconds',time.time()-start,flush=True) +for h in hits[:10]:print({k:v for k,v in encode(h).items()if k not in('a','b','c','d')},flush=True) diff --git a/research/p104-causal-retimed-step/inputs/pr7004.tar b/research/p104-causal-retimed-step/inputs/pr7004.tar new file mode 100644 index 0000000000..ba8815bae1 Binary files /dev/null and b/research/p104-causal-retimed-step/inputs/pr7004.tar differ diff --git a/research/p104-causal-retimed-step/source.py b/research/p104-causal-retimed-step/source.py new file mode 100644 index 0000000000..0e405e5570 --- /dev/null +++ b/research/p104-causal-retimed-step/source.py @@ -0,0 +1,53 @@ +"""Authenticated read-only extraction and rebuilding of the exact #7004 input.""" +from contextlib import contextmanager +from hashlib import sha256,sha1 +from pathlib import Path +import importlib.util,json,sys,tarfile,tempfile +HERE=Path(__file__).resolve().parent + +def need(ok, why): + if not ok:raise ValueError(why) + +def read(p): + import gzip + raw=Path(p).read_bytes() + return json.loads(gzip.decompress(raw)if raw[:2]==b'\x1f\x8b'else raw) + +def load(name,path): + spec=importlib.util.spec_from_file_location(name,path);m=importlib.util.module_from_spec(spec);sys.modules[name]=m;spec.loader.exec_module(m);return m + +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':')).encode() + +@contextmanager +def sources(): + pins=read(HERE/'INPUTS.json');archive=HERE/'inputs/pr7004.tar' + need(sha256(archive.read_bytes()).hexdigest()==pins['archive_sha256'],'Immutable source archive SHA256') + with tempfile.TemporaryDirectory(prefix='kappa7004-')as tmp: + root=Path(tmp).resolve();expected={x['path']:x for x in pins['files']};seen=set() + with tarfile.open(archive)as tar: + for member in tar: + if member.isdir():continue + need(member.isfile()and member.name in expected and member.name not in seen,'Unique listed regular source member') + path=root/member.name;need(path.resolve().is_relative_to(root),'Safe source member') + raw=tar.extractfile(member).read();pin=expected[member.name] + need(len(raw)==pin['size'] and sha256(raw).hexdigest()==pin['sha256'] and sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==pin['git_blob'],'Exact per-file Git blob and SHA256') + path.parent.mkdir(parents=True,exist_ok=True);path.write_bytes(raw);seen.add(member.name) + need(seen==set(expected),'Complete source closure') + base=root/'research';previous=base/'shared-wire-stop-fusion';vendor=base/'shared-wire-split-composition' + old_path=list(sys.path);sys.path.insert(0,str(previous)) + try: + builder=load('successor_previous_builder',previous/'build_candidate.py') + peer=load('successor_peer_builder',base/'peer-move-retiming/build_candidate.py') + source=read(vendor/'data/final.json.gz');spaces=[builder.span(x)for x in source['frames']];history,_,_=builder.inventory(source,spaces) + mid,_,_=builder.place(source,read(previous/'EDITS.json'),spaces,history) + word,_,_=peer.edit(mid) + need(sha256(canonical(word)).hexdigest()==pins['source_canonical_sha256'],'Exact regenerated #7004 source word') + yield base,word + finally:sys.path[:]=old_path + +if __name__=='__main__': + import argparse,gzip + parser=argparse.ArgumentParser();parser.add_argument('--output',type=Path,required=True);args=parser.parse_args() + with sources()as(base,word): + raw=canonical(word) + with args.output.open('xb')as out:out.write(gzip.compress(raw,mtime=0)if args.output.suffix=='.gz'else raw+b'\n') diff --git a/research/p104-causal-retimed-step/split.py b/research/p104-causal-retimed-step/split.py new file mode 100644 index 0000000000..3260b2a0a3 --- /dev/null +++ b/research/p104-causal-retimed-step/split.py @@ -0,0 +1,145 @@ +"""Split independent helper jobs with three scalar basis changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Adapted for arbitrary counted owned-field inventory by @CubeJerry with OpenAI assistance. +Successor: OpenAI Codex for dillona excludes both hosted main planes from helper groups. +The source word and caller retain the credits in README.md. +""" +from copy import deepcopy +from fractions import Fraction as Q +from support import L + + +def inverse(program): + return [[e[0], *e[1:-2], + str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])), e[-1]] + for e in reversed(program)] + + +def basis(a, b, pivot, frame): + """Return B with row pivot equal to a and B b equal to e_pivot.""" + L.need(sum(v*b.get(k, 0) for k, v in a.items()) == 1, 'Unit basis pairing') + roles = sorted(set(a) | set(b) | {pivot}) + values, program = dict(b), [] + + def emit(event): + program.append(event) + r, q = event[1], Q(event[-2]) + if event[0] == 'SCALE': + values[r] = values.get(r, 0)*q + else: + values[r] = values.get(r, 0)+q*values.get(event[2], 0) + + j = pivot if b.get(pivot) else next(r for r in roles if b.get(r)) + if j != pivot: + for event in [['ADD', pivot, j, '1', frame], + ['ADD', j, pivot, '-1', frame], + ['ADD', pivot, j, '1', frame], + ['SCALE', j, '-1', frame]]: + emit(event) + if values[pivot] != 1: + emit(['SCALE', pivot, str(1/values[pivot]), frame]) + for r in roles: + if r != pivot and values.get(r): + emit(['ADD', r, pivot, str(-values[r]), frame]) + L.need(all(values.get(r, 0) == int(r == pivot) for r in roles), 'Basis column') + inverse_rows = {r: {r: Q(1)} for r in roles} + for e in inverse(program): + if e[0] == 'SCALE': + inverse_rows[e[1]] = {k: Q(e[-2])*v for k, v in inverse_rows[e[1]].items()} + else: + L.add(inverse_rows[e[1]], inverse_rows[e[2]], Q(e[-2])) + row = {} + for r, q in a.items(): + L.add(row, inverse_rows[r], q) + L.need(row[pivot] == 1, 'Basis row coefficient') + for r in roles: + if r != pivot and row.get(r): + program.append(['ADD', pivot, r, str(row[r]), frame]) + return program + + +def check_cut(word, h): + """Check the whole prefix row and suffix column over the rationals.""" + n, cut, f, p = word['public'], h['cut_after'], h['frame'], h['pivot'] + a, b, c, d = ({int(k): Q(v) for k, v in h[s].items()} for s in ('a', 'b', 'c', 'd')) + main = set(word['live']) | {r+112 for r in word['live']} | set(word['hosted']['X2']) | set(word['hosted']['Y2']) + L.need(p < n and p not in main, 'A helper supplies the retained output role') + u, v = word['initial'][p], word['final'][p] + group = {r for r in range(n) if r not in main and + (word['initial'][r], word['final'][r]) == (u, v)} + L.need(set(c) | set(d) <= group, 'Both boundary vectors use one helper group') + L.need(L.span(word['frames'][u]) < L.span(word['frames'][f]) < L.span(word['frames'][v]), + 'Two strictly productive nested targets') + L.need(h['ranks'] == [len(word['frames'][f])-len(word['frames'][u]), + len(word['frames'][v])-len(word['frames'][f])], 'Declared split ranks') + rows = [{r: Q(1)} if r < n else {} for r in range(n+word['owned_fields'])] + current = word['initial']+[None]*word['owned_fields'] + for e in word['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + current[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + current[r] = e[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[r] = {k: Q(e[-2])*x for k, x in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: Q(e[-2])*x for k, x in rows[e[2]].items()} + else: + L.add(rows[r], rows[e[2]], Q(e[-2])) + L.need(all(current[r] == f for r in set(a) | set(b) | {p}), 'One intermediate chart') + total = {} + for r, q in a.items(): + L.add(total, rows[r], q) + L.need(total == c, 'Exact prefix functional; no other input') + column = [b.get(r, Q(0)) for r in range(n+word['owned_fields'])] + for e in word['program'][cut+1:]: + op, r = e[:2] + if op in ('INIT', 'CLEAR'): + column[r] = Q(0) + elif op == 'SCALE': + column[r] *= Q(e[-2]) + elif op == 'COPY': + column[r] = Q(e[-2])*column[e[2]] + elif op == 'ADD': + column[r] += Q(e[-2])*column[e[2]] + L.need(column == [d.get(r, Q(0)) for r in range(n+word['owned_fields'])], 'Exact suffix direction; no other output') + L.need(sum(x*b.get(r, 0) for r, x in a.items()) == + sum(x*d.get(r, 0) for r, x in c.items()) == 1, 'Both independent pairings') + return a, b, c, d + + +def split(word, h): + a, b, c, d = check_cut(word, h) + n, p, f, cut = word['public'], h['pivot'], h['frame'], h['cut_after'] + u, v = word['initial'][p], word['final'][p] + + def shift_owned(event): + e = event.copy() + e[1] += int(e[1] >= n) + if e[0] in ('ADD', 'COPY'): + e[2] += int(e[2] >= n) + return e + + def use_successor(event): + e = event.copy() + if e[1] == p: + e[1] = n + if e[0] in ('ADD', 'COPY') and e[2] == p: + e[2] = n + return e + + boundary, middle = basis(c, d, p, u), basis(a, b, p, f) + out = deepcopy(word) + out['public'] = n+1 + out['initial'].append(f) + out['final'].append(v) + out['final'][p] = f + out['program'] = inverse(boundary) + out['program'] += [shift_owned(e) for e in word['program'][:cut+1]] + out['program'] += [shift_owned(e) for e in middle] + out['program'] += [use_successor(shift_owned(e)) for e in inverse(middle)] + out['program'] += [use_successor(shift_owned(e)) for e in word['program'][cut+1:]] + out['program'] += [use_successor([*e[:-1], v]) for e in boundary] + return out diff --git a/research/p104-causal-retimed-step/support.py b/research/p104-causal-retimed-step/support.py new file mode 100644 index 0000000000..192cd38d27 --- /dev/null +++ b/research/p104-causal-retimed-step/support.py @@ -0,0 +1,18 @@ +"""Small exact sparse operations, retained from Ali Romman/CubeJerry. Apache-2.0.""" +class L: + @staticmethod + def need(ok, why): + if not ok: raise ValueError(why) + @staticmethod + def add(dst, src, q): + for k,v in tuple(src.items()): + value=dst.get(k,0)+q*v + if value: dst[k]=value + else: dst.pop(k,None) + @staticmethod + def span(basis): + out={0} + for v in basis: + L.need(type(v) is int and 0