diff --git a/research/complex-routing-leaf-fusion/CAP-SOURCE.json b/research/complex-routing-leaf-fusion/CAP-SOURCE.json new file mode 100644 index 0000000000..d56c816ec9 --- /dev/null +++ b/research/complex-routing-leaf-fusion/CAP-SOURCE.json @@ -0,0 +1,9 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "path": "research/t74-joint-twelve/vendor/ceiling.py", + "local_path": "vendor/ceiling.py", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "credit": "Douglas Colkitt, with Claude assistance; retained unchanged. Adapter derived from Tekalign PR2751 packing_cap.py, with Codex assistance." +} diff --git a/research/complex-routing-leaf-fusion/CLAIM.json b/research/complex-routing-leaf-fusion/CLAIM.json new file mode 100644 index 0000000000..d352e67b80 --- /dev/null +++ b/research/complex-routing-leaf-fusion/CLAIM.json @@ -0,0 +1,26 @@ +{ + "status": "COMPLETE_FINITE_RELEASE_PASSED_CONDITIONAL_KAPPA", + "complex_lower": "0.001717256973467002308270", + "complex_upper": "0.001717256973467002308271", + "kappa": "17172569734670023082699999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017172569734670023082699999999999999999999998999999999999999999999999", + "profile": { + "1": 1591740, + "2": 430902, + "3": 204396, + "4": 79920, + "5": 22532, + "8": 5328, + "32": 1, + "48": 26558 + }, + "comparison_pr": 2751, + "comparison_head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "comparison_kappa": "17171415863484263381089999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "absolute_gain": "115387118575970161/1000000000000000000000000", + "relative_gain": "1153871185759701610000000000000000000000000000000000000000000000/17171415863484263381089999999999999999999998999999999999999999999999", + "relative_gain_percent_decimal": "0.006719720697076920262999344663512072867487887126182086416724216655132904", + "credited_refit_pr": 2733, + "credited_refit_head": "a63c55ff56aaa8645d64d1162d1f017b59ded42a", + "scope": "New composition of the credited PR2733 frame refit with PR2751 joint twelve-source recovery. Complete finite native, supplier and modern outer release passed; inherited universal hypotheses and selected frontier unchanged." +} diff --git a/research/complex-routing-leaf-fusion/CREDIT-PINS.json b/research/complex-routing-leaf-fusion/CREDIT-PINS.json new file mode 100644 index 0000000000..135d91f4f6 --- /dev/null +++ b/research/complex-routing-leaf-fusion/CREDIT-PINS.json @@ -0,0 +1,20 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "pr": 2733, + "head": "a63c55ff56aaa8645d64d1162d1f017b59ded42a", + "root": "references/pr2733", + "files": { + "PROOF.md": { + "sha256": "7e029f68b0ff7beb0b1ba1f9013d525ec97060c0309026b3838d4d2680cc5dd0", + "git_blob": "452212aa89fa23a3c058b5485c9f97b8877f4cb6" + }, + "CLAIM.json": { + "sha256": "7402be1dcf6225f36fe727f0d0d5ae801de3b5dfda5bf18f8c1290e71d6f25c1", + "git_blob": "4d848d5466e2b9b203891ac8a2ad75fd97124c9b" + }, + "NOTICE": { + "sha256": "43b0546bcdf17863c8c2199b2da3f436b4fa92b634ae36a0e793ef10ce3f8b98", + "git_blob": "6dacc7b2ce7ad75c7574914c8b30fa64611be9b0" + } + } +} diff --git a/research/complex-routing-leaf-fusion/FULL-REPLAY-CHANGES.patch b/research/complex-routing-leaf-fusion/FULL-REPLAY-CHANGES.patch new file mode 100644 index 0000000000..4f1f4c3220 --- /dev/null +++ b/research/complex-routing-leaf-fusion/FULL-REPLAY-CHANGES.patch @@ -0,0 +1,118 @@ +--- pr2751/full_replay.py ++++ full_replay.py +@@ -1,7 +1,8 @@ + #!/usr/bin/env python3 + # SPDX-License-Identifier: Apache-2.0 +-# Tekalign (@tekuuu), with substantial OpenAI Codex assistance. +-"""Cold reproduction of the joint twelve-source/pre-life composition. ++# Derived from Tekalign / PR2751 full_replay.py, with substantial OpenAI Codex assistance. ++# This derivative composes Marius-Paul Dumitrean / PR2733's exact frame refit. ++"""Cold reproduction of the twelve-source / five-frame composition. + + Default: authenticated source download, fresh native providers and retained + parent admission, then the complete original supplier/release verifier. An +@@ -27,6 +28,8 @@ + from urllib.parse import quote + from urllib.request import Request, urlopen + ++from derive_runtime import derive_runtime ++ + HERE = Path(__file__).resolve().parent + REPOSITORY = HERE.parents[1] + STEPS = ['native', 'ledgers', 'local-replay', 'wrappers', 'phases'] +@@ -116,6 +119,7 @@ + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--source', type=Path, help='Exact original PR2679 package directory; otherwise download pinned files.') + ap.add_argument('--work', type=Path, required=True) ++ ap.add_argument('--composition-source', type=Path, help='Exact PR2751 package; otherwise fetch four pinned composition files.') + ap.add_argument('--prepared-native-cache', type=Path, help='Explicit reuse of the complete published pinned cache.') + ap.add_argument('--jobs', type=int, default=4) + a = ap.parse_args() +@@ -129,10 +133,22 @@ + need(versions['sympy'] == '1.14.0', 'pinned predecessor evidence requires sympy==1.14.0') + work = a.work.resolve() + need(not work.exists() and not work.is_relative_to(REPOSITORY), 'fresh external work required') +- for path in (a.source, a.prepared_native_cache): ++ for path in (a.source, a.composition_source, a.prepared_native_cache): + need(path is None or (path.is_dir() and not work.is_relative_to(path.resolve())), 'input/work separation') +- pins, reuse, claim = read(HERE / 'SOURCE-FILES.json'), read(HERE / 'REUSE-PINS.json'), read(HERE / 'CLAIM.json') ++ config, claim = read(HERE / 'FULL-REPLAY-PINS.json'), read(HERE / 'CLAIM.json') ++ reuse = read(HERE / 'evidence/NATIVE-RECEIPT.json') if a.prepared_native_cache else None + work.mkdir(parents=True) ++ composition = work / 'composition' ++ composition.mkdir() ++ for name, expected in config['files'].items(): ++ safe(name) ++ body = ((a.composition_source / name).read_bytes() if a.composition_source ++ else download(config['base_url'] + quote(name, safe='/'), expected)) ++ need(hashlib.sha256(body).hexdigest() == expected, 'composition source bytes: ' + name) ++ destination = composition / name ++ destination.parent.mkdir(parents=True, exist_ok=True) ++ destination.write_bytes(body) ++ pins = read(composition / 'SOURCE-FILES.json') + env = dict(os.environ, PYTHONDONTWRITEBYTECODE='1', PYTHONUTF8='1', PYTHONINTMAXSTRDIGITS='0', + OPENBLAS_NUM_THREADS='1', OMP_NUM_THREADS='1') + for name in ('PYTHONOPTIMIZE', 'WITNESS_SPEC', 'WITNESS_DISCOVER', 'WITNESS_RECORD'): +@@ -157,10 +173,10 @@ + run('literal-review', HERE / 'verify.py') + source = work / 'source' + source_copy(a.source.resolve() if a.source else None, source, pins, a.jobs) +- overlay = read(HERE / 'OVERLAY-PINS.json') ++ overlay = read(composition / 'OVERLAY-PINS.json') + need(sha(source/'MANIFEST.json') == overlay['original_manifest_sha256'], 'overlay base manifest') +- need(sha(HERE/'DERIVATIVE-OVERLAY.tar.gz') == overlay['archive_sha256'], 'overlay archive') +- with tarfile.open(HERE/'DERIVATIVE-OVERLAY.tar.gz') as archive: ++ need(sha(composition/'DERIVATIVE-OVERLAY.tar.gz') == overlay['archive_sha256'], 'overlay archive') ++ with tarfile.open(composition/'DERIVATIVE-OVERLAY.tar.gz') as archive: + members=archive.getmembers() + need(set(m.name for m in members)==set(overlay['files']) and len(members)==len(overlay['files']), 'exact overlay paths') + for member in members: +@@ -170,7 +186,25 @@ + (source/member.name).write_bytes(body) + need(sha(source/'MANIFEST.json')==overlay['derived_manifest_sha256'] and + tree(source,('MANIFEST.json',))==read(source/'MANIFEST.json'), 'complete derived source tree') +- pins=dict(pins,commit='local-joint12-pr2733',manifest_sha256=overlay['derived_manifest_sha256']) ++ changes = derive_runtime(source, HERE) ++ need(sha(source/'MANIFEST.json') == config['derived_manifest_sha256'] ++ and tree(source, ('MANIFEST.json',)) == read(source/'MANIFEST.json'), 'complete refit source tree') ++ write(work/'DERIVATION.json', changes) ++ pins=dict(pins,commit=config['source_commit'],manifest_sha256=config['derived_manifest_sha256']) ++ # Only source bindings and the strict predecessor comparison change in the ++ # authenticated admission driver. Its physical costs and controls remain. ++ admission = (composition/'workflow/admit.py').read_text() ++ edits = [("SOURCE_COMMIT = 'local-joint12-pr2733'", "SOURCE_COMMIT = " + repr(config['source_commit'])), ++ ("SOURCE_MANIFEST = '7980dbde79b63de4093cde89d1564a18c6bf16a2e35d810e38cf9797fe09e0cf'", ++ "SOURCE_MANIFEST = " + repr(config['derived_manifest_sha256'])), ++ ("previous = Q('0.0017161404259974415161889999999999999999999998999999999999999999999999')", ++ "previous = Q(" + repr(read(HERE/'vendor/pr2751/CLAIM.json')['kappa']) + ")")] ++ for before, after in edits: ++ need(admission.count(before) == 1, 'exact admission patch preimage') ++ admission = admission.replace(before, after) ++ (work/'admit.py').write_text(admission) ++ write(work/'ADMISSION-CHANGES.json', edits) ++ + cache = work / 'native-cache' + if a.prepared_native_cache: + need(tree(a.prepared_native_cache.resolve()) == reuse['cache_files'], 'published complete cache pins') +@@ -221,8 +255,8 @@ + source_commit=pins['commit'], manifest_sha256=pins['manifest_sha256'], providers=providers, + retained_parent_receipt_sha256=sha(receipts / 'RECEIPT.json'), cache_files=tree(cache)) + write(work / 'NATIVE-RECEIPT.json', native_receipt) +- run('complete-admission', HERE / 'workflow/admit.py', '--source', source, +- '--fill', HERE / 'inputs/FILL.json.gz', '--order', HERE / 'inputs/ORDER.json', ++ run('complete-admission', work / 'admit.py', '--source', source, ++ '--fill', HERE / 'vendor/pr2751/inputs/FILL.json.gz', '--order', HERE / 'vendor/pr2751/inputs/ORDER.json', + '--native-cache', cache, '--native-receipt', work / 'NATIVE-RECEIPT.json', + '--work', work / 'admission', '--jobs', a.jobs) + result = read(work / 'admission/RESULT.json') +@@ -230,8 +264,8 @@ + and Q(result['kappa']) == Q(claim['kappa']) and Q(result['complex_lower']) == Q(claim['complex_lower']), + 'published complete claim binding') + need(result['profile'] == {str(k):v for k,v in read(HERE / 'CLAIM.json')['profile'].items()}, 'published complete profile binding') +- result.update(status='PASS_T74_JOINT_TWELVE_COLD_COMPLETE_RELEASE', explicit_native_cache_reuse=bool(a.prepared_native_cache), +- source_files_sha256=sha(HERE / 'SOURCE-FILES.json'), native_receipt_sha256=sha(work / 'NATIVE-RECEIPT.json'), ++ result.update(status='PASS_T74_JOINT_TWELVE_REFIT_COLD_COMPLETE_RELEASE', explicit_native_cache_reuse=bool(a.prepared_native_cache), ++ source_files_sha256=sha(composition / 'SOURCE-FILES.json'), native_receipt_sha256=sha(work / 'NATIVE-RECEIPT.json'), + cold_stages=stages, cold_seconds=time.monotonic()-started, + environment=dict(python=platform.python_version(), executable=sys.executable, versions=versions)) + write(work / 'RESULT.json', result) diff --git a/research/complex-routing-leaf-fusion/FULL-REPLAY-PINS.json b/research/complex-routing-leaf-fusion/FULL-REPLAY-PINS.json new file mode 100644 index 0000000000..9b40d7aece --- /dev/null +++ b/research/complex-routing-leaf-fusion/FULL-REPLAY-PINS.json @@ -0,0 +1,12 @@ +{ + "base_url": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/4cfbb0cc8314d7fb4e8e754545a49a42eb590a69/research/t74-joint-twelve/", + "derived_manifest_sha256": "1e75eabffe1ce311cc3bddc05e76118cbdedfc806200a906c57fbc5a5dd213eb", + "files": { + "DERIVATIVE-OVERLAY.tar.gz": "16468f7428c6e01522fcb15a8e3040d13de6cb8856428e32dcfbce8dbe46b8ec", + "OVERLAY-PINS.json": "c5aab657b189d1324b75c2a35dd21063877229ebfd58b4b64261fdf0e5861e75", + "SOURCE-FILES.json": "4191b13800d48048f8b3b736c888040445d02c31ee7756915c21e011da62f5a1", + "workflow/admit.py": "f0d510b46a5f05b033b13fecb706389ab374b783bd46ef30e7386195d9e56d3e" + }, + "source_commit": "local-joint12-refit393", + "source_head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69" +} diff --git a/research/complex-routing-leaf-fusion/OVERLAP.json b/research/complex-routing-leaf-fusion/OVERLAP.json new file mode 100644 index 0000000000..d6ea92f4c7 --- /dev/null +++ b/research/complex-routing-leaf-fusion/OVERLAP.json @@ -0,0 +1,55 @@ +{ + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-15T20:50:51.799511+00:00", + "terms": [ + "routing", + "leaf", + "H2", + "bootstrap", + "2751", + "2733", + "refit" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T20:48:19.409017+00:00", + "complete_pagination": true, + "records": 711 + }, + "discussions": { + "fetched_at": "2026-10-15T20:50:51.632152+00:00", + "complete_pagination": true, + "records": 1400 + } + }, + "local_records": 1961, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 979, + "reviewed_distinctions": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2751", + "head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "finding": "Latest twelve-source words retain the old rank-six frame at B1151. This package composes the credited earlier refit and validates full native/outer admission." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2733", + "head": "a63c55ff56aaa8645d64d1162d1f017b59ded42a", + "finding": "Credited rank-five refit on a different predecessor word at B1149; not new authorship of the refit." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2755", + "finding": "Native replay acceleration, not a changed paid leaf profile." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319", + "finding": "BIT caller, control and numerical storage work; does not supply this changed binding complex paid moment." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2399", + "finding": "Conditional fast-callee substitution already overlaps an initial BIT target; not replicated here." + } + ], + "source_heads_checked_at_utc": "2026-10-15T20:48:00Z", + "decision": "No duplicate composition found in the inspected metadata and relevant source words. Metadata is not a novelty certificate." +} diff --git a/research/complex-routing-leaf-fusion/PACKING-CAP.json b/research/complex-routing-leaf-fusion/PACKING-CAP.json new file mode 100644 index 0000000000..c7bedd3bf6 --- /dev/null +++ b/research/complex-routing-leaf-fusion/PACKING-CAP.json @@ -0,0 +1,25 @@ +{ + "status": "PASS_FIXED_WORD_PACKING_CEILING", + "source_sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", + "local_per_call": { + "1": "2364", + "2": "647", + "3": "297", + "4": "120", + "5": "26", + "8": "8" + }, + "dimension": 73, + "families": 896, + "stages": 9, + "centre_rank_per_call": 64, + "max_idle_rank": 51, + "complex_cap_bracket": [ + "875246617611/500000000000000", + "1750493235223/1000000000000000" + ], + "complex_cap_upper_decimal": "0.001750493235223", + "realized_fraction_lower": "171725697346700230827/175049323522300000000", + "realized_fraction_decimal": "0.98101320182950399363412598930700232291074148709344", + "scope": "Fixed joint-twelve local word and hosted nine-stage coverage law; all remaining mass is relaxed to fractional rank51 children. This generic coverage-law ceiling is weaker than a window-aware packing or lattice bound. It does not certify or import the predecessor advertised lattice ceiling. It bounds this complex model, not different words or coverage laws. Modern outer admission is separate; no historical a/(1+a) conversion is used." +} diff --git a/research/complex-routing-leaf-fusion/PATCH.json b/research/complex-routing-leaf-fusion/PATCH.json new file mode 100644 index 0000000000..96a2f040c3 --- /dev/null +++ b/research/complex-routing-leaf-fusion/PATCH.json @@ -0,0 +1,111 @@ +{ + "status": "EXACT_CREDITED_FRAME_REFIT_COMPOSITION", + "source_head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "refit_head": "a63c55ff56aaa8645d64d1162d1f017b59ded42a", + "providers": { + "base": { + "source_sha256": "ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a", + "canonical_source_sha256": "f01476ff54463854b4bf0d76ab8880335d4352d2c9835a3f9e04f861833f3a0c", + "canonical_result_sha256": "af1a684d3ae4a6fb7f8709a3ff5a84e4449e10a97f5b415f5733016cab9997c4", + "section": "B", + "index": 1151, + "old": [ + "add", + 393, + 515, + 1, + 1, + [ + 259, + 132, + 66, + 36, + 16, + 9 + ] + ], + "new": [ + "add", + 393, + 515, + 1, + 1, + [ + 259, + 148, + 66, + 36, + 9 + ] + ], + "local_profile": { + "1": 2364, + "2": 647, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + } + }, + "extra": { + "source_sha256": "1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127", + "canonical_source_sha256": "4c29482885c1a189186c4641bfe34b8a95936f5536ac607ffbb1a9f17d94800e", + "canonical_result_sha256": "d2c596ce4aecf9af92f294bbc1d7e9450cf83b9d80dfe347faa6be849d7f6cbc", + "section": "B", + "index": 1151, + "old": [ + "add", + 393, + 515, + 1, + 1, + [ + 259, + 132, + 66, + 36, + 16, + 9 + ] + ], + "new": [ + "add", + 393, + 515, + 1, + 1, + [ + 259, + 148, + 66, + 36, + 9 + ] + ], + "local_profile": { + "1": 2364, + "2": 647, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + } + } + }, + "global_delta": { + "1": -1332, + "2": 666 + }, + "global_profile": { + "1": 1591740, + "2": 430902, + "3": 204396, + "4": 79920, + "5": 22532, + "8": 5328, + "32": 1, + "48": 26558 + }, + "source_refit_authorship": "Marius-Paul Dumitrean PR2733; joint twelve-source recovery Tekalign PR2751", + "scope": "Generator only; independent algebra/frame checks and native/global/outer replay remain separate." +} diff --git a/research/complex-routing-leaf-fusion/PREDECESSOR.json b/research/complex-routing-leaf-fusion/PREDECESSOR.json new file mode 100644 index 0000000000..035f363968 --- /dev/null +++ b/research/complex-routing-leaf-fusion/PREDECESSOR.json @@ -0,0 +1,92 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "pr": 2751, + "head": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "root": "vendor/pr2751", + "files": { + "independent_local.py": { + "sha256": "ee1faab70095fa312fc61d375ddf015b76104cb1a542ae7876a149e7999faa20", + "git_blob": "e0b556adc3d05c8f97e94992e0f872916154202d" + }, + "independent_owners.py": { + "sha256": "4e0785a659b4a6516581f15476c054de1581aa4b3763ce45b1fd20e45c2bb5af", + "git_blob": "93270b725a4efd56b283b02f9abf7a5d0e66c55f" + }, + "composition.py": { + "sha256": "f202f8ce9730b778c9ee1213d63d444d117df5ff7d47933037a924723a37e3f4", + "git_blob": "bb455e907ddf8227cb5c8062825540eda219ba17" + }, + "exact_moment.py": { + "sha256": "f170292f7983773d4f142afdac4677c1615fb7b781dbabf395200aea886dcade", + "git_blob": "30dc8aa22939ea377d893462a863bc7c37b4e210" + }, + "PROFILE.json": { + "sha256": "36e76f32570bac074cf70a6076b7c54e6d5b0fc3b505f404bc58fd02abf7967d", + "git_blob": "080d9e165dbc951c9e8d3eb027bf2b187e932c5d" + }, + "CLAIM.json": { + "sha256": "78e99222196fca8b74a895b9e2db40a0e4afd1d69cd4fb52f38bfb157bac2438", + "git_blob": "48ad23a430def28e485ee311ac92828ac9664a0c" + }, + "README.md": { + "sha256": "d8501fbc11b3dc87fc618122c83f10a56cd4457c7abdab792e2f9506bab4666e", + "git_blob": "77ab0d3121069a8aa365bf0f6c35ee8e5ac15ac8" + }, + "PROOF.md": { + "sha256": "6ecefda5d853e3ede1ee06aab08de24dfde960d98178a71844340ed86ae0d9b9", + "git_blob": "d2b1a96ba8ea6f20e87e12cf2817e0c3ce4c5f30" + }, + "SOURCE-NOTICE": { + "sha256": "ee0c73ca35877aad0e0b6adc560a3881cb82276dba4cf2d4fc58cd19e57cc420", + "git_blob": "380e979f0e84e00a22bd890615d87cc4684ad740" + }, + "LICENSE": { + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + }, + "inputs/WORD-base.json.gz": { + "sha256": "ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a", + "git_blob": "f1fc67a6eaf4bcc5dfa852b448aa2659070fa5f8" + }, + "inputs/WORD-extra.json.gz": { + "sha256": "1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127", + "git_blob": "f06e80c4dddb9741d0051cb85a57d356e673f687" + }, + "inputs/FILL.json.gz": { + "sha256": "9ce94578640b4927cb9c73244692b1f79ac2999179d309f6bf0c015c06f7a2f1", + "git_blob": "17129e917b31b15625c53181d303b68e17ffed55" + }, + "inputs/ORDER.json": { + "sha256": "129e791d5b45c279443ff9e1edef5ac33d5abc51717ecbae8265abea5c247ae7", + "git_blob": "c202d6ec222a257a64b2017eb1bbb0f9d2682669" + }, + "inputs/PROVIDERS.json": { + "sha256": "ec4802a33c0e1d41369da77b19b9b783dc812b2d3246e096fee13d29f226dd66", + "git_blob": "26be26b6d25be67327ae77623c2eaa0a9fe463dc" + }, + "inputs/DISPATCH.json.gz": { + "sha256": "14fe756dcac93a0f3b2b7f38ba7b998dec89d56d5171b691af4fae45e5d83d11", + "git_blob": "4f4c2138d6be71dc649b8ee746385f059c242f21" + }, + "inputs/PLAN.json.gz": { + "sha256": "afb3c5c8134fc2cfce0b50a21758490c225574994b2c3c5161e53e2355acc6fa", + "git_blob": "973f576bccc4b8021bfa9b4fff815b0949fe5932" + }, + "inputs/GLOBAL-TEMPLATE.json.gz": { + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e" + }, + "inputs/SOURCE-FILL.json.gz": { + "sha256": "dc96598624ee49d368e1130ec2148734be0bbc68402cc181e1f02ae9ca8e3d06", + "git_blob": "4a0d605902453ca2eb8bb2e318274022c136ab81" + }, + "inputs/SOURCE-ORDER.json": { + "sha256": "aa7c53c188c90fd74421a804f4c6fb13aa1187c06dbac51fa147830a40e00667", + "git_blob": "7141bd58cc465e28f0189345713ddd366c814ca4" + }, + "inputs/SOURCE-PROVIDERS.json": { + "sha256": "d8d90c3b906c66874f9fe07df67be24e53f3f3f9146565b56a272548108327b7", + "git_blob": "d49a003505049499afb213c09e1011cb511ebbcc" + } + } +} diff --git a/research/complex-routing-leaf-fusion/PROFILE.json b/research/complex-routing-leaf-fusion/PROFILE.json new file mode 100644 index 0000000000..5bd9ded8e3 --- /dev/null +++ b/research/complex-routing-leaf-fusion/PROFILE.json @@ -0,0 +1,10 @@ +{ + "1": 1591740, + "2": 430902, + "3": 204396, + "4": 79920, + "5": 22532, + "8": 5328, + "32": 1, + "48": 26558 +} diff --git a/research/complex-routing-leaf-fusion/PROOF.md b/research/complex-routing-leaf-fusion/PROOF.md new file mode 100644 index 0000000000..ae74069fb0 --- /dev/null +++ b/research/complex-routing-leaf-fusion/PROOF.md @@ -0,0 +1,208 @@ +# A credited frame refit on the joint twelve-source recovery word + +This construction composes Marius-Paul Dumitrean's one-gate refit from +[PR2733](https://github.com/CrocSwap/integer-mult-bounds/pull/2733), head +`a63c55ff56aaa8645d64d1162d1f017b59ded42a`, with Tekalign's joint twelve-source +recovery from [PR2751](https://github.com/CrocSwap/integer-mult-bounds/pull/2751), +head `4cfbb0cc8314d7fb4e8e754545a49a42eb590a69`. The refit is predecessor work; +the new result is its valid composition with the changed recovery word and +the resulting complete invoice. No new scalar identity or refit mechanism +is claimed. + +The two source words do not contain this refit. Their unique gate +`393 += 515` is B1151, with zero-based indexing, in both providers. PR2733 +performs the corresponding edit at B1149 in its different word. Matching a +register pair is not enough to justify composition: the proof below checks +the actual preceding and following frames in the PR2751 words. The local +symbolic checks also retain the changed source recoveries and dirty-input +corrections. + +## Exact changed gate and its legal frames + +Frames are binary subspaces of `F_2^9`, encoded by the listed integer vectors. +Their use in the native complex construction retains the predecessor's +common-label, realization and transport contracts. Let + +``` +P = span(407,66,36,9), dim P = 4, +N = span(259,148,66,36,9), dim N = 5, +O = span(259,132,66,36,16,9), dim O = 6. +``` + +At B1151 the current frame of register 393 is P and the current frame of +register 515 is N. The existing gate executes at O. Replace that gate by + +``` +['add',393,515,1,1,[259,148,66,36,9]]. +``` + +Both operands can reach N: `407 = 259 xor 148` proves `P <= N`, and +`148 = 132 xor 16` gives `N < O`. Each operand's next touched frame has +dimension 7 and contains O. Explicitly they are + +``` +Q393 = span(256,132,65,36,16,9,3), +Q515 = span(259,128,66,32,16,9,4). +``` + +Consequently the smaller gate frame still lies between both preceding and +following frames. Every other gate frame, start frame, final frame, warp +entrance/exit, target level and centre frame is identical. This is a legal +monotone frame assignment under the inherited calculus. It does not cross +a warp or alter a private-buffer lifetime. + +The scalar gate, coefficient and order are identical. Thus the formal +noncommuting-operator word is unchanged, including all source recoveries, +anticipatory dirty-input corrections and inverse cleanup. The physical +realization of a scalar operation at a legal common frame is an inherited +contract, not a consequence of binary subspace containment alone. The +independent replay checks the complete arbitrary-input maps in both forward +and dual orientations and checks all cleanup operations; native phase and +wrapper replay remains a separate evidence layer. + +## Complete local and global paid change + +Only the following two frame paths change: + +| Register | Source path | Composed path | Paid ranks | +| --- | --- | --- | --- | +| 393 | 4 -> 6 -> 7 | 4 -> 5 -> 7 | `(2,1)` becomes `(1,2)` | +| 515 | 5 -> 6 -> 7 | 5 -> 5 -> 7 | `(1,1)` becomes `(0,2)` | + +Zero-rank transitions require no child. Register 393's histogram is +unchanged, while register 515 replaces two rank-one children by one rank-two +child. The local change is therefore exactly `H2 - 2H1`, with unchanged +rank mass. Both providers have the new local profile + +``` +{1:2364, 2:647, 3:297, 4:120, 5:26, 8:8}. +``` + +There remain 415 helpers and 72 private buffers per local word. Entrances, +exits, residual widths and chronological owner lifetimes are unchanged. +The source allocation has 666 call equivalents, so the complete change is +`666*(H2-2H1)`. Retaining every source idle remainder gives + +``` +H = {1:1591740, 2:430902, 3:204396, 4:79920, + 5:22532, 8:5328, 32:1, 48:26558}. +``` + +Its rank mass is 4,816,512. The dimension remains 73, live stock 66,304 and +physical stock 66,801. All 276,390 owner-role reservations remain part of the +construction. Their reuse is justified by the unchanged allocation inputs +and residual interfaces, and checked by the independent owner replay. It is +not permission to drop hosting, stock or other invoice terms. + +No scalar or adapter is added. The mathematical operation count changes +because a recursive frame transition is replaced, not because an additive +implementation constant is smaller. Native generation and the complete +finite invoice accept the changed transition and its phases; the recorded +full release checks this separately from the local proof. + +## Strict moment improvement and certified endpoint + +For saving `0=1 it writes x=2^k y with 1<=y<2 and uses + +``` +log(y) = 2 sum_(j>=0) z^(2j+1)/(2j+1), z=(y-1)/(y+1). +``` + +After 36 terms the positive remainder is at most +`2 z^73/[73(1-z^2)]`. Scaling by k gives exact lower/upper logarithm +enclosures. The argument `a log(73/r)` is less than 1/100 in the checker +domain. Its exponential is bounded by the degree 20 Taylor polynomial +and the tail `next_term/(1-x/22)`. Positive weights preserve interval +orientation. All comparisons use rational arithmetic; fixed-point +dyadic rounding is only a compact outward representation of the resulting +slacks. + +The checker proves `M_new(L)<1 0, "positive integer multiplicity") + out[rank] = value + return out + + +@lru_cache(None) +def logarithm(x): + """Rational enclosure of log(x), x>=1, using 36 positive atanh terms.""" + need(x >= 1, "logarithm input") + exponent = 0 + reduced = x + while reduced >= 2: + reduced /= 2 + exponent += 1 + + def core(y): + z = (y-1)/(y+1) + need(0 <= z <= Q(1, 3), "atanh reduction") + lo = 2*sum((z**(2*j+1)/Q(2*j+1) for j in range(36)), Q(0)) + tail = 2*z**73/(73*(1-z*z)) + return lo, lo+tail + + lo, hi = core(reduced) + two_lo, two_hi = core(Q(2)) + return lo+exponent*two_lo, hi+exponent*two_hi + + +def exponential(x): + """Positive Taylor polynomial through degree 20 plus a geometric tail.""" + need(0 <= x < Q(1, 100), "small exponential input") + term = total = Q(1) + for degree in range(1, 21): + term = term*x/degree + total += term + next_term = term*x/21 + tail = next_term/(1-x/22) + return total, total+tail + + +def moment(histogram, saving, live=LIVE): + need(type(live) is int and live == LIVE, "source-bound live normalization") + need(Q(0) < saving < Q(1, 500), "certified saving domain") + lo = hi = Q(0) + for rank, count in sorted(histogram.items()): + log_lo, log_hi = logarithm(Q(DIMENSION, rank)) + exp_lo, _ = exponential(saving*log_lo) + _, exp_hi = exponential(saving*log_hi) + weight = Q(count*rank, DIMENSION*live) + lo += weight*exp_lo + hi += weight*exp_hi + return lo, hi + + +def floor(x): + return x.numerator//x.denominator + + +def dyadic(lo, hi): + """Small exact outward display; acceptance uses the full rational values.""" + return {"lower_numerator": floor(lo*SCALE), + "upper_numerator": -floor(-hi*SCALE), "denominator": SCALE} + + +def require_bracket(histogram, low, high): + need(low < high, "strictly ordered root endpoints") + a, b = moment(histogram, low) + c, d = moment(histogram, high) + need(b < 1 < c, "strict adjacent root bracket") + return {"lower_endpoint": str(low), "upper_endpoint": str(high), + "lower_moment_minus_one": dyadic(a-1, b-1), + "upper_moment_minus_one": dyadic(c-1, d-1)} + + +def check(candidate_raw, source_raw, claim): + candidate, source = profile(candidate_raw), profile(source_raw) + need(sum(r*n for r, n in source.items()) == MASS, "source paid mass") + expected = dict(source) + expected[1] -= 2*CALLS + expected[2] += CALLS + need(candidate == expected, "complete 666-call H2-minus-2H1 invoice") + need(sum(r*n for r, n in candidate.items()) == MASS, "candidate paid mass") + need(Q(claim["complex_lower"]) == LOW and Q(claim["complex_upper"]) == HIGH, + "claim root endpoints") + need(Q(claim["kappa"]) == KAPPA, "conditional modern outer target") + need(profile(claim["profile"]) == candidate, "claim full profile") + bracket = require_bracket(candidate, LOW, HIGH) + source_lo, source_hi = moment(source, LOW) + need(source_lo > 1, "unchanged source does not certify the new endpoint") + # An exact sign comparison is independent of the transcendental engine: + # 0 0, 'enabled assertions and positive jobs required') + versions = {} + for name in ('numpy', 'sympy', 'scipy', 'mpmath'): + try: + versions[name] = str(importlib.import_module(name).__version__) + except ImportError as exc: + raise RuntimeError('install requirements.txt in this Python environment before full replay') from exc + need(versions['sympy'] == '1.14.0', 'pinned predecessor evidence requires sympy==1.14.0') + work = a.work.resolve() + need(not work.exists() and not work.is_relative_to(REPOSITORY), 'fresh external work required') + for path in (a.source, a.composition_source, a.prepared_native_cache): + need(path is None or (path.is_dir() and not work.is_relative_to(path.resolve())), 'input/work separation') + config, claim = read(HERE / 'FULL-REPLAY-PINS.json'), read(HERE / 'CLAIM.json') + reuse = read(HERE / 'evidence/NATIVE-RECEIPT.json') if a.prepared_native_cache else None + work.mkdir(parents=True) + composition = work / 'composition' + composition.mkdir() + for name, expected in config['files'].items(): + safe(name) + body = ((a.composition_source / name).read_bytes() if a.composition_source + else download(config['base_url'] + quote(name, safe='/'), expected)) + need(hashlib.sha256(body).hexdigest() == expected, 'composition source bytes: ' + name) + destination = composition / name + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(body) + pins = read(composition / 'SOURCE-FILES.json') + env = dict(os.environ, PYTHONDONTWRITEBYTECODE='1', PYTHONUTF8='1', PYTHONINTMAXSTRDIGITS='0', + OPENBLAS_NUM_THREADS='1', OMP_NUM_THREADS='1') + for name in ('PYTHONOPTIMIZE', 'WITNESS_SPEC', 'WITNESS_DISCOVER', 'WITNESS_RECORD'): + env.pop(name, None) + stages, lock = [], threading.Lock() + started = time.monotonic() + + def run(name, script, *args): + begin = time.monotonic() + log = work / (name + '.log') + command = [sys.executable, '-B', str(script), *map(str, args)] + with log.open('w') as output: + result = subprocess.run(command, env=env, cwd=work, stdin=subprocess.DEVNULL, + stdout=output, stderr=subprocess.STDOUT) + with lock: + stages.append(dict(name=name, command=command, exit_code=result.returncode, + script_sha256=sha(script), seconds=time.monotonic()-begin, log_sha256=sha(log))) + write(work / 'STAGES.json', stages) + need(result.returncode == 0, 'failed ' + name + '; see ' + str(log)) + print('PASS', name, flush=True) + + run('literal-review', HERE / 'verify.py') + source = work / 'source' + source_copy(a.source.resolve() if a.source else None, source, pins, a.jobs) + overlay = read(composition / 'OVERLAY-PINS.json') + need(sha(source/'MANIFEST.json') == overlay['original_manifest_sha256'], 'overlay base manifest') + need(sha(composition/'DERIVATIVE-OVERLAY.tar.gz') == overlay['archive_sha256'], 'overlay archive') + with tarfile.open(composition/'DERIVATIVE-OVERLAY.tar.gz') as archive: + members=archive.getmembers() + need(set(m.name for m in members)==set(overlay['files']) and len(members)==len(overlay['files']), 'exact overlay paths') + for member in members: + safe(member.name);need(member.isfile(), 'regular overlay file') + body=archive.extractfile(member).read() + need(hashlib.sha256(body).hexdigest()==overlay['files'][member.name], 'overlay member hash') + (source/member.name).write_bytes(body) + need(sha(source/'MANIFEST.json')==overlay['derived_manifest_sha256'] and + tree(source,('MANIFEST.json',))==read(source/'MANIFEST.json'), 'complete derived source tree') + changes = derive_runtime(source, HERE) + need(sha(source/'MANIFEST.json') == config['derived_manifest_sha256'] + and tree(source, ('MANIFEST.json',)) == read(source/'MANIFEST.json'), 'complete refit source tree') + write(work/'DERIVATION.json', changes) + pins=dict(pins,commit=config['source_commit'],manifest_sha256=config['derived_manifest_sha256']) + # Only source bindings and the strict predecessor comparison change in the + # authenticated admission driver. Its physical costs and controls remain. + admission = (composition/'workflow/admit.py').read_text() + edits = [("SOURCE_COMMIT = 'local-joint12-pr2733'", "SOURCE_COMMIT = " + repr(config['source_commit'])), + ("SOURCE_MANIFEST = '7980dbde79b63de4093cde89d1564a18c6bf16a2e35d810e38cf9797fe09e0cf'", + "SOURCE_MANIFEST = " + repr(config['derived_manifest_sha256'])), + ("previous = Q('0.0017161404259974415161889999999999999999999998999999999999999999999999')", + "previous = Q(" + repr(read(HERE/'vendor/pr2751/CLAIM.json')['kappa']) + ")")] + for before, after in edits: + need(admission.count(before) == 1, 'exact admission patch preimage') + admission = admission.replace(before, after) + (work/'admit.py').write_text(admission) + write(work/'ADMISSION-CHANGES.json', edits) + + cache = work / 'native-cache' + if a.prepared_native_cache: + need(tree(a.prepared_native_cache.resolve()) == reuse['cache_files'], 'published complete cache pins') + shutil.copytree(a.prepared_native_cache.resolve(), cache) + native_receipt = reuse + else: + cache.mkdir() + layout = work / 'retained-layout' + layout.mkdir() + old = source / 'vendor/pr1297' + with tarfile.open(old / 'upstream-layout.tar.gz') as archive: + need(all(m.isfile() and not Path(m.name).is_absolute() and '..' not in Path(m.name).parts + for m in archive.getmembers()), 'retained archive paths') + archive.extractall(layout, filter='data') + retained_driver = layout / 'joint1148-round45/source/research/k8-eight-ends/replay_native.py' + words = {'base': source / 'new/borrow/words/BORROW-WORD-43base.json.gz', + 'extra': source / 'new/borrow/words/BORROW-WORD-43extra.json.gz', + 'retained-base': old / 'gauge44-word.json.gz', 'retained-extra': old / 'extra-word.json.gz'} + + def fresh_native(tag): + word = words[tag] + entry = cache / sha(word) + script = retained_driver if tag.startswith('retained-') else source / 'new/run_native_borrow.py' + run('native-' + tag, script, word, entry) + bind_native(entry, word) + write(entry / 'CACHE.json', dict(word_sha256=sha(word), files=tree(entry))) + + with ThreadPoolExecutor(max_workers=min(a.jobs, 4)) as pool: + for _ in pool.map(fresh_native, words): + pass + run('retained-parent', old / 'verify.py', '--work', work / 'retained-parent', + '--base-native-from', cache / sha(words['retained-base']), + '--extra-native-from', cache / sha(words['retained-extra'])) + parent = read(work / 'retained-parent/RESULT.json') + need(parent['status'] == 'PASS_GLOBAL_MIXED_X54_FUSIONS_NATIVE_AND_STRICT_ADMISSION' + and parent['kappa'] == read(old / 'CLAIM.json')['kappa'], 'fresh retained parent admission') + pm = sha(old / 'MANIFEST.json') + receipts = cache / '_receipts' / pm + receipts.mkdir(parents=True) + for name in ('RESULT.json', 'STAGES.json'): + shutil.copy2(work / 'retained-parent' / name, receipts / name) + write(receipts / 'RECEIPT.json', dict(schema='parent-receipt/1', vendor_manifest_sha256=pm, + claim_sha256=sha(old / 'CLAIM.json'), words={tag:sha(words['retained-'+tag]) for tag in ('base','extra')}, + files={name:sha(receipts / name) for name in ('RESULT.json','STAGES.json')})) + providers = {tag:dict(word_sha256=sha(words[tag]), complete_native_files=tree(cache / sha(words[tag]), ('CACHE.json',))) + for tag in ('base','extra')} + native_receipt = dict(status='PASS_COMPOSED_FRESH_NATIVE_PROVIDERS_AND_AUTHENTICATED_CACHE', + source_commit=pins['commit'], manifest_sha256=pins['manifest_sha256'], providers=providers, + retained_parent_receipt_sha256=sha(receipts / 'RECEIPT.json'), cache_files=tree(cache)) + write(work / 'NATIVE-RECEIPT.json', native_receipt) + run('complete-admission', work / 'admit.py', '--source', source, + '--fill', HERE / 'vendor/pr2751/inputs/FILL.json.gz', '--order', HERE / 'vendor/pr2751/inputs/ORDER.json', + '--native-cache', cache, '--native-receipt', work / 'NATIVE-RECEIPT.json', + '--work', work / 'admission', '--jobs', a.jobs) + result = read(work / 'admission/RESULT.json') + need(result['status'] == 'PASS_COMPOSED_ORDER_FILL_DERIVATIVE_COMPLETE_RELEASE' + and Q(result['kappa']) == Q(claim['kappa']) and Q(result['complex_lower']) == Q(claim['complex_lower']), + 'published complete claim binding') + need(result['profile'] == {str(k):v for k,v in read(HERE / 'CLAIM.json')['profile'].items()}, 'published complete profile binding') + result.update(status='PASS_T74_JOINT_TWELVE_REFIT_COLD_COMPLETE_RELEASE', explicit_native_cache_reuse=bool(a.prepared_native_cache), + source_files_sha256=sha(composition / 'SOURCE-FILES.json'), native_receipt_sha256=sha(work / 'NATIVE-RECEIPT.json'), + cold_stages=stages, cold_seconds=time.monotonic()-started, + environment=dict(python=platform.python_version(), executable=sys.executable, versions=versions)) + write(work / 'RESULT.json', result) + print(result['status'], result['kappa_decimal'], flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/complex-routing-leaf-fusion/generate.py b/research/complex-routing-leaf-fusion/generate.py new file mode 100644 index 0000000000..b6aeec7004 --- /dev/null +++ b/research/complex-routing-leaf-fusion/generate.py @@ -0,0 +1,39 @@ +#!/usr/bin/env python3 +"""Compose Dumitrean's PR2733 refit with Tekalign's PR2751 joint-twelve word. +Does not certify native/global/outer admission. Outputs an exact word delta. +""" +import argparse,copy,gzip,hashlib,json +from pathlib import Path +SOURCE_HEAD='4cfbb0cc8314d7fb4e8e754545a49a42eb590a69' +REFIT_HEAD='a63c55ff56aaa8645d64d1162d1f017b59ded42a' +PINS={'base':'ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a','extra':'1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127'} +OLD=['add',393,515,1,1,[259,132,66,36,16,9]] +NEW=['add',393,515,1,1,[259,148,66,36,9]] +EXPECTED={'1':2366,'2':646,'3':297,'4':120,'5':26,'8':8} +def need(x,m): + if not x:raise ValueError(m) +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':')).encode() +def patch(w): + need(w['report']['local_profile']==EXPECTED,'Exact source local profile') + sites=[i for i,g in enumerate(w['B']) if g==OLD] + need(sites==[1151],'Exact unique source B1151') + out=copy.deepcopy(w);out['B'][1151]=copy.deepcopy(NEW) + out['report']['local_profile']['1']-=2;out['report']['local_profile']['2']+=1 + return out +if __name__=='__main__': + ap=argparse.ArgumentParser();ap.add_argument('--source',type=Path,required=True);ap.add_argument('--out',type=Path,required=True);a=ap.parse_args() + need(not a.out.exists(),'Output directory must be fresh') + outputs={};receipts={} + for tag,pin in PINS.items(): + raw=(a.source/f'inputs/WORD-{tag}.json.gz').read_bytes();need(hashlib.sha256(raw).hexdigest()==pin,'Source bytes '+tag) + before=json.loads(gzip.decompress(raw));after=patch(before) + outputs[tag]=canonical(after) + receipts[tag]={'source_sha256':pin,'canonical_source_sha256':hashlib.sha256(canonical(before)).hexdigest(),'canonical_result_sha256':hashlib.sha256(outputs[tag]).hexdigest(),'section':'B','index':1151,'old':OLD,'new':NEW,'local_profile':after['report']['local_profile']} + sourceprofile=json.loads((a.source/'PROFILE.json').read_bytes());newprofile=sourceprofile.copy();newprofile['1']-=1332;newprofile['2']+=666 + need(sum(int(r)*n for r,n in newprofile.items())==4816512,'Preserved full paid mass') + a.out.mkdir() + for tag,data in outputs.items():(a.out/f'WORD-{tag}.json.gz').write_bytes(gzip.compress(data,mtime=0)) + receipt={'status':'EXACT_CREDITED_FRAME_REFIT_COMPOSITION','source_head':SOURCE_HEAD,'refit_head':REFIT_HEAD,'providers':receipts,'global_delta':{'1':-1332,'2':666},'global_profile':newprofile,'source_refit_authorship':'Marius-Paul Dumitrean PR2733; joint twelve-source recovery Tekalign PR2751','scope':'Generator only; independent algebra/frame checks and native/global/outer replay remain separate.'} + (a.out/'PATCH.json').write_text(json.dumps(receipt,indent=2)+'\n') + (a.out/'PROFILE.json').write_text(json.dumps(newprofile,indent=2)+'\n') + print(receipt['status']) diff --git a/research/complex-routing-leaf-fusion/independent_check.py b/research/complex-routing-leaf-fusion/independent_check.py new file mode 100644 index 0000000000..8cd75aec6f --- /dev/null +++ b/research/complex-routing-leaf-fusion/independent_check.py @@ -0,0 +1,324 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# David Arias, with substantial OpenAI Codex assistance. +"""Independent literal-word replay for the credited PR2733/PR2751 composition. + +Uses only Python's standard library. No producer, predecessor checker, cached +profile, or native audit is imported. Frames use binary Gaussian elimination; +linear endpoints use sparse rational expressions in free noncommuting warp +symbols. This verifies a finite construction, not the conditional analytic or +fixed-tape assumptions of the complete multiplication theorem. +""" +from __future__ import annotations + +import argparse +from collections import Counter, defaultdict +import copy +from fractions import Fraction +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +OLD_FRAME = [259, 132, 66, 36, 16, 9] +NEW_FRAME = [259, 148, 66, 36, 9] +GATE = 1151 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def normal(vectors): + """Canonical reduced binary row basis, with descending pivots.""" + rows = {} + for vector in vectors: + require(isinstance(vector, int) and 0 <= vector < 512, 'binary coordinate') + for pivot in sorted(rows, reverse=True): + if vector >> pivot & 1: + vector ^= rows[pivot] + if vector: + pivot = vector.bit_length() - 1 + for old in list(rows): + if rows[old] >> pivot & 1: + rows[old] ^= vector + rows[pivot] = vector + return tuple(rows[p] for p in sorted(rows, reverse=True)) + + +def contained(small, large): + return normal((*large, *small)) == large + + +FULL = normal(1 << i for i in range(9)) + + +def image(columns, vector): + value = 0 + for i, column in enumerate(columns): + if vector >> i & 1: + value ^= column + return value + + +def touched(gate): + return gate[1:3] if gate[0] == 'add' else gate[1:2] + + +def endpoints(word): + live = set(range(704)) - set(word['removed']) + start = {r: normal([word['ports'][r]] if r < 112 else + word['start_extra'].get(str(r), [])) for r in live} + finish = {r: FULL for r in live} + for i, port in enumerate(word['ports']): + require(port != 0, 'nonzero target port') + pivot = (port & -port).bit_length() - 1 + finish[112 + i] = normal((1 << j) ^ (((port >> j) & 1) << pivot) + for j in range(9) if j != pivot) + for r, frame in word['helper_final'].items(): + finish[int(r)] = normal(frame) + return start, finish + + +def frame_replay(word): + start, finish = endpoints(word) + current = dict(start) + paid = Counter() + history = defaultdict(list) + + def climb(r, frame, location): + frame = normal(frame) + require(contained(current[r], frame), f'frame inclusion at {location}/{r}') + degree = len(frame) - len(current[r]) + if degree: + paid[degree] += 1 + history[r].append((location, len(current[r]), len(frame))) + current[r] = frame + + def warp(r, op, old, new, location): + columns = word['warps'][abs(op) - 1][2] + require(len(normal(columns)) == 9, f'invertible warp {op}') + old, new = normal(old), normal(new) + require(current[r] == old, f'warp entrance {location}/{r}') + before, after = (old, new) if op > 0 else (new, old) + require(normal(image(columns, v) for v in before) == after, + f'warp transported frame {location}/{r}') + current[r] = new + history[r].append((location, len(old), len(new))) + + def gate(g, location): + if g[0] == 'warp': + warp(*g[1:], location) + else: + require(g[0] in ('add', 'scale'), 'known scalar operation') + for r in touched(g): + climb(r, g[-1], location) + + for i, g in enumerate(word['A']): + gate(g, f'A{i}') + levels = {int(t): normal(vs) for t, vs in word['target_levels'].items()} + require(all(current[112 + t] == levels.get(t, ()) for t in range(112)), + 'all cut target entrances') + # The native central child pays the nested descent once; its other side + # retains the center's start chart for the B-side ascent representation. + for r, frame in zip(word['centers'], word['center_frames']): + previous = normal(frame) + require(current[r] == previous, 'central source entrance') + readers = {levels.get(g[1] - 112, ()) for g in word['cut'] if g[2] == r} + for target in sorted(readers, key=lambda x: (-len(x), x)): + require(contained(target, previous), 'nested central descent') + if len(previous) != len(target): + paid[len(previous) - len(target)] += 1 + previous = target + warps = defaultdict(list) + for op, entry in enumerate(word['warps'], 1): + warps[entry[0]].append((op, entry)) + for i in range(len(word['B']) + 1): + for op, (_, r, _, old, new) in warps[i]: + warp(r, op, old, new, f'warp{op}') + if i < len(word['B']): + gate(word['B'][i], f'B{i}') + for i, g in enumerate(word['restore']): + gate(g, f'restore{i}') + for r in sorted(current): + climb(r, finish[r], 'endpoint') + inventory = Counter(len(finish[r]) - len(start[r]) for r in current if r >= 224) + require(dict(paid) == {int(k): v for k, v in word['report']['local_profile'].items()}, + 'complete paid profile, including endpoint climbs') + require(dict(inventory) == {int(k): v for k, v in word['report']['width_inventory'].items()}, + 'helper endpoint width inventory') + return paid, history + + +def reduced(left, right): + """Multiply free-group words, stored with the newest operation first.""" + result = list(left) + for symbol in right: + if result and result[-1] == -symbol: + result.pop() + else: + result.append(symbol) + return tuple(result) + + +def scalar_replay(word, dual): + live = set(range(704)) - set(word['removed']) + cold = set(map(int, word['helper_final'])) + rows = {r: {(r, ()): Fraction(1)} for r in live} + rows.update({704 + r: {} for r in cold}) + + def add(target, source, coefficient, operator=()): + for (origin, old), value in list(rows[source].items()): + term = (origin, reduced(operator, old)) + total = rows[target].get(term, Fraction(0)) + coefficient * value + if total: + rows[target][term] = total + else: + rows[target].pop(term, None) + + def dual_symbol(symbol): + return (abs(symbol) + 1000) * (1 if symbol > 0 else -1) + + def apply(g): + kind = g[0] + if kind == 'add': + target, source, numerator, denominator = g[1:5] + coefficient = Fraction(numerator, denominator) + require(target != source, 'distinct ADD registers') + if dual: + target, source, coefficient = source, target, -coefficient + add(target, source, coefficient) + elif kind == 'scale': + r, numerator, denominator = g[1:4] + coefficient = Fraction(numerator, denominator) + require(coefficient != 0, 'invertible scalar') + if dual: + coefficient = 1 / coefficient + rows[r] = {term: coefficient * value for term, value in rows[r].items()} + elif kind == 'warp': + r, symbol = g[1:3] + if not dual and 47 <= symbol <= 58: + require(rows[r] == {(r, ()): Fraction(1)}, 'recovered source lender') + if dual: + symbol = dual_symbol(symbol) + rows[r] = {(origin, reduced((symbol,), old)): value + for (origin, old), value in rows[r].items()} + else: + raise ValueError(f'unknown scalar operation {kind}') + + for correction in word['initial_corrections']: + target, source = correction['target'], correction['source'] + coefficient = Fraction(correction['coefficient']) + operator = tuple(correction['operator_word']) + if dual: + target, source, coefficient = source, target, -coefficient + operator = tuple(-dual_symbol(x) for x in reversed(operator)) + add(target, source, coefficient, operator) + for section in ('precondition', 'compensation', 'A', 'cut'): + for g in word[section]: + apply(g) + warps = defaultdict(list) + for op, entry in enumerate(word['warps'], 1): + warps[entry[0]].append(['warp', entry[1], op]) + for i in range(len(word['B']) + 1): + for g in warps[i]: + apply(g) + if i < len(word['B']): + apply(word['B'][i]) + for g in word['restore']: + apply(g) + if not dual: + for r in cold: + require(rows[r] == {(r, ()): Fraction(1)}, 'dirty helper restored before cleanup') + for t in range(112): + require(rows[112 + t] == {(112 + t, ()): Fraction(1), (t, ()): Fraction(1)}, + 'forward target before cleanup') + for g in word['cleanup']: + apply(g) + for r in live: + expected = {(r, ()): Fraction(1)} + if dual and r < 112: + expected[(112 + r, ())] = Fraction(-1) + if not dual and 112 <= r < 224: + expected[(r - 112, ())] = Fraction(1) + require(rows[r] == expected, f'complete {"dual" if dual else "forward"} endpoint {r}') + require(all(not rows[704 + r] for r in cold), 'all cold outputs zero') + + +def check_change(source, candidate): + require(source['B'][GATE] == ['add', 393, 515, 1, 1, OLD_FRAME], 'source refit gate') + require(candidate['B'][GATE] == ['add', 393, 515, 1, 1, NEW_FRAME], 'candidate refit gate') + expected = copy.deepcopy(source) + expected['B'][GATE][-1] = NEW_FRAME + expected['report']['local_profile'] = candidate['report']['local_profile'] + require(expected == candidate, 'only the credited frame and paid profile change') + + +def reject(callback, label): + try: + callback() + except ValueError: + return label + raise ValueError(f'negative control accepted: {label}') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--source', type=Path, default=HERE / 'vendor/pr2751') + parser.add_argument('--candidate', type=Path, default=HERE) + args = parser.parse_args() + source = args.source.resolve() + candidate = args.candidate.resolve() + candidate_inputs = candidate / 'inputs' if (candidate / 'inputs').is_dir() else candidate + result = {'status': 'PASS_INDEPENDENT_CREDITED_FUSION', 'providers': {}} + local_delta = Counter({1: -2, 2: 1}) + for tag in ('base', 'extra'): + old = read(source / f'inputs/WORD-{tag}.json.gz') + new = read(candidate_inputs / f'WORD-{tag}.json.gz') + check_change(old, new) + before, old_history = frame_replay(old) + after, new_history = frame_replay(new) + delta = Counter(after) + delta.subtract(before) + require({r: n for r, n in delta.items() if n} == dict(local_delta), 'exact local fusion charge') + paths = {} + for r, prior in ((393, 4), (515, 5)): + a = old_history[r] + b = new_history[r] + index = next(i for i, entry in enumerate(a) if entry[0] == f'B{GATE}') + require(a[index][1:] == (prior, 6) and a[index + 1][1:] == (6, 7), 'old local path') + require(b[index][1:] == (prior, 5) and b[index + 1][1:] == (5, 7), 'new local path') + paths[str(r)] = {'old': [prior, 6, 7], 'new': [prior, 5, 7]} + scalar_replay(new, False) + scalar_replay(new, True) + bad_frame = copy.deepcopy(new) + bad_frame['B'][GATE][-1] = [1] + omitted = copy.deepcopy(new) + omitted['report']['local_profile']['2'] -= 1 + controls = [reject(lambda: frame_replay(bad_frame), 'invalid frame'), + reject(lambda: check_change(old, old), 'unchanged identity candidate'), + reject(lambda: frame_replay(omitted), 'omitted child charge')] + result['providers'][tag] = {'profile': dict(sorted(after.items())), 'paths': paths, + 'forward': 'PASS', 'dual': 'PASS', 'controls': controls} + order = read(source / 'inputs/ORDER.json') + require(len(order) == len({tuple(x) for x in order}) == 666, '666 distinct provider invocations') + global_old = Counter({int(k): v for k, v in read(source / 'PROFILE.json').items()}) + expected = Counter(global_old) + expected.update({r: 666 * n for r, n in local_delta.items()}) + claimed = {int(k): v for k, v in read(candidate / 'PROFILE.json').items()} + require(dict(expected) == claimed, 'complete global profile includes fusion charge') + require(sum(r * n for r, n in expected.items()) == sum(r * n for r, n in global_old.items()), + 'unchanged global rank mass') + result['global_delta'] = {r: 666 * n for r, n in local_delta.items()} + result['profile'] = claimed + print(json.dumps(result, sort_keys=True, separators=(',', ':'))) + + +if __name__ == '__main__': + main() diff --git a/research/complex-routing-leaf-fusion/inputs/WORD-base.json.gz b/research/complex-routing-leaf-fusion/inputs/WORD-base.json.gz new file mode 100644 index 0000000000..9a49a90965 Binary files /dev/null and b/research/complex-routing-leaf-fusion/inputs/WORD-base.json.gz differ diff --git a/research/complex-routing-leaf-fusion/inputs/WORD-extra.json.gz b/research/complex-routing-leaf-fusion/inputs/WORD-extra.json.gz new file mode 100644 index 0000000000..a3fdc91b1b Binary files /dev/null and b/research/complex-routing-leaf-fusion/inputs/WORD-extra.json.gz differ diff --git a/research/complex-routing-leaf-fusion/packing_cap.py b/research/complex-routing-leaf-fusion/packing_cap.py new file mode 100644 index 0000000000..f73d080920 --- /dev/null +++ b/research/complex-routing-leaf-fusion/packing_cap.py @@ -0,0 +1,60 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Uses Douglas Colkitt's exact ceiling engine (Claude-assisted), pinned unchanged. +# Adapter derived from Tekalign (@tekuuu), with substantial OpenAI Codex assistance. +# Updated for the credited frame composition by David Arias, with Codex assistance. +"""Fixed-word coverage-law ceiling; separate from physical and outer admission.""" +import argparse, hashlib, importlib.util, json, sys +from fractions import Fraction as Q +from decimal import Decimal, localcontext +from pathlib import Path +HERE = Path(__file__).resolve().parent +sys.dont_write_bytecode = True +ENGINE_SHA = "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" +IDLE = {1:17316,3:6594,5:5216,32:1,48:26558} +CANDIDATE = {1:1591740,2:430902,3:204396,4:79920,5:22532,8:5328,32:1,48:26558} +ENDPOINT = Q('0.001717256973467002308270') + +def need(ok, message): + if not ok: + raise ValueError(message) + +def calculate(profile_path=None): + path = HERE / 'vendor/ceiling.py' + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == ENGINE_SHA, 'ceiling source pin') + spec = importlib.util.spec_from_file_location('packing_ceiling', path) + engine = importlib.util.module_from_spec(spec) + exec(compile(raw, str(path), 'exec'), engine.__dict__) + h = {int(r): n for r,n in json.loads((profile_path or HERE/'PROFILE.json').read_text()).items()} + need(h == CANDIDATE and sum(r*n for r,n in h.items()) == 4816512, + 'complete candidate histogram and rank mass') + local = {r: Q(h[r]-IDLE.get(r,0),666) for r in h if h[r] != IDLE.get(r,0)} + need(local == {1:2364,2:647,3:297,4:120,5:26,8:8}, 'complete local profile') + model = engine.model(local,73,896,9,64) + need(model['total_mass']*666 == 4816512 and model['local_mass'] == 5223, 'coverage identity') + lo,hi = engine.ceiling(local,73,896,9,64) + need(engine.relax(local,73,896,9,64,hi)[0] > 1, 'upper cap rejection') + c = Q(json.loads((HERE/'CLAIM.json').read_text())['complex_lower']) + need(c == ENDPOINT, 'certified candidate endpoint') + with localcontext() as ctx: + ctx.prec = 50 + dec = lambda x: str(Decimal(x.numerator)/Decimal(x.denominator)) + return dict(status='PASS_FIXED_WORD_PACKING_CEILING',source_sha256=ENGINE_SHA, + local_per_call={str(r):str(n) for r,n in local.items()}, + dimension=73,families=896,stages=9,centre_rank_per_call=64,max_idle_rank=model['R'], + complex_cap_bracket=[str(lo),str(hi)],complex_cap_upper_decimal=dec(hi), + realized_fraction_lower=str(c/hi),realized_fraction_decimal=dec(c/hi), + scope='Fixed joint-twelve local word and hosted nine-stage coverage law; all remaining mass is relaxed to fractional rank51 children. This generic coverage-law ceiling is weaker than a window-aware packing or lattice bound. It does not certify or import the predecessor advertised lattice ceiling. It bounds this complex model, not different words or coverage laws. Modern outer admission is separate; no historical a/(1+a) conversion is used.') + +def main(): + ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('--output',type=Path) + ap.add_argument('--profile',type=Path,default=HERE/'PROFILE.json');a=ap.parse_args() + result=calculate(a.profile) + if not a.output: + need(result == json.loads((HERE/'PACKING-CAP.json').read_text()), 'packing-cap receipt mismatch') + text=json.dumps(result,indent=2)+'\n' + if a.output: + a.output.parent.mkdir(parents=True,exist_ok=True);a.output.write_text(text) + print(text,end='') +if __name__=='__main__': main() diff --git a/research/complex-routing-leaf-fusion/references/pr2733/CLAIM.json b/research/complex-routing-leaf-fusion/references/pr2733/CLAIM.json new file mode 100644 index 0000000000..4d848d5466 --- /dev/null +++ b/research/complex-routing-leaf-fusion/references/pr2733/CLAIM.json @@ -0,0 +1,81 @@ +{ + "status": "PASS_COMPLETE_CONDITIONAL_ONE_GATE_REFIT", + "kappa": "17162556782301801990819999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017162556782301801990819999999999999999999998999999999999999999999999", + "complex_lower": "858127839115090099541/500000000000000000000000", + "complex_upper": "1716255678230180199083/1000000000000000000000000", + "global_profile": { + "1": 1594404, + "2": 430902, + "3": 204396, + "4": 79920, + "5": 22532, + "7": 2664, + "8": 2664, + "32": 1, + "48": 26558 + }, + "local_profile": { + "1": 2368, + "2": 647, + "3": 297, + "4": 120, + "5": 26, + "7": 4, + "8": 4 + }, + "comparison": { + "pr": 2733, + "head": "2761b52b17590b8cf94f2e410004a8252d5592dc", + "kappa": "17161404259974415161889999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000" + }, + "gain": "115252232738682893/1000000000000000000000000", + "gain_percent": "0.006715781004441807559271426243840475422143424914816497532787219587423584", + "helpers": 415, + "calls": 666, + "roles": 276390, + "private_zero_buffers": 72, + "live": 66304, + "physical": 66801, + "rank_mass": 4816512, + "full_receipt": "evidence/full/RESULT.json", + "full_receipt_sha256": "3960db1a20f225619994cc1207973e73333a67f5d3411679e5e6beeac50155f3", + "source2679_head": "2e2cf56521df8a2b816b2689144765ee00b69a24", + "source2679_manifest_sha256": "db498ed7998397ef00501e037f10678e89ee113d57af4667c5c6978fc42e83ba", + "source2696_head": "5a42add713e09a8798a84d0be7a8276626d9e785", + "candidate_manifest_sha256": "234cd08b5ae55b81f49c68549ec550c62a30a1e43f1c451d4836c12ed0464bd4", + "coverage": { + "current_stages": 18, + "retained_parent_stages": 18, + "strict_steps": 8, + "supplier_inequalities": 47, + "modern_inequalities": 63, + "modern_negative_controls": 17, + "evidence_replays": 19, + "admission_controls": 114, + "bit_controls": 12, + "current_controller_mutations": 25, + "independent_owner_controls": 8, + "geometry_controls": 6, + "prelife_mutations_per_provider": 78, + "alias_mutations_per_provider": 7, + "native_recipe_mutations_per_provider": 13, + "dirty_columns_each_orientation": 639, + "native_operator_count": 65, + "native_physical_classes": 166, + "native_columns_per_class": 512, + "ordinary_sufficient_stages": 37 + }, + "native_and_parent_receipt_reuse": false, + "inherited_parent_geometry_reuse": true, + "selected_main_changed": false, + "human_review": false, + "proof_assistant_verified": false, + "scope": "Finite conditional construction and exact outer inequalities; inherited all-size, machine, analytic and bit assumptions remain.", + "latest_comparison": { + "pr": 2745, + "head": "4f485de05544884fa0f2edf6063bb9259decad30", + "source_claim_sha256": "3dd22facffda276820de211ccbebcdb51296d0dc4544eaf824c0982a0ecce5e6", + "gain": "1152522327386828923986958405456550016704982851526653723338897453235077363137955563484477972014655144849901016224958370736452836874748324552514434252165193760012421558201475515892676178298844377486299355652132598928274405431550684387484094490504115233222418160769653597661174415592502648718377841476158643571134598900661279605763041147288209663739853590127428569334882278938889212770337810458546653024480764824925785522147407275424823833001377673320296666889062633592613879785770048368191481861636732094780186823400433902504245113278482732391124149769505091896493786837649208207668558651234481386694029719550345680934522957309797753657784460928481348591236710504214847910629330174919063157972846674431261560192401805114029748198590019913511051623811552806109170167892566593094174294084194603336817274759327823163922695977936791304886025696668084326690154451196659226458417144622840250124183055368787281008148076829847857564094201109768180780488096807777657169184484992021279602259409827300317883878667085017324762808192221751343057378456623173168825948172507145572284532651946722548662909466595834514472481514320163121897852933619130839360101152609296615510240176415606431571092302394993336965432419668385640052238267408068377690615866558262492318158178988042740245947148176887598870151226232990312997958870741987814513762632060994115232960297459855946600638352674389748474390357380216250942806878273315319080861622070278195001083214726086247355962049517627954677928426461007804566222925742890444925646278000097986723482842830059438431821613379271163950227521549145546610012841272427195397678003980739261847843242838651732112088808713219186384523614303490266301536079946639924174300183433182199128326791309663705250352572052472500320592963559976987565828718953357573936345029060042818347734470556409212902538468198613988536256030024137219735914362231743710581217320176469736039924885335628492652267723187030135732438954485875610869266686567122188440884114974487473429828031068433041203007826614929936141402577750775225940608644167330559212566993748279193328233708010650529289445193333389808571712849037050330033125103779500724923110107063540392910321332440414135582413001243323654896577862616563860835925935586083994714827027565777465019241962321348662814548124062774482527467964077250052105952955692535818463556789085955817556196520698820013289686825895123726521617061431152273697648294580922195333547716210315006486789799911669360718822392333124336078261788309378651120643305379599021565393198057587072784837906397694814384362561357343866759385548898153347483190182690964710964510152026539120933722502448956501934530691560295954628228745536285324141446345868001230240638408221068503976674258798165395942621264009756163768505813981941714313277481457363778096179652001048939892344420799481076606518833289055530698255335185088782882039318915993349797797758940369731095116215929321656051292221291980095202394838218079303112450163917616266815079526837270234785195021223149683812983948470647812041600000000000000000000001000000000000000000000001/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" + } +} diff --git a/research/complex-routing-leaf-fusion/references/pr2733/NOTICE b/research/complex-routing-leaf-fusion/references/pr2733/NOTICE new file mode 100644 index 0000000000..6dacc7b2ce --- /dev/null +++ b/research/complex-routing-leaf-fusion/references/pr2733/NOTICE @@ -0,0 +1,30 @@ +One-gate frame refit of the concentrated source-partner/pre-life composition. +Copyright 2026 Marius-Paul Dumitrean. Apache-2.0. +Substantial OpenAI Codex assistance was used for research, implementation, +orchestration and separately developed checks. No independent human review or +proof-assistant verification is claimed. + +The predecessor concentrated-prelife-composition package and every imported +source retain their original license, NOTICE and AI-assistance disclosures. +This package imports that frozen package rather than duplicating its source. +Mason Hale supplied PR2696 concentrated source partners and independent algebra; +Philippe Van Velzen supplied PR2679 pre-life/refit and PR2559 evacuation; +Jeremy Kothe supplied PR2588 comparison words and PR2673 order/allocation; +zxv supplied PR2530 source-partner recovery/owner flows; themilkman216 PR2621 +priority scheduling; Tekalign PR2436 lifted-target compensation; Rohan Arun +owner work. Douglas Colkitt's exact interval primitives retain their notices. +The retained native, bit and outer source lineage remains authoritative. + +Frozen inherited patch metadata contains an early incorrect author label: +PR2679 is Philippe Van Velzen's contribution, not Jeremy Kothe's. Source bytes +are preserved, and SOURCE-HEADS.json and this notice correct the attribution. + +check_admission.py, combined_adapt.py and replay_engine.py are derived from the +same author's prior PR2733 package. REPLAY-DERIVATION.patch records the scientific +engine/adapter changes. The new gate/frame witness and complete-cost comparison +are in PROOF.md. + +Jeremy Kothe's concurrent PR2745 independently composes the same words, gives +an equally priced alternate fill and refines the exact endpoint grid. Its full +claim is retained with exact source pins for comparison; its inputs do not add +a further paid-profile improvement to the B1149 candidate. diff --git a/research/complex-routing-leaf-fusion/references/pr2733/PROOF.md b/research/complex-routing-leaf-fusion/references/pr2733/PROOF.md new file mode 100644 index 0000000000..452212aa89 --- /dev/null +++ b/research/complex-routing-leaf-fusion/references/pr2733/PROOF.md @@ -0,0 +1,102 @@ +# One legal frame change and its exact paid gain + +The source is the complete frozen PR2733 composition, pinned by its original +published head and artifact manifest in `SOURCE-HEADS.json`. Both orientation +providers receive precisely the same change at B gate 1149: + +``` +['add',393,515,1,1,[259,132,66,36,16,9]] + -> [259,148,66,36,9] +``` + +The first five gate fields stay fixed. Only the common frame changes from rank +six to rank five. The complete scalar word, 112 source and 112 target roles, +entrances, final frames, operator words, precondition/compensation, 36 +anticipatory corrections, all warps and inverse cleanup remain identical. +`verify_refit.py` checks complete decoded-word equality after this declared edit +and the corresponding report update, not merely matching rank histograms. + +## Legal frame witness + +For register 393 the preceding B gate is 1141, with frame +`[407,66,36,9]` of rank four. Its following B gate is 1790, with rank-seven frame +`[256,132,65,36,16,9,3]`. For register 515 the preceding B gate is 894, with frame +`[259,148,66,36,9]` of rank five. Its following B gate is 1778, with rank-seven +frame `[259,128,66,32,16,9,4]`. There is no intervening warp between each +register's respective neighboring occurrences. Register 393's warp at 1130 +precedes gate 1141 and is unchanged. + +Over F2 the new frame contains both incoming subspaces and is contained in both +outgoing subspaces. It is a proper subspace of the old common frame. Thus the +unchanged elementary addition is legal, and all four adjacent climbs remain +legal. Their old bill is `H2+3H1`; their new bill is `2H2+H1`. The exact local +change is therefore `H2-2H1`. + +The independent checker computes the complete frame invoice, all arbitrary-input +free-operator rows in the forward and dual orientations, and literal inverse +cleanup. A zero frame and a changed coefficient sign are rejected separately +for each provider. Native physical recipes and phases are additional obligations +of the complete cold replay; they are not inferred from the free-operator check. + +## Complete cost and owner interface + +The resulting local profile is +`{1:2368,2:647,3:297,4:120,5:26,7:4,8:4}`. Since every entry and exit is unchanged, +so is every helper width. The original literal owner fill/order applies without +any remapping, and every one of the 276,390 roles remains charged. There are 415 +helpers per call and 72 private FULL buffers. Physical stock remains +`66304+415+8+72+2=66801`. Across 666 calls, the global profile changes only by +`666*(H2-2H1)` to + +``` +{1:1594404,2:430902,3:204396,4:79920,5:22532,7:2664,8:2664,32:1,48:26558}. +``` + +Its rank mass is still 4,816,512. For native normalization +`M(b)=sum_r H_r*(r/73)^(1-b)/66304`, the exact moment change is + +``` +Delta M(b) = 666*73^(b-1)/66304*(2^(1-b)-2) < 0, 0 < b < 1. +``` + +This proves native moment dominance throughout that interval. It does not, by +itself, prove any unexamined conservative surcharge or whole outer exponent. +Those are rederived in the fresh complete replay and bound to `CLAIM.json`. + +## Chained reconstruction and checker adaptation + +`generate.py` authenticates the complete frozen predecessor packages before and +after reconstructing both words. It appends the new refit to the original +B894 refit stage. The following alias653 patch replaces a complete B list, so +that patch is regenerated as well; otherwise it would silently restore the old +B1149 frame. Both final decoded words must match the committed expected words. +Compressed regeneration is compared by complete decoded payload, while frozen +source bytes retain exact hashes. + +`REPLAY-DERIVATION.patch` describes the changes from the previous composition +engine and adapter. In addition to the three already declared candidate checker +adaptations, `new/rebuild_borrow.py` now requires precisely the original B894 +refit and this B1149 refit. It checks the exact original and resulting B1149 gate, +the original B894 gate and dimension drop, and equality of every other B gate. +The resulting four modified derivative checker files are individually hash-bound; +other frozen proof/checker Python remains unchanged. Eight deliberate extra or +incorrect edits were independently rejected. Frozen upstream packages are never +edited in place. + +## Scope of the endpoint ceiling and remaining obligations + +The exact rational dual/lattice ceiling applies only to this fixed local profile, +415-helper width inventory, 666 calls and original bin multiset. It relaxes +window/family constraints, so covers every packing order under those premises. +A changed local word/profile, inventory, warp or bin geometry requires a new +bound. The finite 914-closure screen is not an all-frame optimum. + +All-size machine/compiler and common-label realization, sequential physical +borrowing/hosting/routing, uniform precision and fixed tape, exact recovery and +analytic transfer, native recurrence corrections, the bit supplier and modern +outer phase-cell/radix/prime-padding assumptions remain inherited. Finite receipt +checks do not establish those uniform hypotheses or an unconditional integer +multiplication theorem. The selected repository result is unchanged. + +Marius-Paul Dumitrean, with substantial OpenAI Codex assistance. Apache-2.0. +Source attribution and source-specific notices are retained in `NOTICE`. diff --git a/research/complex-routing-leaf-fusion/requirements.txt b/research/complex-routing-leaf-fusion/requirements.txt new file mode 100644 index 0000000000..816d0c8e91 --- /dev/null +++ b/research/complex-routing-leaf-fusion/requirements.txt @@ -0,0 +1,4 @@ +numpy==2.5.4 +sympy==1.14.0 +scipy==1.18.1 +mpmath==1.3.0 diff --git a/research/complex-routing-leaf-fusion/test_integrity.py b/research/complex-routing-leaf-fusion/test_integrity.py new file mode 100644 index 0000000000..114f85953b --- /dev/null +++ b/research/complex-routing-leaf-fusion/test_integrity.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Git-free read-only replay and fail-closed public-entrypoint controls.""" +import gzip +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def inventory(root): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + + +def call(package, args, expected_code=0, reason=None): + env = dict(os.environ, PYTHONDONTWRITEBYTECODE='1', PATH='') + env.pop('PYTHONOPTIMIZE', None) + process = subprocess.run([sys.executable, '-I', '-B', *args], cwd=package.parent, + env=env, capture_output=True, text=True, timeout=220) + if expected_code == 0: + need(process.returncode == 0, 'public replay failed: ' + process.stderr[-2000:]) + else: + need(process.returncode != 0, 'public entry accepted corruption') + need(reason in process.stderr + process.stdout, 'wrong failure reason: ' + process.stderr[-2000:]) + + +def main(): + with tempfile.TemporaryDirectory(prefix='routing-leaf-export-') as directory: + target = Path(directory) / 'relocated-package' + shutil.copytree(HERE, target, ignore=shutil.ignore_patterns('__pycache__')) + baseline = inventory(target) + call(target, [str(target/'verify.py')]) + need(inventory(target) == baseline, 'successful verification wrote package files') + # A valid source comment change is still an unauthenticated input change. + path = target/'vendor/pr2751/independent_local.py' + original = path.read_bytes() + path.write_bytes(original+b'\n# unauthenticated change\n') + call(target, [str(target/'verify.py')], 1, 'predecessor SHA256') + path.write_bytes(original) + # Keep the profitable claimed profile but remove the actual frame edit. + path = target/'inputs/WORD-base.json.gz' + original = path.read_bytes() + value = json.loads(gzip.decompress(original)) + value['B'][1151][-1] = [259,132,66,36,16,9] + path.write_bytes(gzip.compress(json.dumps(value).encode(), mtime=0)) + call(target, [str(target/'verify.py')], 1, 'complete generated word equality') + path.write_bytes(original) + # JSON numeric equality must not conflate an integer receipt with float. + path = target/'RESULT.json' + original = path.read_bytes() + value = json.loads(original) + value['calls'] = float(value['calls']) + path.write_text(json.dumps(value)) + call(target, [str(target/'verify.py')], 1, 'complete typed RESULT.json equality') + path.write_bytes(original) + call(target, ['-O', str(target/'verify.py')], 1, 'run without -O') + out = Path(directory)/'existing-output' + out.mkdir() + (out/'sentinel').write_text('must survive') + call(target, [str(target/'generate.py'), '--source', str(target/'vendor/pr2751'), + '--out', str(out)], 1, 'Output directory must be fresh') + need((out/'sentinel').read_text() == 'must survive', 'generator replaced output') + need(inventory(target) == baseline, 'failure controls changed restored package') + print('PASS_ROUTING_LEAF_INTEGRITY Git-free=1 source=1 omitted-frame=1 typed-receipt=1 optimized-refusal=1 output-preservation=1') + + +if __name__ == '__main__': + main() diff --git a/research/complex-routing-leaf-fusion/vendor/ceiling.py b/research/complex-routing-leaf-fusion/vendor/ceiling.py new file mode 100644 index 0000000000..6c0f54527d --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/ceiling.py @@ -0,0 +1,152 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Packing-independent ceiling for a complex local word under the hosted nine-stage coverage law. + +Model (all inputs explicit): + * per replica the template has `families` live data families and `stages` invocations, so + w = families / stages live families per call; on the selected T37/T16 line all helpers are + hosted on data families, so w = 2 * pairs * V / stages is fixed by the port count V; + * coverage identity (PR1012, re-checked here on the selected profile): paid rank mass equals + (m - 1) * W + centre * N, i.e. every live family keeps exactly one unpaid coordinate and every + call pays its centre path (`unpaid` > 1 is a what-if for a changed coverage law only); + * the local word fixes its own paid child profile `local` (per call); + * every remaining unit of mass is an idle/remainder child of rank at most R, where the outer + recipe's halving guard m^2 > 2 R^2 bounds R (R = 51 for m = 73). + +Lemma. For a >= 0, a child of rank r costs (r/m)^(1-a) = r * c(r), with c(r) = r^(-a) m^(a-1) +non-increasing in r. Hence, with idle mass M fixed and idle ranks <= R, every idle histogram has +moment >= the relaxation that puts all of M into (possibly fractional) rank-R children: + + relax(a) = [ sum_local n_r (r/m)^(1-a) + (M/R) (R/m)^(1-a) ] / w (per call). + +The moment is increasing in a. So relax(a*) > 1 certifies that no hosting, owner packing or +idle-remainder change of the given local word, template and outer recipe certifies a saving +>= a*. Under the retained reduction kappa < a/(1+a) when the complex side binds, so +a*/(1+a*) also bounds kappa. This is a bound for the stated model, not for other local words, +templates, coverage laws or outer recipes. + +Exact rational intervals: ln k from atanh chains, exp by Taylor with Lagrange remainder, +outward rounding to 2^-PREC. Standard library only. Douglas Colkitt, with Claude (Anthropic) +assistance. +""" +from fractions import Fraction as Q +from functools import lru_cache +from math import isqrt + +PREC = 256 + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def down(x): + return Q((x.numerator << PREC) // x.denominator, 1 << PREC) + + +def up(x): + return -down(-x) + + +@lru_cache(None) +def atanh(t): + """Enclosure of atanh(t) for rational 0 < t <= 1/3.""" + require(0 < t <= Q(1, 3), 'atanh range') + s, p, k = Q(0), t, 0 + while True: + term = p / (2 * k + 1) + s += term + p *= t * t + k += 1 + tail = p / ((2 * k + 1) * (1 - t * t)) + if tail < Q(1, 1 << (PREC + 8)): + return down(s), up(s + tail) + + +@lru_cache(None) +def ln(k): + """Enclosure of ln k for an integer k >= 1: ln k = ln(k-1) + 2 atanh(1/(2k-1)).""" + require(isinstance(k, int) and k >= 1, 'ln domain') + if k == 1: + return Q(0), Q(0) + lo, hi = ln(k - 1) + a, b = atanh(Q(1, 2 * k - 1)) + return down(lo + 2 * a), up(hi + 2 * b) + + +def exp(lo, hi): + """Enclosure of exp([lo, hi]) for 0 <= lo <= hi <= 1/2.""" + require(0 <= lo <= hi <= Q(1, 2), 'exp range') + def series(y, upper): + s, t, k = Q(1), Q(1), 0 + while True: + k += 1 + t = t * y / k + s += t + if t * y < Q(1, 1 << (PREC + 8)): + return up(s + 2 * t * y / (k + 1)) if upper else down(s) + return series(lo, False), series(hi, True) + + +def child_cost(r, m, a): + """Enclosure of (r/m)^(1-a) = (r/m) exp(a ln(m/r)).""" + lm, um = ln(m) + lr, ur = ln(r) + e = exp(max(Q(0), a * (lm - ur)), a * (um - lr)) + return down(Q(r, m) * e[0]), up(Q(r, m) * e[1]) + + +def max_idle_rank(m): + """Largest R with m^2 > 2 R^2 (outer halving guard).""" + R = isqrt((m * m - 1) // 2) + while 2 * (R + 1) ** 2 < m * m: + R += 1 + while 2 * R * R >= m * m: + R -= 1 + return R + + +def model(local, m, families, stages, centre, R=None, unpaid=1): + """Per-call quantities. local: {rank: count per call (Fraction ok)}.""" + R = max_idle_rank(m) if R is None else R + require(2 * R * R < m * m, 'idle rank cap violates the halving guard') + require(all(0 < r < m for r in local) and all(n >= 0 for n in local.values()), 'local profile') + w = Q(families, stages) + require(1 <= unpaid < m, 'unpaid coordinates per family') + total = (m - unpaid) * w + centre + local_mass = sum(r * Q(n) for r, n in local.items()) + idle = total - local_mass + require(idle >= 0, 'local word pays more mass than the coverage law allows') + return dict(R=R, w=w, total_mass=total, local_mass=local_mass, idle_mass=idle, deficit=unpaid * w - centre) + + +def relax(local, m, families, stages, centre, a, R=None, unpaid=1): + """Enclosure of the per-call relaxation moment at saving a.""" + q = model(local, m, families, stages, centre, R, unpaid) + lo = hi = Q(0) + for r, n in local.items(): + c = child_cost(r, m, a) + lo, hi = lo + Q(n) * c[0], hi + Q(n) * c[1] + c = child_cost(q['R'], m, a) + k = q['idle_mass'] / q['R'] + lo, hi = lo + k * c[0], hi + k * c[1] + return down(lo / q['w']), up(hi / q['w']) + + +def ceiling(local, m, families, stages, centre, grid=Q(1, 10 ** 15), R=None, unpaid=1): + """Grid bracket [a_lo, a_hi]: relax(a_lo) < 1 < relax(a_hi), certified. a_hi is the ceiling.""" + lo, hi = Q(0), Q(1, 20) + require(relax(local, m, families, stages, centre, hi, R, unpaid)[0] > 1, 'search window too small') + require(relax(local, m, families, stages, centre, lo, R, unpaid)[1] < 1, 'relaxation has no positive saving') + while hi - lo > grid: + mid = Q(int((lo + hi) / 2 / grid)) * grid + if mid <= lo: + mid = lo + grid + v = relax(local, m, families, stages, centre, mid, R, unpaid) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise ValueError('enclosure too wide to separate the grid point') + return lo, hi diff --git a/research/complex-routing-leaf-fusion/vendor/pr2751/CLAIM.json b/research/complex-routing-leaf-fusion/vendor/pr2751/CLAIM.json new file mode 100644 index 0000000000..48ad23a430 --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/CLAIM.json @@ -0,0 +1,24 @@ +{ + "status": "PASS_CONDITIONAL_FINITE_CONSTRUCTION_COMPLETE_RELEASE", + "complex_lower": "0.001717141586348426338109", + "complex_upper": "0.001717141586348426338110", + "kappa": "17171415863484263381089999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "profile": { + "1": 1593072, + "2": 430236, + "3": 204396, + "4": 79920, + "5": 22532, + "8": 5328, + "32": 1, + "48": 26558 + }, + "comparison_pr": 2733, + "comparison_head": "2761b52b17590b8cf94f2e410004a8252d5592dc", + "scope": "Conditional finite construction and complete strict supplier/modern outer release; inherited theorem assumptions remain.", + "latest_comparison": { + "pr": 2745, + "head": "4f485de05544884fa0f2edf6063bb9259decad30", + "exact_claim": "evidence/PR2745-CLAIM.json" + } +} diff --git a/research/complex-routing-leaf-fusion/vendor/pr2751/LICENSE b/research/complex-routing-leaf-fusion/vendor/pr2751/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/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/complex-routing-leaf-fusion/vendor/pr2751/PROFILE.json b/research/complex-routing-leaf-fusion/vendor/pr2751/PROFILE.json new file mode 100644 index 0000000000..080d9e165d --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/PROFILE.json @@ -0,0 +1,10 @@ +{ + "1": 1593072, + "2": 430236, + "3": 204396, + "4": 79920, + "5": 22532, + "8": 5328, + "32": 1, + "48": 26558 +} diff --git a/research/complex-routing-leaf-fusion/vendor/pr2751/PROOF.md b/research/complex-routing-leaf-fusion/vendor/pr2751/PROOF.md new file mode 100644 index 0000000000..d2b1a96ba8 --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/PROOF.md @@ -0,0 +1,25 @@ +# Changed recovery contract and complete moment + +The exact object is the two finite T74 words reconstructed by `generate.py`. The experiment uses a single explicit assignment, not a search over all assignments. Starting before PR2462's lowfour transformation is essential: applying the old lowfour patch first is a positive control reproducing its complete original words. + +The new `(removed helper, recovered source, partner)` assignments are: + +``` +(696,33,49), (697,55,101), (698,74,83), (700,85,98), +(680,49,33), (681,83,74), (682,98,85), (684,101,55), +(688,68,4), (689,80,88), (690,88,80), (692,31,12). +``` + +The last eight are PR2696's assignment. For each of the pairs33/49,55/101,74/83,85/98, let `(x,y)` denote the values after their last original uses, in their shared frame. The two added gates are `x += y/2` followed by `y -= x`, hence the linear map is `(x+y/2, y/2-x)`. For the actual predecessor state these restore the two original source values. The proof of that word-specific premise is the full arbitrary-input exact symbolic replay, not a claim that this map is the identity on arbitrary `(x,y)`. + +These restorations precede the new alias handoffs. Original operator IDs remain stable; twelve new chart transformations are appended. Removed-helper echoes are deleted only where they are target additions. For each new source, the generator computes the complete symbolic residual, transports its negative through precondition/compensation, and emits explicit initial correction gates and inverse source warps. Every residual must consist of a single new operator applied to its recovered source. Independent forward/dual propagation checks the resulting arbitrary-input identity, including dirty registers, and separately checks inverse cleanup. + +All lifted targets have frame `[45]`; their offsets are14,21,37,41,43,47,52,78,99,104,106,110. None is a target read by any cut gate. Actual frame propagation therefore leaves all eight centre children rank8. This changes the old-four recovery/target paths fixed in PR2720; its obstruction is respected within its stated domain. + +Apply the six PR2679 pre-life substitutions to the actual resulting state, refit the unique `515 += 563` gate (now B904), then alias653 into563. The complete generator checks semantic equality of both resulting words. The source-bound original checks and negative controls are rerun. No helper saving is inferred solely from nominal register labels. + +The complete local profile is `{1:2366,2:646,3:297,4:120,5:26,8:8}`. Compared with the PR2733 composition it changes by `4*(H8-H7-H1)` per local word. The same415-helper inventory admits the explicit complete allocation; `independent_owners.py` checks276390 roles, strict temporal windows, every physical cell, family masks and all remainders. There are666 call equivalents, giving global delta `2664*(H8-H7-H1)` and rank mass4816512 unchanged. + +At exponent `0= 1, 'positive logarithm range') + power = 0 + while x >= 2: + x /= 2 + power += 1 + a, b = log_reduced(x) + c, d = log_reduced(F(2)) + return a + power * c, b + power * d + + +def exp_bounds(x): + """Taylor terms 0..15; later term ratios are bounded by x/17.""" + require(0 <= x < F(1, 100), 'exponential argument range') + term, lower = F(1), F(1) + for n in range(1, 16): + term = term * x / n + lower += term + tail = term * x / 16 / (1 - x / 17) + return lower, lower + tail + + +def moment_bounds(profile, exponent): + lower = upper = F(0) + for rank, count in sorted(profile.items()): + log_lo, log_hi = log_bounds(F(DIMENSION, rank)) + exp_lo, _ = exp_bounds(exponent * log_lo) + _, exp_hi = exp_bounds(exponent * log_hi) + weight = F(count * rank, DIMENSION) + lower += weight * exp_lo + upper += weight * exp_hi + return lower, upper diff --git a/research/complex-routing-leaf-fusion/vendor/pr2751/independent_local.py b/research/complex-routing-leaf-fusion/vendor/pr2751/independent_local.py new file mode 100644 index 0000000000..e0b556adc3 --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/independent_local.py @@ -0,0 +1,161 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Mason Hale/Codex PR2696 literal replay, extended by Tekalign/Codex. +Adds anticipatory corrections, checks six pre-life hosts and checks all twelve +source-recovery assertions at operator IDs47 through58. +""" +import json,gzip,hashlib +from collections import Counter,defaultdict +from fractions import Fraction as F +from functools import lru_cache +from pathlib import Path +@lru_cache(None) +def span(vs): + s={0} + for v in vs:s|={x^v for x in tuple(s)} + return frozenset(s) +def S(vs):return span(tuple(vs)) +def rank(vs):return len(S(vs)).bit_length()-1 +def dm(s):return len(s).bit_length()-1 +FULL=S([1<>i&1:a^=c + return a +def regs(g):return g[1:3] if g[0]=='add' else g[1:2] +def nt(r):return not 112<=r<224 +def load(p):return json.loads(gzip.decompress(p.read_bytes())) +def chronological(w): + d=defaultdict(list) + for op,(p,r,*_) in enumerate(w['warps'],1):d[p].append(['warp',r,op]) + b=[] + for i in range(len(w['B'])+1): + b+=d[i] + if i0 else (new,old) + assert frozenset(im(cols,x) for x in S(a))==S(b) + cur[r]=S(new) + for g in w['A']: + if g[0]=='warp':warp(*g[1:]) + else: + for r in regs(g):climb(r,g[-1]) + bysection['A']=dict(counts);prev=counts.copy() + lev={int(k):S(v) for k,v in w['target_levels'].items()} + assert all(cur[112+t]==lev.get(t,S([])) for t in range(112)) + paths=[] + for r,vs in zip(w['centers'],w['center_frames']): + s=S(vs);assert cur[r]==s + targets=[g[1]-112 for g in w['cut'] if g[2]==r] + frames=sorted({lev.get(t,S([])) for t in targets},key=lambda s:-len(s)) + ds=[] + for f in frames: + assert f<=s + d=dm(s)-dm(f) + if d:counts[d]+=1;ds.append(d) + s=f + paths.append({'center':r,'start_rank':rank(vs),'target_offsets':targets,'reader_lines':[sorted(f-{0}) for f in frames],'paid_degrees':ds}) + bysection['cut']=dict(counts-prev);prev=counts.copy() + ops=defaultdict(list) + for op,rec in enumerate(w['warps'],1):ops[rec[0]].append((op,rec)) + for i in range(len(w['B'])+1): + for op,(_,r,cols,old,new) in ops[i]:warp(r,op,old,new) + if i=224) + assert counts==Counter({int(k):v for k,v in w['report']['local_profile'].items()}) + assert inventory==Counter({int(k):v for k,v in w['report']['width_inventory'].items()}) + return {'profile':dict(sorted(counts.items())),'section_profiles':bysection,'inventory':dict(sorted(inventory.items())),'center_paths':paths},start,ends + +def check_cleanup(w): + restored=set(map(int,w['helper_final'])) + cold=lambda r:r+704 if r in restored else r + forward=w['A'][w['prelude_events']:]+chronological(w)+w['restore'] + expected=[] + for g in reversed(forward): + if g[0]=='warp':expected.append(['warp',cold(g[1]),-g[2]]) + elif nt(g[1]): + if g[0]=='add':expected.append(['add',cold(g[1]),cold(g[2]),-g[3],g[4]]) + else:expected.append(['scale',cold(g[1]),g[3],g[2]]) + assert expected==[g[:-1] for g in w['cleanup']] + assert all(S(g[-1])==FULL for g in w['cleanup']) + return len(expected) + +def algebra(w): + # A monomial records its operations oldest-first; appending an inverse + # cancels the newest symbol. No native/generator/audit modules imported. + live=set(range(704))-set(w['removed']);cold=set(map(int,w['helper_final'])) + assert all(112<=x['target']<224 and x['source'] in {273,275,289,291,305,321} for x in w['initial_corrections']) + program=[['correction',x] for x in w['initial_corrections']]+w['precondition']+w['compensation']+w['A']+w['cut']+chronological(w)+w['restore'] + result={} + for dual in [False,True]: + rows={r:{(r,()):F(1)} for r in live} + rows.update({704+r:{} for r in cold}) + def apply(g): + op=g[0] + if op=='correction': + x=g[1];t,s=x['target'],x['source'];q=F(x['coefficient']) + ops=list(reversed(x['operator_word'])) + if dual: + t,s,q=s,t,-q + ops=[-(abs(v)+1000)*(1 if v>0 else -1) for v in x['operator_word']] + for (r,word),c in list(rows[s].items()): + for v in ops:word=word[:-1] if word and word[-1]==-v else word+(v,) + key=(r,word);value=rows[t].get(key,F(0))+q*c + if value:rows[t][key]=value + else:rows[t].pop(key,None) + elif op=='add': + t,s=g[1:3];q=F(g[3],g[4]);assert t!=s + if dual:t,s,q=s,t,-q + for term,c in list(rows[s].items()): + v=rows[t].get(term,F(0))+q*c + if v:rows[t][term]=v + else:rows[t].pop(term,None) + elif op=='scale': + q=F(g[2],g[3]);q=1/q if dual else q + rows[g[1]]={term:q*c for term,c in rows[g[1]].items()} + elif op=='warp': + d=g[2] + if not dual and 460 else -1) + rows[g[1]]={(r,word[:-1] if word and word[-1]==-d else word+(d,)):c for (r,word),c in rows[g[1]].items()} + else:raise AssertionError(op) + for g in program:apply(g) + if not dual: + assert all(rows[112+t]=={(112+t,()):F(1),(t,()):F(1)} for t in range(112)) + assert all(rows[r]=={(r,()):F(1)} for r in cold) + assert all(not any(var in cold-{r} for (var,word) in rows[r]) for r in live) + for g in w['cleanup']:apply(g) + for r in live: + exp={(r,()):F(1)} + if dual and r<112:exp[(112+r,())]=F(-1) + if not dual and 112<=r<224:exp[(r-112,())]=F(1) + assert rows[r]==exp,(dual,r,rows[r]) + assert all(not rows[704+r] for r in cold) + result['dual' if dual else 'forward']='PASS' + return result diff --git a/research/complex-routing-leaf-fusion/vendor/pr2751/independent_owners.py b/research/complex-routing-leaf-fusion/vendor/pr2751/independent_owners.py new file mode 100644 index 0000000000..93270b725a --- /dev/null +++ b/research/complex-routing-leaf-fusion/vendor/pr2751/independent_owners.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Tekalign (@tekuuu), with substantial OpenAI Codex assistance. +"""Independent integer-time chronology and bit-mask whole-fill verification. + +No retained window code, donor generator, solver or native checker is imported. +Credit PR2679's pre-life/refit words, PR2673/PR2621 priority scheduling, +PR2588's swapped words, PR2559's evacuation, PR2530's source-partner +fill and the PR2462/PR2322/PR2436 lineage; +Hao Yan and the retained controller authors supply the underlying schedule. +This checks a finite hosting witness, not native circuitry or an exponent. +""" +import argparse +import sys +sys.dont_write_bytecode=True +import gzip +import hashlib +import json +from collections import Counter +from pathlib import Path + + +def need(ok, why): + if not ok: + raise RuntimeError(why) + + +def windows(template, order): + ranks={c['child']:c['rank'] for c in template['idle_children']} + pairs={e['stage']:e['pair'] for e in template['recipe'] if e['kind']=='local'} + blocks={};stage=None + for event in template['execution_schedule']: + if event['kind'] in ('bank_padding_cover_sweep','translate_every_live_family'): + continue + if event['kind']=='local_cover_sweep': + stage=event['stage'];blocks[stage]=[] + need(stage is not None,'event before first call') + blocks[stage].append(event) + progression=[0]*74;last={};result={} + for t,(stage,replica) in enumerate(order): + need(0<=replica<74 and stage==progression[replica],'order chronology') + progression[replica]+=1 + for j,event in enumerate(blocks[stage]): + kind=event['kind'] + if kind=='local_cover_sweep': + need(j==0,'local call position') + last[replica,pairs[stage]]=t + elif kind=='bridge': + last[replica,event['src']]=last[replica,event['dst']]=t + elif kind=='idle_cover_sweep': + need(j>0,'idle position') + start=last.get((replica,event['pair']),-1) + for child in event['child_indices']: + if child in ranks: + result[replica,child]=(ranks[child],start,t) + need(progression==[9]*74,'complete replica progression') + return result + + +def check(plan, template, order, fill, providers, initial_dispatch, expected_profile): + need(len(order)==666 and len(set(map(tuple,order)))==666,'call coverage') + win=windows(template,order) + dispatch=dict(initial_dispatch) + for s,r,pid in fill['dispatch_overrides']: + need((s,r) in dispatch and pid in providers,'dispatch override') + dispatch[s,r]=pid + need(set(dispatch)==set(map(tuple,order)),'dispatch coverage') + need(fill['columns']==['time','helper','owner_replica','child','port','offset'],'role columns') + need(len(fill['rows'])==666*415,'role count') + need(all(len(p['widths'])==415 for p in providers.values()),'helper widths') + helper_bits=[0]*666;family_bits=[0]*666;occupied={} + for row in fill['rows']: + need(len(row)==6 and all(type(v) is int for v in row),'role shape') + t,h,o,c,port,offset=row + need(0<=t<666 and 0<=h<415 and 0<=port<112,'role bounds') + cap,start,stop=win[o,c] + need(start Fraction(read(SOURCE/'CLAIM.json')['kappa']), + 'strict improvement over source target') + _, lower_hi = M.moment_bounds(profile, low) + upper_lo, _ = M.moment_bounds(profile, high) + source_lo, _ = M.moment_bounds(old_profile, low) + need(lower_hi < 66304 < upper_lo and source_lo > 66304, + 'retained independent interval engine root and strict source comparison') + return dict(status='PASS_COMPLETE_FRAME_COMPOSITION', authenticated_files=authenticated, + providers=reports, roles=owner['roles'], calls=len(order), + profile={str(k): v for k, v in sorted(profile.items())}, + rank_mass=sum(k*v for k, v in profile.items()), controls=controls, + complex_lower=str(low), complex_upper=str(high), kappa=claim['kappa'], + scope='Complete finite words and allocation; fresh native and outer release are separate.') + + +if __name__ == '__main__': + actual = run() + expected = read(HERE / 'RESULT.json') + canonical = lambda value: json.dumps(value, sort_keys=True, separators=(',', ':')) + need(canonical(actual) == canonical(expected), 'complete typed RESULT.json equality') + print(json.dumps(actual, sort_keys=True, indent=2))