From 48153115a150af98a9c94adb34cab180dcd226e5 Mon Sep 17 00:00:00 2001 From: Matthieu Pascal Date: Wed, 14 Oct 2026 18:28:34 +0800 Subject: [PATCH] research: bind R439 helper-mixing word to hosted invoice --- research/r439-abc-hosted-invoice/README.md | 168 +++++++++ research/r439-abc-hosted-invoice/RESULT.json | 310 ++++++++++++++++ research/r439-abc-hosted-invoice/SOURCES.json | 336 ++++++++++++++++++ research/r439-abc-hosted-invoice/TASK.json | 84 +++++ .../r439-abc-hosted-invoice/VALIDATION.json | 40 +++ research/r439-abc-hosted-invoice/VERIFY.json | 77 ++++ research/r439-abc-hosted-invoice/invoice.py | 111 ++++++ research/r439-abc-hosted-invoice/invoke.py | 36 ++ research/r439-abc-hosted-invoice/verify.py | 222 ++++++++++++ 9 files changed, 1384 insertions(+) create mode 100644 research/r439-abc-hosted-invoice/README.md create mode 100644 research/r439-abc-hosted-invoice/RESULT.json create mode 100644 research/r439-abc-hosted-invoice/SOURCES.json create mode 100644 research/r439-abc-hosted-invoice/TASK.json create mode 100644 research/r439-abc-hosted-invoice/VALIDATION.json create mode 100644 research/r439-abc-hosted-invoice/VERIFY.json create mode 100644 research/r439-abc-hosted-invoice/invoice.py create mode 100644 research/r439-abc-hosted-invoice/invoke.py create mode 100644 research/r439-abc-hosted-invoice/verify.py diff --git a/research/r439-abc-hosted-invoice/README.md b/research/r439-abc-hosted-invoice/README.md new file mode 100644 index 0000000000..9a289d1090 --- /dev/null +++ b/research/r439-abc-hosted-invoice/README.md @@ -0,0 +1,168 @@ +# Complete nine-stage hosted invoice for the PR1122 helper-mixing word + +**Finite hosted construction replay; no new circuit, supplier selection or κ.** +The fixed 10,652-ADD word of [PR1122](https://github.com/CrocSwap/integer-mult-bounds/pull/1122) +passes the unchanged nine-stage emitter and owner auditor with PR589's frozen +hosting assignment. All **126,432 helper occurrences** are hosted without banks; +the complete emitted program has **3,911,328 instructions**. Its invoice retains +the selected bit profile and bit saving. The unrounded prefix and two-level +bounds use 176 and 390 bits, still charged at 192 and 512 bits. + +PR1122 supplied the circuit and native evidence. [PR1194](https://github.com/CrocSwap/integer-mult-bounds/pull/1194) +supplied the semantic-D substitution argument; [PR1311](https://github.com/CrocSwap/integer-mult-bounds/pull/1311) +applied it to this changed-A word. Both the composition and bridge packages +explicitly left the **changed-word hosted emission/audit and invoice** open. +This package completes that finite handoff, binding those stages to one word. +It does not supply a new proof of the inherited physical or all-size premises. + +## Exact object and complete bill + +Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. The candidate is the unmodified +`research/r439-abc-semantic-bridge/inputs/candidate.json.gz`, inherited from +PR1122 head `a2551e70fce0cc34348f50f1a94e7cc4c80bbcbf`: + +- File SHA256: `2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066`. +- Canonical decoded SHA256: `7bbaed96041297cd38e89ff48eb055750cfab36609b9fdbeafcec1b2758c1254`. +- Emitted instruction SHA256: `8f2239a09b87367ba754a6c0ebd8989e81b295df3628ebf4991d1cab15fabfcf`. + +| Quantity | PR589 selected bit word | Fixed PR1122 word | +| --- | ---: | ---: | +| Local ADDs, including preparation/restoration | 24,305 | 10,652 | +| Local MOVE/ADD/COPY/ERASE records | 27,234 | 13,581 | +| Local COPY / ERASE | 9 / 9 | 9 / 9 | +| Local rank mass | 5,129 | 5,129 | +| Nine-stage local invocations | 288 | 288 | +| Hosted helper occurrences / banks | 126,432 / 0 | 126,432 / 0 | +| Paid recursive children | 904,896 | 904,896 | +| Live / physical families | 28,416 / 28,425 | 28,416 / 28,425 | +| Prefix bits / charge | 177 / 192 | 176 / 192 | +| Two-level coefficient bits / charge | 393 / 512 | 390 / 512 | +| Row coefficient | 18,355 | 18,355 | + +The baseline column is pinned PR589 evidence, not a new baseline hosted replay. +All gate savings are PR1122's and its predecessors'. The freshly recounted +hosted profile is +`{1:381024, 2:400416, 3:22752, 4:26880, 5:29376, 6:17376, 7:26784, 42:288}`. +Rank mass is 1,808,352 and deficit is 10,272. The bit saving remains +`1733427039589844234749 / 10^24`; the next grid point is rejected by exact +moment enclosures. The selected complex supplier still binds. + +[RESULT.json](RESULT.json) retains every integer term of the invoice: +3,131,712 scalar additions (288 complete local words plus 63,936 bridges), +2,592 copied-centre episodes, selector, address, compiler, store and precision +terms. Each episode contains both COPY and ERASE; the inherited `J` term +also charges their lifecycle work. No virtual replacement D is executed or +billed. The row, child-size and 192/512-bit guards pass at their full charges. + +## Reproduce + +Python 3.12, C++17, Boost headers and the exact NumPy/SymPy/SciPy versions in +[VERIFY.json](VERIFY.json) are required. Set `BOOST_INCLUDE` to the directory +containing `boost/` if headers are not in `/usr/include`; `CXX` defaults to `c++`. +From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/r439-abc-hosted-invoice +``` + +Expected final lines: + +```text +PASS_R439_ABC_HOSTED_INVOICE ADDs=10652 helpers=126432 banks=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/r439-abc-hosted-invoice outcome=completed +``` + +The registered command has a 600-second limit. To retain all emitted files, +native binaries, commands and logs, use a fresh output directory outside the +checkout: + +```sh +python3.12 -I -B research/r439-abc-hosted-invoice/verify.py --output /tmp/r439-abc-hosted-run +``` + +The default replay is read-only with respect to repository files. Existing +output directories are refused. `--write` explicitly regenerates RESULT.json. +All checks in the wrapper remain enabled under `-O`; inherited scripts run +in separate interpreters with assertions enabled. + +## What is checked + +1. The unchanged PR1311 verifier checks the full arbitrary-dirty D boundary, + raw J/V/K blocks, original-D chronological splice, geometry, endpoints and + its nine semantic controls. Literal H2 and K syntax still reject the actual + helper-mixing word; their predicates are not weakened. +2. The unchanged exporter, native legality checker and native 5/9-stage + programs replay the actual candidate, with 883 and 1,327 formal columns. + Local positive bounds are F=15,223 and B=3,910,388, using 92 bits below the + 104-bit cap. Six and eighteen omitted-bridge controls reject. +3. The inherited geometry and exact string parameterizers run afresh. + PR589's fixed selection is read directly; no optimizer is invoked. + The parent checks 4,839 independent unbanked scalar columns and rejects + seventeen template mutations. The hosted auditor independently reconstructs + ownership, windows, full instruction digest and paid profile, rejecting + sixteen ownership/template mutations. +4. `invoice.py` expands the inherited bit invoice into inspectable integer + terms. It also executes every statement of the unchanged adapted PR510 + bit-invoice prelude, through its `res` assignment, and compares the exact + coefficient, two-level bound, scalar/selector counts and moment brackets. + The subsequent historical complex/outer assembly loop is outside this task. + This is a port-consistency check, not an independent mathematical method. +5. Seven additional controls reject mixed word/record receipts, an understated + profile, prefix or COPY charge, a missing bridge control, and a stale + hosted-parent binding. These mutate the actual output files at the collector + boundary and restore them after each check. + +The inherited geometry receipt contains elapsed time. Only that nonmathematical +field is normalized to zero **before** downstream hashing, so the final +certificate is reproducible. Every downstream producer and auditor consumes +and binds those same bytes. No geometry assertion or mathematical field changes. + +[SOURCES.json](SOURCES.json) pins the complete 53-file input/context closure +to the base, Git blobs and SHA256. Runtime Python read inventories and native +compiler dependency files reject undeclared repository dependencies. Compiler, +Boost and third-party Python libraries remain trusted environment dependencies; +they are not vendored or claimed as independently verified. Catalogue and +selected-record pins are historical provenance, so later selections do not +silently retarget this experiment. + +## Scope and inherited obligations + +This is a finite, source-bound emitted-template and invoice result. It is not +an enumeration of the astronomical cover, a proof-assistant theorem, a new +all-size compiler, or unconditional admission of the supplier. It retains the +common-frame/label interpretation, mutable-source realization, chronological +substitution, whole-call correlated-helper hosting, precision/tape, exact +recovery and analytic-transfer premises of the cited chain. Maintainer +acceptance of the replacement semantic interface remains separate. No current +outer assembly or eleven-stage hosting replay is claimed. The selected record, +upstream files and all predecessor packages are unchanged. + +## Open next questions + +Should this exact word be admitted as a maintained supplier under semantic D? +The next step is a review of PR1194/PR1311 together with this bound hosted +receipt, followed by the repository's supplier-admission process if accepted. +The blockers are acceptance of the replacement interface and inherited +physical/all-size premises, not a missing finite nine-stage invoice. The paid +profile is unchanged, so this package gives no exponent-based reason to change +the selected frontier. [TASK.json](TASK.json) records the same handoff. + +## Coordination and credit + +Assignment seed **1**, bit supplier; card `bit-helper-contract`, refined to the +existing word's complete hosted bill. [Discussion1796](https://github.com/CrocSwap/integer-mult-bounds/discussions/1796) +records the claim. Three candidate scopes and the overlap check are in TASK.json. +Source-supported batch deletion (active Discussion1785), the already covered +3x4/4x4 feedback censuses (PR1557/1706), and PR1782's different copy-sharing +word were not repeated. + +Prepared for **Matthieu Pascal (@mtpsl)** with substantial **OpenAI Codex +assistance** in implementation, checking and writing. Apache-2.0; no independent +human review claimed. Credit Gareth Davidson/PR1122 for the composed word and +native work; Arham Tahir/PR1311 and woklerx/PR1194 for the semantic bridge; +Sagar Thakrar/PR1062, Sricharan Vagvala/PR967, Aaron Wang/PR1015 and Ross +Richardson/PR923 for its circuit lineage; DreamingOfClouds/PR589/510 and +eumemic/PR555/543 for the supplier and parameterization; DaysSky, chafreaky, +Zhihao Chen, Dylan Crow and the retained exporter/native/hosting/moment +contributors. Their OpenAI/Anthropic assistance disclosures and source notices +are retained in the unchanged dependencies. diff --git a/research/r439-abc-hosted-invoice/RESULT.json b/research/r439-abc-hosted-invoice/RESULT.json new file mode 100644 index 0000000000..75fc85424f --- /dev/null +++ b/research/r439-abc-hosted-invoice/RESULT.json @@ -0,0 +1,310 @@ +{ + "schema_version": 1, + "word_sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066", + "semantic_bridge_receipt_sha256": "2cb4c886d02714a103e5e59ab1aaca7501c41845c5224a7a4f054d62a68a336d", + "records_sha256": "c3b2efc2282db0f5593c35c46c44b70af79e724f77b322637b26dc54e8578d7c", + "native": { + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "records": 13581, + "common_frame_ADDs": 10652, + "rank_mass": 5129, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "copies": 9, + "erasures": 9 + }, + "stages": [ + { + "formal_columns_checked": 883, + "local_scalar_additions": 10652, + "bridge_additions": 666, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "15223", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3910388", + "reverse": true + } + ], + "payload_prefix_bits": 92, + "payload_prefix_upper": "3452394524099512658714524672", + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ] + }, + { + "formal_columns_checked": 1327, + "local_scalar_additions": 10652, + "bridge_additions": 1998, + "signed_lift_prefix": [ + { + "bits": 14, + "cancellation_free_signed_row_l1_upper": "15223", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "3910388", + "reverse": true + } + ], + "payload_prefix_bits": 92, + "payload_prefix_upper": "3452394524099512658714524672", + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ] + } + ], + "parent": { + "template_sha256": "fce6aebb6bd72b2d31ef225fc3e3cf7a34d8e831b88fa5810692352e92963795", + "source_records_sha256": "c3b2efc2282db0f5593c35c46c44b70af79e724f77b322637b26dc54e8578d7c", + "word_sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066", + "local_additions": 10652, + "global_prefix_bound": "50109557170207398770972615575887331408085730734374912", + "global_prefix_bits": 176, + "charged_prefix_bits": 192, + "independent_unbanked_scalar_columns": 4839, + "copy_erase_episodes": 2592, + "bridge_additions": 63936 + }, + "parent_controls": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ], + "hosted": { + "status": "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT", + "template_sha256": "d23a10701f19e2525749a53a625e7cff0b64538f9aecd5280b79f5e0d35e7e19", + "emitted_program_sha256": "8f2239a09b87367ba754a6c0ebd8989e81b295df3628ebf4991d1cab15fabfcf", + "emitted_events": 3911328, + "profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "5": 29376, + "6": 17376, + "7": 26784, + "42": 288 + }, + "live": 28416, + "physical": 28425, + "hosted_residuals": 126432, + "bank_assignments": 0, + "rank_mass": 1808352, + "deficit": 10272, + "maxchild": 42, + "mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ] + }, + "invoice": { + "profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "5": 29376, + "6": 17376, + "7": 26784, + "42": 288 + }, + "paid_calls": 904896, + "live": 28416, + "physical": 28425, + "rank_mass": 1808352, + "deficit": 10272, + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "next_grid_point_rejected": "6933708158359376939/4000000000000000000000", + "invoice_terms": { + "scalar_additions": 3131712, + "high_precision": 539367561646080, + "physical_store": 57086496000, + "child_compiler": 242935829263872, + "addresses": 4194304, + "copy_erase": 2592, + "selectors": 5680520640, + "prefix": 50109557170207398770972615575887331408085730734374912, + "constant": 1 + }, + "J": 2008320, + "coefficient": 50109557170207398770972615575887331408868096899630113, + "two_level_coefficient": 2056077243631368522979514168125953974252003783288912121157549688701759645537778978636954329025692193384797096918354564, + "prefix_bits": 176, + "charged_prefix_bits": 192, + "coefficient_bits": 176, + "two_level_bits": 390, + "charged_two_level_bits": 512, + "row_coefficient": 18355, + "maxchild": 42, + "halving_depth": 2, + "new_kappa": false, + "unchanged_reference_bit_invoice_agrees": true + }, + "no_selected_change": true, + "new_kappa": false, + "binding_controls": [ + "wrong-word", + "wrong-records", + "invoice-profile", + "invoice-prefix", + "invoice-copy", + "missing-bridge-control", + "stale-hosted-template" + ] +} diff --git a/research/r439-abc-hosted-invoice/SOURCES.json b/research/r439-abc-hosted-invoice/SOURCES.json new file mode 100644 index 0000000000..0b2a99b5f0 --- /dev/null +++ b/research/r439-abc-hosted-invoice/SOURCES.json @@ -0,0 +1,336 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "usage": "input", + "git_blob": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "usage": "input", + "git_blob": "82d69f7c5d044c9887c96b90c97f5639083ecd14", + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "usage": "input", + "git_blob": "cb1233c7e96b1aa8bbf4d2e4165d75ab0dca64b9", + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "usage": "input", + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/independent/checkword.py", + "usage": "input", + "git_blob": "da4e0fe05067184d4dab1e130ae1384c1fa983f5", + "sha256": "11bf9620ca9db16d52d9fe806b814fc9ec9a89c4d7645354d1861d96f6e805ad" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/independent/relax.py", + "usage": "input", + "git_blob": "a37e8b8176080d4a977bb48bd25f92f4a62b156b", + "sha256": "d6e9f58de3fa41f538516b6227c249d61fb30f0f6843027cc8a07a1a372fa6b6" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/mutate_records.py", + "usage": "input", + "git_blob": "6794516f665d36eac189894e350a5ad01113cb4c", + "sha256": "b0e75d6550412a7be4017695e6b237392b611bb852ad8ff309d6682c9f166a4e" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "usage": "input", + "git_blob": "f6d7afe3e623208c4207b6a683a1e3e49249e31c", + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/eleven/assemble.py", + "usage": "input", + "git_blob": "87cc45bc831fa7003906e8b026ac1480a69da1de", + "sha256": "c47889a606701ae592374dd82a13cee8c5a4e8449b7facfdad2d90563a30a18c" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/eleven/audit.py", + "usage": "input", + "git_blob": "10e47d32e3b4769ae5ce5bad9f76a7b3e5d797fc", + "sha256": "5ad832830c19ec6c904d1b64480f6b1e71c5673fdd38d487d17e179b1d197c09" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/eleven/emit.py", + "usage": "input", + "git_blob": "640cdb4d1220950e198f2fd9994d76d69ecbf764", + "sha256": "b0b25955875625ed63f82690f83aef976e3e9a978ae6620b23a23fc1207acd46" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/eleven/local_audit.py", + "usage": "input", + "git_blob": "2233c5f35f2fcb58809f7a1d8f91e9b36ad74080", + "sha256": "95275473d7f9811011bda760dd0f04de5169c2a6922456dc9a5725a5d671f941" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/outer.py", + "usage": "input", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/geometry.py", + "usage": "input", + "git_blob": "b4ad5074014dc00a01143910eb1cd27fafe0e15c", + "sha256": "9554182d67e434ea84b4430f909a2c400abc755d8487b51454a8e6968e62859d" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/nine/geometry.py", + "usage": "input", + "git_blob": "91594e0223e8fac49162b5aef834ffaa8e94a254", + "sha256": "36eeda3184bd009e89462b65c8725d10860c444f8da8f1f87e5f6e50120011ca" + }, + { + "path": "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz", + "usage": "input", + "git_blob": "8bec1751f7e33c3a1e4673ef5dbc34d6f205321e", + "sha256": "1fb726ea3818fe0837cceb0dd22a71a0814f064e5e781628104610d6468e0e55" + }, + { + "path": "research/e8-bit-carrier-skeleton/data/complex-b.json", + "usage": "input", + "git_blob": "0df48f8e590fc9ad01ca4d6eaf97b9acc10aac7d", + "sha256": "dce3f4b76aa3f6c3ba826ce556ffa61398b33e81e4d1a226dd2a36ce684fb02e" + }, + { + "path": "research/e8-bit-carrier-skeleton/data/eleven/residual-isometries.json", + "usage": "input", + "git_blob": "5c645b267861fd0994d2679885f8e0bbf99640b0", + "sha256": "0fa5b353a0321af2ce4e2045db1d4c2d6418a11663894e2afcdb1eaa1984bddc" + }, + { + "path": "research/e8-bit-carrier-skeleton/discovery/host_select.py", + "usage": "input", + "git_blob": "5b50de453ddbd90d433f9ea8ed584308e7ab2d0f", + "sha256": "2aaaac18e083d289d4341e734c32571c89c51fefba04b388d407c7372b906dc7" + }, + { + "path": "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h", + "usage": "input", + "git_blob": "fc5664e929d9a81d9b4926bee049a93330be86ec", + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + }, + { + "path": "research/e8-bit-p111-tuned/code/adapt9p.py", + "usage": "input", + "git_blob": "96bbc2ba9bb11984736e34db8b65c1a91e8f842e", + "sha256": "14365d0eb8f4a7352edd28816196148fd28d5bbcb36044ebeeb15ca051bca9de" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/data/selection9-p111.json", + "usage": "input", + "git_blob": "e69ea66a3add357f570fc5552ab6368b3c8f9bb2", + "sha256": "4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/verify.sh", + "usage": "input", + "git_blob": "92310cbc220ece46c72f2131ddcc8d802bd35c56", + "sha256": "efb1051d3e2c6119574a29a8e4efbe316307b5901d05079d029e12fae9ff1fb1" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/adapt.py", + "usage": "input", + "git_blob": "7c595c50bc3910577f8587ca94ce8b9c0e6f55b0", + "sha256": "27b6b77cc4ebf439f9019e63a22dedc1ef72ee65fe120aad3d17316b1df06d7b" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "usage": "input", + "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py", + "usage": "input", + "git_blob": "8864ca9b942a3507171edca0cf6cbaaf10fcf434", + "sha256": "57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_parent_k.py", + "usage": "input", + "git_blob": "ee54ca566ff9d8553f845144dd4570fa1fe21495", + "sha256": "374e1d983589463bbfa06b6e9f2ffafb9d2c14acf97b1f858593a3cef90e93d2" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/bank_routes_k.py", + "usage": "input", + "git_blob": "aaab9d5ae3f280dcb82775337d88dc244984e225", + "sha256": "ea678a7befda10c6f1b9dd38a36fe1437c6468472bd649f60b9f01522047e0bf" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py", + "usage": "input", + "git_blob": "b84c795a045143639efe6aefb0562b3c20a2c9d7", + "sha256": "298b16c3d4f58a468ad1a64564c8500cb281414a3f3c0428fd467908eeb4a4b4" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "usage": "input", + "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/hosting_k.py", + "usage": "input", + "git_blob": "02fea8320b676e14f8ffa242c3ddfa85fa829e31", + "sha256": "081c3b95b18d900d97ce82af64fb428f085b6adc6d8ca93ea920797dad7eb81e" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/bank_routes.py", + "usage": "input", + "git_blob": "9e43a876664a26899762f3b8e9a582e684a3650a", + "sha256": "7c6997c455bd55acca3a1603797c34e7733d557c27a7694a1429ff15773a505d" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/config.py", + "usage": "input", + "git_blob": "c6824d9c4ea37d58c0d24cb7a3021c4dfcc6f3bb", + "sha256": "283d7fad45155ee91e704d63ec947cf4a60aeff5cc43510bc0e835f7da7d8767" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/e8core.py", + "usage": "input", + "git_blob": "78983b368715e89fe8524a6dd2c13585d2b5394e", + "sha256": "1cb286196c1530d06f50f0997febc5993b388f33464e295611b920ba30a24eeb" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/outer.py", + "usage": "input", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/tile_m.py", + "usage": "input", + "git_blob": "cd5fd9b5399f5e7afe5d2a95bd3504bd543c0d60", + "sha256": "d6ae4a556472d403773cd2117c992bfc10e1187112da1b3893f3fae628a131dd" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py", + "usage": "input", + "git_blob": "68b536daa9e6546c0aa046934bf840aaa3c3fde3", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr545/code/adapt.py", + "usage": "input", + "git_blob": "bd1552af18ae259c01039627aa06006b9d5e760f", + "sha256": "b9a50303147a3003ad94fc4b1a822d4fca7f9b9e917d165e3c45152575302a0e" + }, + { + "path": "research/r439-abc-semantic-bridge/README.md", + "usage": "input", + "git_blob": "8129b45c65f67785a048b0118e6c3aad068a78cd", + "sha256": "0241708a0d0793d5e099ba23e05314257b3178d4a1c1470756756859700b860a" + }, + { + "path": "research/r439-abc-semantic-bridge/RESULT.json", + "usage": "input", + "git_blob": "c99ce921c94237bac60c6e4d52cfd362c4d34d08", + "sha256": "2cb4c886d02714a103e5e59ab1aaca7501c41845c5224a7a4f054d62a68a336d" + }, + { + "path": "research/r439-abc-semantic-bridge/SOURCES.json", + "usage": "input", + "git_blob": "52477f2ee146fb4424fb94cd22cae008b50b9277", + "sha256": "ae5f92bd6503dce397cd5c3ae0fb833db15ff62df03d25f39a631844cbfcbfac" + }, + { + "path": "research/r439-abc-semantic-bridge/inputs/candidate.json.gz", + "usage": "input", + "git_blob": "0ab597fefd68bfefecc85d631b172d174bdaeb70", + "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066" + }, + { + "path": "research/r439-abc-semantic-bridge/verify.py", + "usage": "input", + "git_blob": "5a9a3651bfc573c817391fba7d8047ca1963970d", + "sha256": "b7cad6b1b5cd55aed96dcaa3cc0879a99f7ddaa20b09f18faea4e04968c79b26" + }, + { + "path": "research/r439-abc-star-composition/README.md", + "usage": "input", + "git_blob": "bd483291155f83b662f099c974db57a152d3158e", + "sha256": "5b26bbd515abeb1544502806a5812342763815cb224d4f3119561736077d9d31" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-semantic-d-contract-seed10/PROOF.md", + "usage": "input", + "git_blob": "2707fdb0d2f34c1c6c4ea41c2a68e44904a3e4fd", + "sha256": "dfbca8c61a92fdf0db8af450dc4466849da37fc296e28b67f357e196e87327db" + } + ] +} diff --git a/research/r439-abc-hosted-invoice/TASK.json b/research/r439-abc-hosted-invoice/TASK.json new file mode 100644 index 0000000000..f9ccf5f82e --- /dev/null +++ b/research/r439-abc-hosted-invoice/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "Bind the fixed PR1122 10652-ADD candidate and PR1311 semantic bridge to a fresh nine-stage whole-helper hosted emission, owner audit and complete invoice, using the inherited frozen selection.", + "scope_change_reason": "PR1194 and PR1311 already discharge the replacement H2/K implication and PR1122 supplies native evidence; their explicit next obligation is the full changed-word hosted invoice.", + "bottleneck_link": "Discharges the named finite hosted-emission/invoice handoff for the fixed helper-mixing word. Fewer ADDs and smaller unrounded precision bounds leave the paid recursive profile and selected kappa unchanged.", + "budget_minutes": 60, + "stop_rule": "One fixed word and nine-stage frozen hosting assignment only. Stop after the scoped native/hosting checks and invoice; if a material check fails, retain the exact negative handoff. Reserve the last 15 minutes of the 60-minute session for replay and delivery.", + "outcome": "completed", + "evidence": "RESULT.json: 10652 local ADDs, 3911328 emitted instructions, 126432 hosted helper occurrences, zero banks, 904896 paid children, 176/390-bit prefix/two-level bounds charged at 192/512. Native 883/1327-column checks, 17 parent/16 hosted controls and seven receipt-binding controls. Paid bit moment remains PR589.", + "author": "Matthieu Pascal (@mtpsl)", + "ai_assistance": "Substantial OpenAI Codex assistance in implementation, checking and documentation; no independent human review claimed.", + "open_questions": [ + { + "question": "Should the fixed PR1122 word be admitted as a maintained supplier using the semantic-D contract?", + "why_it_matters": "The scalar replacement, native replay and finite hosted invoice now have bound evidence, but admission still requires explicit acceptance of inherited realization and interface assumptions.", + "first_step": "Review PR1194/PR1311 alongside this complete emitted-word receipt; if accepted, integrate the exact source chain through the normal supplier-review process.", + "blocked_by": "Maintainer acceptance and inherited all-size/compiler, common-label, physical hosting, precision/tape, exact recovery and analytic obligations. No exponent advantage motivates automatic selection." + } + ], + "assignment_seed": 1, + "candidate_comparison": [ + { + "scope": "Source-supported joint helper deletion", + "decision": "Not selected: active Discussion1785 covers physical batch schedules." + }, + { + "scope": "Target-feedback 3x4 or 4x4 compensation census", + "decision": "Not selected: PR1557 and PR1706 already certify these domains." + }, + { + "scope": "PR1122/PR1311 complete hosted invoice", + "decision": "Selected: explicitly open handoff; no matching active PR/discussion in the complete 459-PR/432-Discussion snapshot." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1796", + "final_overlap": { + "searched_at": "2026-10-14T10:27:53.760866+00:00", + "open_prs": 465, + "discussions": 444, + "complete_pagination": true, + "warnings": [], + "result": "No matching hosted-invoice contribution found beyond this claim and predecessor handoffs. PR1802 concerns the selected complex private-centre adapter, a different object. Also searched exact candidate digest and 10652/10,652 aliases. Literal search is not a novelty proof." + } +} diff --git a/research/r439-abc-hosted-invoice/VALIDATION.json b/research/r439-abc-hosted-invoice/VALIDATION.json new file mode 100644 index 0000000000..fa4dce8c7c --- /dev/null +++ b/research/r439-abc-hosted-invoice/VALIDATION.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "date_utc": "2026-10-14", + "platform": "macOS-26.6.2-arm64-arm-64bit", + "python": "3.12.3", + "compiler": "Apple clang version 21.0.0 (clang-2100.1.1.101)", + "boost": "1.85.0", + "boost_archive_sha256": "7009fe1faa1697476bdc7027703a2badb84e849b7b0baad5086b087b971f8617", + "requirements": { + "numpy": "2.2.1", + "sympy": "1.14.0", + "scipy": "1.17.0" + }, + "checks": [ + { + "command": "BOOST_INCLUDE=/path/to/boost_1_85_0 python3 -B research/r439-abc-hosted-invoice/verify.py --output /fresh/external/directory", + "result": "PASS_R439_ABC_HOSTED_INVOICE ADDs=10652 helpers=126432 banks=0 no_new_kappa", + "receipt_comparison": "complete canonical JSON equality with RESULT.json; seven binding controls reject" + }, + { + "command": "python3 -B scripts/research_package.py --package research/r439-abc-hosted-invoice --check-only", + "result": "PASS_PACKAGE_METADATA_AND_PINS" + }, + { + "command": "python3 -B research/r439-bsection-stars-seed01/verify.py", + "result": "PASS_R439_BSECTION_STARS blocks=10 gates=388->254 ADDs=11783->11515->11500 guard_rejections=24->0 columns=661 controls=8 no_new_kappa" + }, + { + "command": "python3 -B scripts/research_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + } + ], + "unrun": [ + "selected cold replay", + "current outer assembly", + "eleven-stage hosting", + "generic hook full replay (its exact registered verifier was run directly)", + "proof-assistant or all-size physical proof" + ] +} diff --git a/research/r439-abc-hosted-invoice/VERIFY.json b/research/r439-abc-hosted-invoice/VERIFY.json new file mode 100644 index 0000000000..9e27f59c13 --- /dev/null +++ b/research/r439-abc-hosted-invoice/VERIFY.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.2.1", + "sympy==1.14.0", + "scipy==1.17.0" + ], + "inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/e8-bit-carrier-skeleton/code/bit/independent/checkword.py", + "research/e8-bit-carrier-skeleton/code/bit/independent/relax.py", + "research/e8-bit-carrier-skeleton/code/bit/mutate_records.py", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "research/e8-bit-carrier-skeleton/code/eleven/assemble.py", + "research/e8-bit-carrier-skeleton/code/eleven/audit.py", + "research/e8-bit-carrier-skeleton/code/eleven/emit.py", + "research/e8-bit-carrier-skeleton/code/eleven/local_audit.py", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/base_two_moment.py", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/outer.py", + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/geometry.py", + "research/e8-bit-carrier-skeleton/code/nine/geometry.py", + "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz", + "research/e8-bit-carrier-skeleton/data/complex-b.json", + "research/e8-bit-carrier-skeleton/data/eleven/residual-isometries.json", + "research/e8-bit-carrier-skeleton/discovery/host_select.py", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h", + "research/e8-bit-p111-tuned/code/adapt9p.py", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-p111-tuned/data/selection9-p111.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/tune/verify.sh", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/adapt.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_parent_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/bank_routes_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/hosting_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/bank_routes.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/config.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/e8core.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/base_two_moment.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/moment.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/outer.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/tile_m.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py", + "research/e8-bit-p111-tuned/vendor/pr545/code/adapt.py", + "research/r439-abc-semantic-bridge/README.md", + "research/r439-abc-semantic-bridge/RESULT.json", + "research/r439-abc-semantic-bridge/SOURCES.json", + "research/r439-abc-semantic-bridge/inputs/candidate.json.gz", + "research/r439-abc-semantic-bridge/verify.py", + "research/r439-abc-star-composition/README.md", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-semantic-d-contract-seed10/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Semantic-D bridge; fresh native 5/9-stage columns and controls; geometry, full nine-stage emission and owner audit; exact bit invoice and seven receipt-binding mutations." + } + ] +} diff --git a/research/r439-abc-hosted-invoice/invoice.py b/research/r439-abc-hosted-invoice/invoice.py new file mode 100644 index 0000000000..e7839ca552 --- /dev/null +++ b/research/r439-abc-hosted-invoice/invoice.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""Bit-only nine-stage invoice, adapted from PR510 assemble9.py. + +Arithmetic and moment engines: DreamingOfClouds/PR510, the PR463/493 chain, +and their disclosed AI assistance. Apache-2.0. This omits only the unrelated +cited complex/outer assembly loop. Matthieu Pascal, with OpenAI Codex assistance. +""" +import ast +import importlib.util +import json +from fractions import Fraction as Q +from pathlib import Path +import sys + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def compute(root, work): + read = lambda p: json.loads(p.read_text()) + pg = read(work / 'v9/nine/GLOBAL.json') + bg = read(work / 'v9/hosted/GLOBAL.json') + audit = read(work / 'v9/hosted/AUDIT.json') + geo = read(work / 'v9/nine/GEOMETRY.json') + need(audit['status'] == 'PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT', 'hosted audit') + need(audit['template_sha256'] == bg['template_sha256'], 'audited template') + P = {int(r): n for r, n in audit['profile'].items()} + m, W, T, R, V = bg['m'], audit['live'], pg['replicas'], pg['R'], pg['v'] + L = (m - 1) // 7 + K, depth = (L - 1) // 2, bg['halving_depth'] + E = sum(P.values()) + mass = sum(r * n for r, n in P.items()) + need((m, T, R, V, L, W, depth) == (64, 32, 439, 111, 9, 28416, 2), 'fixed model') + need(m * W - mass == audit['deficit'] == T * (2 * K * V - L * 63), 'rank mass') + physical, d, N = W + 9, m * m, 2 * m + unit = L * T * pg['local_additions'] + pg['bridge_additions'] + J = 8 * T * L * (2 * V + R) + 8 * (2 * K * V * T) + 2 * L * T * R + 2 * pg['copy_erase_episodes'] + high, good, compiler = 16 * (d + 1) ** 2, 8 * m * m + 8, 128 * N ** 3 + selectors = 2 * L * T * ((W - 1) + R * m * (geo['max_route_factors'] + 144 + 2 + (m - 1) + m)) + prefix = int(pg['global_prefix_bound']) + charged_prefix = 64 * ((prefix.bit_length() + 63) // 64) + terms = dict(scalar_additions=unit, high_precision=J * high, physical_store=J * physical, + child_compiler=E * (good + compiler), addresses=16 * m ** 3, + copy_erase=pg['copy_erase_episodes'], selectors=selectors, prefix=prefix, constant=1) + coefficient = sum(terms.values()) + two = (coefficient + 1) ** depth * (E + 1) ** depth + charged_two = 512 if two.bit_length() <= 512 else 64 * ((two.bit_length() + 63) // 64) + row = depth * (m * m + 1) + 9909 + 252 + need(prefix < 1 << 192 and charged_prefix == 192, 'nine-stage precision') + need(two < 1 << 512 and charged_two == 512, 'two-level precision') + need(2 * max(P) ** depth < m ** depth and row == 18355 < 20161, 'child and row guards') + engines = root / 'research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines' + def load(name): + spec = importlib.util.spec_from_file_location(name, engines / (name + '.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + M, Other = load('moment'), load('base_two_moment') + enclosure = M.certify(P, m, W, True) + c, chi = Q(enclosure['lower']), Q(enclosure['upper']) + need(c == Q(1733427039589844234749, 10**24), 'unchanged PR589 bit moment') + fallback = 32 * m * m * E + lo, hi = Other.moment(m, W, list(P.items()), c) + bl, bh = Other.moment(m, W, [(1, fallback)], c) + lo2, hi2 = Other.moment(m, W, list(P.items()), chi) + bl2, bh2 = Other.moment(m, W, [(1, fallback)], chi) + need(hi + bh / 10**16 < 1 < lo2 + bl2 / 10**16, 'moment grid brackets') + result = dict(profile={str(k): v for k, v in sorted(P.items())}, paid_calls=E, + live=W, physical=physical, rank_mass=mass, deficit=audit['deficit'], + bit_lower=str(c), next_grid_point_rejected=str(chi), invoice_terms=terms, + J=J, coefficient=coefficient, two_level_coefficient=two, + prefix_bits=prefix.bit_length(), charged_prefix_bits=charged_prefix, + coefficient_bits=coefficient.bit_length(), two_level_bits=two.bit_length(), + charged_two_level_bits=charged_two, row_coefficient=row, + maxchild=max(P), halving_depth=depth, new_kappa=False) + # Execute every statement of the unchanged adapted PR510 bit-invoice + # prelude, stopping immediately after its `res` assignment. Its subsequent + # loop assembles historical complex suppliers and is outside this task. + reference = work / 'a9p/assemble9.py' + tree = ast.parse(reference.read_text(), filename=str(reference)) + stops = [i for i, node in enumerate(tree.body) if isinstance(node, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == 'res' for t in node.targets)] + need(len(stops) == 1, 'reference bit-invoice boundary') + tree.body = tree.body[:stops[0] + 1] + argv = sys.argv + namespace = {'__name__': 'reference_bit_invoice'} + try: + sys.argv = [str(reference), str(work / 'v9'), str(work / 'v9/hosted'), + str(work / 'v9/hosted/AUDIT.json'), + str(root / 'research/e8-bit-carrier-skeleton'), str(work / 'unused.json'), ''] + exec(compile(tree, str(reference), 'exec'), namespace) + finally: + sys.argv = argv + ref = namespace['res'] + need(ref['bit_profile'] == result['profile'] and ref['bit_lower'] == result['bit_lower'] + and ref['next_grid_point_rejected'] == result['next_grid_point_rejected'], 'reference moment') + for key in ('prefix_bits', 'charged_prefix_bits', 'coefficient_bits', 'row_coefficient'): + need(ref['bit'][key] == result[key], 'reference invoice ' + key) + need(namespace['coefficient'] == coefficient and namespace['two'] == two + and namespace['unit'] == unit and namespace['J'] == J + and namespace['selectors'] == selectors, 'reference exact invoice integers') + result['unchanged_reference_bit_invoice_agrees'] = True + return result + + +if __name__ == '__main__': + root, work, out = map(Path, sys.argv[1:]) + out.write_text(json.dumps(compute(root, work), indent=2) + '\n') + print('PASS_R439_ABC_BIT_INVOICE') diff --git a/research/r439-abc-hosted-invoice/invoke.py b/research/r439-abc-hosted-invoice/invoke.py new file mode 100644 index 0000000000..74bc7c640a --- /dev/null +++ b/research/r439-abc-hosted-invoice/invoke.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python3 +"""Inventory reads while running an unchanged Python entry point. + +Matthieu Pascal, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import atexit +import importlib.util +import json +from pathlib import Path +import runpy +import sys + +root, destination, script = map(lambda x: Path(x).resolve(), sys.argv[1:4]) +args = sys.argv[4:] +seen = set() + + +def audit(event, args): + if event != 'open' or not isinstance(args[0], (str, bytes)): + return + path = Path(args[0].decode() if isinstance(args[0], bytes) else args[0]) + if path.suffix == '.pyc': + try: + path = Path(importlib.util.source_from_cache(str(path))) + except ValueError: + return + path = path.resolve() + if path.is_relative_to(root) and path.is_file(): + seen.add(path.relative_to(root).as_posix()) + + +atexit.register(lambda: destination.write_text(json.dumps(sorted(seen), indent=2) + '\n')) +sys.addaudithook(audit) +sys.argv = [str(script), *args] +sys.path.insert(0, str(script.parent)) +runpy.run_path(str(script), run_name='__main__') diff --git a/research/r439-abc-hosted-invoice/verify.py b/research/r439-abc-hosted-invoice/verify.py new file mode 100644 index 0000000000..bec1d4f565 --- /dev/null +++ b/research/r439-abc-hosted-invoice/verify.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Fresh fixed-word nine-stage hosting replay; no synthesis or outer assembly. + +Orchestration follows PR589 tune/verify.sh, using unchanged exporters, native +checkers, parameterizers, emitter and owner auditors. Apache-2.0. +Matthieu Pascal, with substantial OpenAI Codex assistance. +""" +import argparse +import gzip +import hashlib +import json +import os +from pathlib import Path +import shlex +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P = ROOT / 'research/e8-bit-carrier-skeleton' +PKG = ROOT / 'research/e8-bit-p111-tuned' +WORD = ROOT / 'research/r439-abc-semantic-bridge/inputs/candidate.json.gz' +V510 = PKG / 'vendor/pr510/e8-r480-nine-stage' +VK = V510 / 'vendor/e8-r715-eleven-stage-whole/code' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + def unique(rows): + result = {} + for key, value in rows: + need(key not in result, 'duplicate JSON key') + result[key] = value + return result + return json.loads(path.read_text(), object_pairs_hook=unique, + parse_constant=lambda _: (_ for _ in ()).throw(ValueError('nonfinite JSON'))) + + +def canonical(x): + return json.dumps(x, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def replay(work, discover=False): + pins = read(HERE / 'SOURCES.json') + inputs = {r['path']: r['sha256'] for r in pins['files'] if r['usage'] == 'input'} + for name, expected in inputs.items(): + need(sha(ROOT / name) == expected, 'source hash: ' + name) + need(not work.is_relative_to(ROOT), 'output must be outside checkout') + work.mkdir(parents=True, exist_ok=False) + (work / 'logs').mkdir() + (work / 'bin').mkdir() + consumed = set() + commands = [] + + def run(name, args): + args = list(map(str, args)) + print(name, flush=True) + commands.append(args) + with (work / 'logs' / (name + '.log')).open('x') as log: + subprocess.run(args, stdout=log, stderr=subprocess.STDOUT, check=True, timeout=600) + + def python(name, script, *args): + reads = work / 'logs' / (name + '.inputs.json') + run(name, [sys.executable, '-I', '-B', HERE / 'invoke.py', ROOT, reads, script, *args]) + consumed.update(read(reads)) + + python('semantic-bridge', ROOT / 'research/r439-abc-semantic-bridge/verify.py') + python('export', P / 'code/bit/export_records.py', WORD, work / 'records') + python('stage', P / 'code/bit/regression/stage_cohort.py', work / 'records', work / 'records', work / 'cin', work / 'cout') + checker = P / 'code/bit/checkers' + flags = shlex.split(os.environ.get('CXX', 'c++')) + ['-O2', '-std=c++17', '-DHDIM=8', '-DNCOPY=9', + '-I' + str(P / 'portable-include'), '-I' + str(checker), '-I' + os.environ.get('BOOST_INCLUDE', '/usr/include')] + for name, source, more in [('legality', 'legality_h.cpp', []), + ('columns5', 'columns_k.cpp', ['-DVPORTS=111', '-DRHELP=439', '-DKPAIRS=2']), + ('columns9', 'columns_k.cpp', ['-DVPORTS=111', '-DRHELP=439', '-DKPAIRS=4'])]: + dep = work / 'logs' / (name + '.d') + run('compile-' + name, flags + more + ['-MMD', '-MF', dep, '-o', work / 'bin' / name, checker / source]) + # Make dependency files escape spaces; shlex decodes their path tokens. + for token in shlex.split(dep.read_text().replace('\\\n', ' ').split(':', 1)[1]): + path = Path(token).resolve() + if path.is_relative_to(ROOT): + consumed.add(path.relative_to(ROOT).as_posix()) + run('legality', [work / 'bin/legality', work / 'cin', work / 'cout', work / 'cout/legality.json']) + run('columns5', [work / 'bin/columns5', work / 'cout/COHORT249-RECORDS.bin', work / 'cout/columns.json']) + run('columns9', [work / 'bin/columns9', work / 'cout/COHORT249-RECORDS.bin', work / 'cout/columns9.json']) + python('geometry-adapter', PKG / 'vendor/pr545/code/adapt.py', P, WORD, work / 'ad545') + python('geometry', work / 'ad545/nine_geometry.py', '--source', P, '--out', work / 'v9/nine', '--word', WORD) + # The inherited geometry certificate includes elapsed time in its hash. + # Normalize that nonmathematical field before any downstream binding. + geometry_path = work / 'v9/nine/GEOMETRY.json' + geometry = read(geometry_path) + geometry['seconds'] = 0 + geometry_path.write_text(json.dumps(geometry, indent=2) + '\n') + python('parent-adapter', V510 / 'code/adapt.py', VK, work / 'adapted9') + python('port-adapter', PKG / 'code/adapt9p.py', VK, V510 / 'code', work / 'adapted9/audit_parent_k.py', work / 'a9p') + (work / 'v9/records').symlink_to(work / 'records', target_is_directory=True) + python('parent-template', work / 'a9p/global_k.py', '--word', WORD, '--local-check', work, + '--out', work / 'v9/nine', '--isometries', P / 'data/eleven/residual-isometries.json') + python('parent-audit', work / 'a9p/audit_parent_k.py', '--local-check', work, '--out', work / 'v9/nine', '--word', WORD) + python('hosted-emission', work / 'a9p/emit_k.py', work / 'v9/nine', work, work / 'v9/hosted', + '--selection', PKG / 'data/selection9-p111.json', '--key', 'bit') + python('hosted-audit', work / 'a9p/audit_hosted_k.py', work / 'v9', work / 'v9/hosted', work / 'v9/hosted/AUDIT.json') + python('invoice', HERE / 'invoice.py', ROOT, work, work / 'INVOICE.json') + consumed -= {p for p in consumed if p.startswith('research/r439-abc-hosted-invoice/')} + (work / 'CONSUMED.json').write_text(json.dumps(sorted(consumed), indent=2) + '\n') + (work / 'commands.json').write_text(json.dumps(commands, indent=2) + '\n') + if not discover: + need(consumed <= set(inputs), 'undeclared consumed inputs: ' + repr(sorted(consumed - set(inputs)))) + result = collect(work) + result['binding_controls'] = controls(work) + (work / 'RESULT.json').write_text(json.dumps(result, indent=2) + '\n') + return result + + +def collect(work): + """Bind fresh producer/auditor outputs, with no generation or mutation.""" + legality = read(work / 'cout/legality.json') + columns = [read(work / 'cout' / p) for p in ('columns.json', 'columns9.json')] + parent = read(work / 'v9/nine/GLOBAL.json') + pa = read(work / 'v9/nine/AUDIT.json') + hosted = read(work / 'v9/hosted/AUDIT.json') + hg = read(work / 'v9/hosted/GLOBAL.json') + invoice = read(work / 'INVOICE.json') + for folder, receipt in [('nine', parent), ('hosted', hg)]: + blob = gzip.decompress((work / 'v9' / folder / 'GLOBAL-TEMPLATE.json.gz').read_bytes()) + need(hashlib.sha256(blob).hexdigest() == receipt['template_sha256'], 'template bytes ' + folder) + need(pa['status'] == 'PASS_INDEPENDENT_COMPRESSED_BIT_TEMPLATE_AUDIT' + and pa['template_sha256'] == parent['template_sha256'], 'parent audit binding') + need(hg['parent_template_sha256'] == parent['template_sha256'] + and hosted['template_sha256'] == hg['template_sha256'], 'hosted audit binding') + need(hosted['status'] == 'PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT', 'hosted status') + for key in ('emitted_program_sha256', 'emitted_events', 'profile', 'live', 'physical', + 'hosted_residuals', 'bank_assignments', 'rank_mass', 'deficit', 'maxchild'): + need(hosted[key] == hg[key], 'hosted receipt mismatch: ' + key) + for key in ('profile', 'live', 'physical', 'rank_mass', 'deficit', 'maxchild'): + need(invoice[key] == hosted[key], 'invoice ownership mismatch: ' + key) + need(invoice['paid_calls'] == sum(hosted['profile'].values()), 'invoice paid calls') + need(invoice['invoice_terms']['prefix'] == int(parent['global_prefix_bound']), 'invoice prefix binding') + need(invoice['invoice_terms']['copy_erase'] == parent['copy_erase_episodes'] == 2592, 'invoice copy binding') + need(invoice['invoice_terms']['scalar_additions'] == 288 * 10652 + parent['bridge_additions'], 'invoice scalar binding') + need(len(pa['mutations_rejected']) == 17 and len(hosted['mutations_rejected']) == 16, 'audit control coverage') + need(legality['common_frame_ADDs'] == parent['local_additions'] == 10652, 'changed scalar bill') + need(legality['copies'] == legality['erasures'] == 9 and legality['rank_mass'] == 5129, 'local copy/rank bill') + need(hosted['hosted_residuals'] == 126432 and hosted['bank_assignments'] == 0, 'complete hosting') + need(hosted['emitted_events'] == 288 * legality['records'], 'all local instructions emitted') + for col, count, controls in zip(columns, (883, 1327), (6, 18)): + need(col['formal_columns_checked'] == count and col['local_scalar_additions'] == 10652, 'native column binding') + need(col['payload_prefix_bits'] == 92 and len(col['negative_controls']) == controls + and all(c['rejected'] is True for c in col['negative_controls']), 'native guard/controls') + result = dict(schema_version=1, word_sha256=sha(WORD), semantic_bridge_receipt_sha256=sha(ROOT / 'research/r439-abc-semantic-bridge/RESULT.json'), + records_sha256=sha(work / 'records/249-records.bin'), + native={k: legality[k] for k in ('status', 'records', 'common_frame_ADDs', 'rank_mass', 'paid_histogram', 'copies', 'erasures')}, + stages=[{k: c[k] for k in ('formal_columns_checked', 'local_scalar_additions', 'bridge_additions', 'signed_lift_prefix', 'payload_prefix_bits', 'payload_prefix_upper', 'negative_controls')} for c in columns], + parent={k: parent[k] for k in ('template_sha256', 'source_records_sha256', 'word_sha256', 'local_additions', 'global_prefix_bound', 'global_prefix_bits', 'charged_prefix_bits', 'independent_unbanked_scalar_columns', 'copy_erase_episodes', 'bridge_additions')}, + parent_controls=pa['mutations_rejected'], hosted=hosted, invoice=invoice, + no_selected_change=True, new_kappa=False) + need(result['parent']['word_sha256'] == result['word_sha256'], 'word-to-template binding') + need(result['parent']['source_records_sha256'] == result['records_sha256'], 'record-to-template binding') + return result + + +def controls(work): + """Reject mixed or understated receipts at the actual collection boundary.""" + cases = [ + ('wrong-word', 'v9/nine/GLOBAL.json', lambda x: x.__setitem__('word_sha256', '0' * 64), 'word-to-template'), + ('wrong-records', 'v9/nine/GLOBAL.json', lambda x: x.__setitem__('source_records_sha256', '0' * 64), 'record-to-template'), + ('invoice-profile', 'INVOICE.json', lambda x: x['profile'].__setitem__('1', x['profile']['1'] - 1), 'invoice ownership'), + ('invoice-prefix', 'INVOICE.json', lambda x: x['invoice_terms'].__setitem__('prefix', x['invoice_terms']['prefix'] // 2), 'invoice prefix'), + ('invoice-copy', 'INVOICE.json', lambda x: x['invoice_terms'].__setitem__('copy_erase', x['invoice_terms']['copy_erase'] - 1), 'invoice copy'), + ('missing-bridge-control', 'cout/columns9.json', lambda x: x['negative_controls'].pop(), 'native guard/controls'), + ('stale-hosted-template', 'v9/hosted/GLOBAL.json', lambda x: x.__setitem__('parent_template_sha256', '0' * 64), 'hosted audit binding'), + ] + rejected = [] + for name, relative, mutate, reason in cases: + path = work / relative + original = path.read_bytes() + altered = read(path) + mutate(altered) + try: + path.write_text(json.dumps(altered) + '\n') + try: + collect(work) + except ValueError as exc: + need(reason in str(exc), 'unexpected control rejection: ' + str(exc)) + rejected.append(name) + else: + raise ValueError('accepted control: ' + name) + finally: + path.write_bytes(original) + return rejected + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path, help='fresh directory outside checkout; preserve logs') + parser.add_argument('--write', action='store_true', help='regenerate the deterministic receipt') + parser.add_argument('--discover-inputs', action='store_true', help='draft-only dependency inventory') + args = parser.parse_args() + need(not args.discover_inputs or read(HERE / 'VERIFY.json')['status'] == 'draft', 'discovery requires draft manifest') + if args.output: + result = replay(args.output.resolve(), args.discover_inputs) + else: + with tempfile.TemporaryDirectory(prefix='r439-abc-hosted-') as tmp: + result = replay(Path(tmp) / 'run', args.discover_inputs) + if args.write: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2) + '\n') + elif not args.discover_inputs: + need(canonical(result) == canonical(read(HERE / 'RESULT.json')), 'deterministic receipt differs') + print('PASS_R439_ABC_HOSTED_INVOICE ADDs=10652 helpers=126432 banks=0 no_new_kappa') + + +if __name__ == '__main__': + main()