From 66de747e597cc1509edaf486d9df8a46061164e8 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:36:52 +0530 Subject: [PATCH 1/2] Research: batch JP8 backward cleanup with reverse Horner --- research/complex-jp8-fanin/CLAIM.md | 19 ++ research/complex-jp8-fanin/EXPECTED.json | 116 +++++++++ research/complex-jp8-fanin/PROOF.md | 150 +++++++++++ research/complex-jp8-fanin/README.md | 122 +++++++++ research/complex-jp8-fanin/SOURCES.json | 40 +++ research/complex-jp8-fanin/VALIDATION.md | 73 ++++++ research/complex-jp8-fanin/check_columns.py | 116 +++++++++ research/complex-jp8-fanin/lowering.py | 85 +++++++ research/complex-jp8-fanin/verify.py | 265 ++++++++++++++++++++ 9 files changed, 986 insertions(+) create mode 100644 research/complex-jp8-fanin/CLAIM.md create mode 100644 research/complex-jp8-fanin/EXPECTED.json create mode 100644 research/complex-jp8-fanin/PROOF.md create mode 100644 research/complex-jp8-fanin/README.md create mode 100644 research/complex-jp8-fanin/SOURCES.json create mode 100644 research/complex-jp8-fanin/VALIDATION.md create mode 100644 research/complex-jp8-fanin/check_columns.py create mode 100644 research/complex-jp8-fanin/lowering.py create mode 100644 research/complex-jp8-fanin/verify.py diff --git a/research/complex-jp8-fanin/CLAIM.md b/research/complex-jp8-fanin/CLAIM.md new file mode 100644 index 0000000000..e260ca1129 --- /dev/null +++ b/research/complex-jp8-fanin/CLAIM.md @@ -0,0 +1,19 @@ +# Complex supplier claim, seed 27 + +- Assignment: OS randomness returned 27 on 2026-10-13 at 04:52 UTC. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Track: complex supplier. Seed parity selects JP8; the distinct object is its backward common-target coefficient runs. +- Hypothesis: forming a signed source sum in one private stream, then using reverse Horner to accumulate its common dyadic multiple, reduces the fully charged cost of backward JP8 additions. The stream must be cleared at the block boundary and every live register must retain its exact map. +- Method: exhaust all maximal contiguous additions with the same target and non-unit coefficient magnitude in the pinned backward program. Price source accumulation, Horner preparation, signed target update and both clears before emitting a replacement. Keep only strictly cheaper blocks. Check exact rational maps and prefix bounds. +- Deliverable: one finite circuit research package, source pins, reproducible verifier, exact cost certificate, negative controls and scoped proof. No new kappa claim. +- Expected finish: 2026-10-13 05:42 UTC, 11:12 IST. Reserve the final quarter for verification and handoff. + +Three candidate tasks were considered: further single-coefficient recoding, CK fixed-boundary frame optimization, and backward JP8 common-target coefficient batching. The first two overlap #723/#696 and #698. The third changes the sharing direction and needs a separate workspace and prefix argument from #722, whose backward scan found no common-source run. + +No pinned coordination issue exists; the only open issue is #650 about Discussions. This local claim follows an open-PR review through #725. Related #681, #696, #719, #722 and #723 were inspected. Delegated work stays within this common-target batching experiment. + +Acceptance requires a positive fully priced saving, exact maps including arbitrary private inputs, charged restoration, preserved source access, an explicit prefix bound, deterministic evidence and meaningful rejection controls. The selected certificate, supplier sources, global accounting, upstream directory and unrelated artifacts stay unchanged. + +During optimistic pricing, the initial two-stream recipe was simplified to one stream. Halve the signed source sum first, then scan numerator bits from least to most significant, accumulating into the target at each set bit and doubling the work stream between bits. This is the transpose direction of binary Horner sharing. It needs no added private register and explicitly credits the related forward construction in #722. + +Prepared for Sagar Thakrar, @thakrarsagar, with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/complex-jp8-fanin/EXPECTED.json b/research/complex-jp8-fanin/EXPECTED.json new file mode 100644 index 0000000000..f463968e21 --- /dev/null +++ b/research/complex-jp8-fanin/EXPECTED.json @@ -0,0 +1,116 @@ +{ + "arbitrary_private_inputs": 9, + "controls": [ + "missing_entry_clear", + "missing_exit_clear", + "missing_source_read", + "missing_halving", + "missing_doubling", + "wrong_source_sign", + "missing_target_accumulation", + "cost_inflation", + "target_alias", + "frame_boundary", + "non_dyadic", + "endpoint_neutral_prefix_excursion" + ], + "live_columns": 716, + "orientations": { + "backward": { + "after": { + "additions": 3022, + "batch_sha256": "d547f02051f833202549364ed8574ecaef5466d45ed4137690b4ba155eb868cf", + "batches": 999, + "length_histogram": { + "2": 536, + "3": 235, + "4": 70, + "5": 69, + "6": 43, + "7": 29, + "8": 6, + "9": 5, + "10": 3, + "11": 1, + "12": 1, + "13": 1 + }, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "prefix_bits": 101, + "prefix_l1": "16753412757380464429924108070201913461/8388608", + "real_primitives": 237592, + "scratch_prefix_l1": "5584470698695991139513971864792267243/4194304" + }, + "before": { + "additions": 0, + "batch_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "batches": 0, + "length_histogram": {}, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "prefix_bits": 101, + "prefix_l1": "16753412757380464429924108070201913461/8388608", + "real_primitives": 257280, + "scratch_prefix_l1": "0" + }, + "real_saved": 19688 + }, + "forward": { + "after": { + "additions": 0, + "batch_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "batches": 0, + "length_histogram": {}, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "prefix_bits": 64, + "prefix_l1": "4536094588619580433782972610869617/281474976710656", + "real_primitives": 257232, + "scratch_prefix_l1": "0" + }, + "before": { + "additions": 0, + "batch_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "batches": 0, + "length_histogram": {}, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "prefix_bits": 64, + "prefix_l1": "4536094588619580433782972610869617/281474976710656", + "real_primitives": 257232, + "scratch_prefix_l1": "0" + }, + "real_saved": 0 + } + }, + "status": "PASS_JP8_REVERSE_HORNER_FANIN" +} diff --git a/research/complex-jp8-fanin/PROOF.md b/research/complex-jp8-fanin/PROOF.md new file mode 100644 index 0000000000..153ced6b59 --- /dev/null +++ b/research/complex-jp8-fanin/PROOF.md @@ -0,0 +1,150 @@ +# JP8 backward fan-in in the full-frame cleanup + +The construction replaces 999 maximal runs in the pinned JP8 backward local +program. Each run consists of consecutive additions to one target, with one +non-unit coefficient magnitude. The replacement uses one existing coefficient +work stream and saves 19,688 real-component arithmetic operations. It preserves +the exact block map and the full program's charged prefix envelope. + +The scope is `full_frame_cleanup`, frame 1, with live-register sources and +targets. Other phases and forward JP8 stay unchanged. This is a finite local +arithmetic result. It does not replace the selected supplier certificate or +claim a new global kappa bound. + +## Inputs and relationship to prior work + +The source program and canonical word are the JP8 files under +`research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/`. +The original coefficient price is the binary-Horner rule in +`research/complex-k492-owner-repair/code/invoice_allcold.py` and its inherited +`emit_local.py`. The package pins those repository inputs rather than depending +on an open pull request. + +The description and metadata of [PR #722](https://github.com/CrocSwap/integer-mult-bounds/pull/722) +were inspected at `a0766ab0fab379e1997fadc3ca157578d57986c1`. +It is a conceptual predecessor for sharing coefficient preparation across a +contiguous run; its implementation was not independently reviewed here. +Its reported common-source scan and +this common-target construction have different access and workspace arguments. +This construction collects sources into one work stream and emits the binary +coefficient into the target, so a second temporary stream is unnecessary. + +## Exact block map + +Write a run of length `g >= 2` as + +```text +target += epsilon_i * n / 2^k * source_i, i = 1,...,g +``` + +Here `n > 0`, `k >= 0`, and `epsilon_i` is either sign. The fraction is in +lowest terms. No source is the target. Sources need not have independent +values, because the argument is an identity of linear maps. + +Let `W` be the original coefficient work register for one real component. +The replacement performs the following operations. + +1. Clear `W`. +2. Add each signed source to `W` once. +3. Halve `W` exactly `k` times. +4. Read the bits of `n` from least to most significant. Add `W` to the target + at each set bit and double `W` between successive bit positions. +5. Clear `W`. + +After step 2, `W = S = sum_i epsilon_i * source_i`. At bit position `j`, +`W = 2^j S / 2^k`. The sum accumulated into the target is therefore +`n S / 2^k`, exactly the original update. Every source and every other live +register stays fixed. + +The entry clear removes arbitrary incoming private dirt. The exit clear maps +the work register to zero. The original per-addition Horner lowering has the +same two clear operations, so the block maps agree on the private input column +as well as every live column. This is equality with the original erase-to-zero +semantics, not a claim that arbitrary private dirt is reversibly restored. + +Apply the same real scalar schedule to both components of a complex stream. +The schedule needs only the work register already used by the original +lowering for that component. It does not require two simultaneous complex +temporary streams or an additional physical helper. + +## Access and frame conditions + +Frame 1 has rank 9, equal to the local frame height. The inherited local audit +requires every source and target of a scalar event to be present in that +event's frame. Each selected run has constant frame metadata equal to 1. +All its sources remain unchanged throughout the run, and the target is not +among them. The sources can therefore be read while forming `S` before any +target accumulation. The cleared coefficient register represents the zero +stream in that same frame. + +No replacement crosses a phase event, recursive child, frame change, wrapper, +or scalar operation of a different kind. The recursive schedule and all +source-register lifetimes outside the replaced run are preserved. Restricting +the construction to the full-frame cleanup avoids any additional claim about +temporary representation at a partial frame. + +## Charged arithmetic cost + +Put `b = bit_length(n)` and `p = popcount(n)`. The inherited implementation +charges `3 + (b - 1) + p + k` operations per real component for each addition. +The three operations are the entry clear, target accumulation, and exit clear. + +The replacement charges `g + 2 + k + (b - 1) + p`. It includes all signed +source additions, both clears, every halving and doubling, and every target +addition. Thus the scalar saving is + +```text +g * [3 + (b - 1) + p + k] - [g + 2 + k + (b - 1) + p] + = (g - 1) * [2 + (b - 1) + p + k] > 0. +``` + +The selected 999 runs contain 3,022 original additions. Their cost falls from +18,075 to 8,231 scalar operations. Doubling for the two real components gives +the saving of 19,688. The complete backward arithmetic price falls from +257,280 to 237,592 real-component operations. The forward price remains +257,232. These counts do not alter recursive-child or wrapper charges. + +## Prefix bound + +Use the inherited nonnegative envelope at each block boundary. Let `T` bound +the target and let `A = sum_i E_i`, where `E_i` bounds source `i`. Signed source +accumulation never exceeds `A`. After the halvings and doublings, the largest +possible work-register envelope is + +```text +A * max(1, 2^(b - 1) / 2^k). +``` + +All binary target additions have nonnegative envelope coefficients. Every +target prefix is bounded by `T + n A / 2^k`, the same envelope as the original +block endpoint. The prefix bound accounts for the possibly larger unscaled +source sum when the common coefficient is below one. + +Replaying this rule through the whole pinned backward program, with the +original lowering on every unchanged event, gives the same envelope for both +programs. + +```text +16753412757380464429924108070201913461 / 8388608 < 2^101 +``` + +This stays below the inherited `2^192` local payload allowance. Entry private +columns have envelope one before the first clear and are included in the +initial bound. The construction inherits the original analytic assumptions +for primitive arithmetic and recursive children. It supplies no new global +precision or asymptotic exponent argument. + +## Verification obligations + +The verifier must bind the source bytes, enumerate exactly the stated domain, +emit each charged operation, and compare every block on exact rational basis +columns including the private work input. It must also check the primitive +prefixes and aggregate invoice. An omitted entry clear must fail on private +dirt; an omitted exit clear must fail the final private column check. A changed +source sign, coefficient bit, target, or source must fail map equality when it +changes the block map. Understated arithmetic or workspace claims must be +rejected separately from endpoint equality. + +The package is scoped to these local obligations. It leaves supplier +promotion, outer-bound recomputation, and other candidate run domains for +separate review. diff --git a/research/complex-jp8-fanin/README.md b/research/complex-jp8-fanin/README.md new file mode 100644 index 0000000000..e1c5dff1f5 --- /dev/null +++ b/research/complex-jp8-fanin/README.md @@ -0,0 +1,122 @@ +# One-stream reverse-Horner batching for JP8 cleanup + +This finite complex-supplier circuit result saves **19,688 real-component +primitives in the backward JP8 program**. It replaces 999 contiguous +common-target cleanup runs containing 3,022 additions. The program uses one +existing coefficient-work stream, preserves every live register's boundary map, +and clears arbitrary incoming private work. The complete scalar prefix envelope +stays unchanged at 101 bits, within the inherited 192-bit allowance. + +Status: **research construction / finite circuit improvement, no new kappa**. +The selected #626 conditional result remains +`51110230636731/31250000000000000 = 0.001635527380375392`. + +| JP8 orientation | Original real primitives | Replacement | Saving | +| --- | ---: | ---: | ---: | +| Forward | 257,232 | 257,232 | 0 | +| Backward | 257,280 | 237,592 | 19,688 | + +Every source read, signed accumulation, halving, doubling, and both scratch +clears is included. Recursive children, wrappers, adapters, scalar macro +boundaries outside each batch, and paid frame profiles retain their original +charges. This is an arithmetic invoice reduction, not a runtime benchmark. + +## Reproduce + +From the repository root, using Python 3.11+ and the standard library: + +```sh +python3 -I -B research/complex-jp8-fanin/verify.py +``` + +Expected: + +```text +PASS_JP8_REVERSE_HORNER_FANIN batches=999 additions=3022 real_saved=19688 columns=716 controls=12 +``` + +The check is offline and writes no files. It checks all source payload hashes, +the selected SPEC's semantic identities, full-frame source lifetimes, every +block's exact map including arbitrary work input, and both complete scalar +projections on 716 input columns plus eight centre inputs and one work input. +It recomputes exact costs and positive prefix envelopes and compares +[EXPECTED.json](EXPECTED.json). `--receipt` prints the independently +recomputed evidence without comparing that aggregate receipt. + +An additional implementation uses independent grouping and a flat-vector +column interpreter: + +```sh +python3 -I -B research/complex-jp8-fanin/check_columns.py +``` + +It checks every local input column of all 999 blocks and rejects an omitted +final clear in every block. The main verifier's twelve controls cover missing +initialization/restoration/source reads/halving/doubling/target accumulation, +wrong sign, aliases, frame mismatches, non-dyadic coefficients, inflated cost, +and an endpoint-neutral prefix excursion. + +## Construction and coverage + +For a run `y += sign_i * n/2^k * x_i`, clear `W` and collect the signed sources +in it. Halve `W` `k` times, scan numerator bits from low to high, add `W` to +`y` at each set bit, and double `W` between bit positions. Finally clear `W`. +The [proof](PROOF.md) gives exact maps, frame conditions, costs and prefix bounds. + +The complete domain is maximal contiguous runs of at least two additions in +`full_frame_cleanup`, frame 1, with one live target and equal non-unit +coefficient magnitude. Each source must differ from the target. Every event +outside this class ends a run. Enumeration is exhaustive with no timeout or +sampling; the forward domain is also scanned and has no eligible run. +Other phases and coefficient-sharing classes are outside the claim. No +optimality or impossibility claim follows from this finite enumeration. + +The assignment seed is **27**, generated using OS randomness. The local +[claim](CLAIM.md) records the three candidates, selection and stopping rule. +The exact base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[SOURCES.json](SOURCES.json) records eight payload SHA-256 pins and Git blobs, +the #626 and #622 heads, and the inherited #543 bit dependency. Gzip equality +uses decompressed payload bytes, so container recompression is harmless. + +## Prior work, attribution and limits + +This construction follows the sharing idea in ellipsi2's [#722](https://github.com/CrocSwap/integer-mult-bounds/pull/722), +whose reported forward common-source grouping saves 19,688 primitives and finds +no backward common-source run. This package supplies the backward common-target +dual and its distinct accumulated-source prefix argument. It imports no pending +implementation. The equal saving comes from the transposed run structure; +it is not a claim of independently inventing forward coefficient sharing. +No combined receipt with #722, [#696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) +or [#723](https://github.com/CrocSwap/integer-mult-bounds/pull/723) is asserted. +Concurrent [#739](https://github.com/CrocSwap/integer-mult-bounds/pull/739) +extends forward common-source sharing across coefficient magnitudes; its +reported backward scan has no join in that class. This package adds backward +common-target batching. [#734](https://github.com/CrocSwap/integer-mult-bounds/pull/734) +changes single-coefficient preparation, and [#745](https://github.com/CrocSwap/integer-mult-bounds/pull/745) +independently audits the original JP8 private-centre inputs by reverse replay. +Their descriptions and metadata were inspected, with no imported code or +combined cost claim. Private-input checking here is a verification obligation, +not a priority claim over those contributions. +[#681](https://github.com/CrocSwap/integer-mult-bounds/pull/681) changes factory +macros, and [#719](https://github.com/CrocSwap/integer-mult-bounds/pull/719) +proves a different CK fixed-middle obstruction. + +Credit to Jeremy Kothe's #622 construction and Claude Code contributors, +Chafik Boukhalfa's #626 package, icekylinx's scalar/factory/direct-delivery +lineage, DreamingOfClouds' compiler and cold-helper work, Dugongue, eumemic, +and the retained predecessor notices. Prepared for **Sagar Thakrar, +@thakrarsagar**, with substantial **OpenAI Codex assistance**, including two +separate scoped AI checks. No independent human review is claimed. +New contributions are Apache-2.0 under the repository license. + +The private coefficient stream is zero at each new batch boundary, rather than +after each replaced macro. This is the explicit local interface change. +The package freshly verifies scalar projections, local full-frame access, +costs and envelopes. Native frame/wrapper/phase correctness outside the blocks +is inherited from the pinned supplier evidence. Production-emitter integration, +global invoice/admission regeneration, and any future supplier promotion remain +separate work. All inherited compiler, common-label/mutable-basis realization, +hosting, residual, precision/tape/recovery, bit-supplier and analytic assumptions +remain. This is not a formal proof of the multiplication theorem. + +See [VALIDATION.md](VALIDATION.md) for executed checks and explicit omissions. diff --git a/research/complex-jp8-fanin/SOURCES.json b/research/complex-jp8-fanin/SOURCES.json new file mode 100644 index 0000000000..d988cf60f6 --- /dev/null +++ b/research/complex-jp8-fanin/SOURCES.json @@ -0,0 +1,40 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_pr626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "construction_pr622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "retained_bit_pr543": "2065fe4f72a914d907f1046603f5a36f17018535", + "files": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/CANONICAL-WORD.json.gz": { + "payload_sha256": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b", + "git_blob": "7fd7cd1fefbb8b0e12397b355d9f6e227813bd58" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": { + "payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "git_blob": "e22169a1633638213a5c63425a1919c7185f4c43" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json": { + "payload_sha256": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67", + "git_blob": "0d84d903086993330ddcd871e66b15854f0c3ccd" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json": { + "payload_sha256": "cb2f99ed351925dd35434b73de16f4085884fe81a35a69e1c7ce2d5e96cb975b", + "git_blob": "19a4edfa2091d4cf38db49d7a780d29232badb49" + }, + "research/complex-k492-owner-repair/data/SPEC.json": { + "payload_sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "git_blob": "cdc4f6ce03e96fd1ffc5a19926e1d0d4bce4e9de" + }, + "research/complex-k492-owner-repair/code/invoice_allcold.py": { + "payload_sha256": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "git_blob": "b244cd59940659465c07b013ebe3225077496f45" + }, + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-global/vendor531/code/emit_local.py": { + "payload_sha256": "eefc76e0bee003015fe21ac685c2cce658033d5444add404d2d509c7d6f39bac", + "git_blob": "a54170b0023d467be3da1db9d8623ac4665f0afe" + }, + "certificates/selected-result.json": { + "payload_sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "git_blob": "92a10096dee76479af88a897714b3818d8263141" + } + } +} diff --git a/research/complex-jp8-fanin/VALIDATION.md b/research/complex-jp8-fanin/VALIDATION.md new file mode 100644 index 0000000000..65625cf090 --- /dev/null +++ b/research/complex-jp8-fanin/VALIDATION.md @@ -0,0 +1,73 @@ +# Validation and overlap record + +Validated on macOS arm64, 2026-10-13, with CPython 3.14.8 and 3.11.15. + +```sh +python3 -I -B research/complex-jp8-fanin/verify.py +python3 -I -O -B research/complex-jp8-fanin/verify.py +python3.11 -I -O -B research/complex-jp8-fanin/verify.py +python3.11 -I -O -B research/complex-jp8-fanin/check_columns.py +make selected-record-check +``` + +All passed. The main result is 999 batches, 3,022 additions and 19,688 saved +real primitives, with twelve controls. The independent column checker covers +5,020 local input columns and rejects the omitted final clear in every block. +The independent checker also passed normal and isolated optimized CPython +3.14.8 execution. No Python assertion is required for these checks. + +The original and replacement full scalar projections have the same exact +endpoint on all 716 live columns, eight arbitrary centre inputs and one +arbitrary coefficient-work input. Original complete costs and prefix envelopes +match the pinned source receipts. The replacement backward peak remains +`16753412757380464429924108070201913461/8388608`, or 101 bits. +The selected-record/source-inventory check preserves +`kappa=51110230636731/31250000000000000`. + +Additional in-memory I/O controls monkeypatched only `Path.read_bytes` or +`Path.read_text`, without modifying any source file. Recompressing the exact +program payload with gzip level 1 and timestamp 123 passed source admission. +Changing its `zero_frame_precondition` marker failed the payload pin. Replacing +`EXPECTED.json` with an empty object failed with `receipt mismatch` after the +full computation. The twelve committed controls separately exercise semantic, +cost and prefix obligations. + +Two separately delegated Codex workers checked the narrowly claimed algebra +and implementation. One independently reconstructed all 999 block identities, +complete prices and prefix envelope. The other supplied `check_columns.py` +using a separate grouping method and flat-vector column execution. Their +findings agree. This is scoped AI review, not independent human review. + +## Overlap and dependency check + +The initial open queue through #725 and the negative results #719 and #698 +guided selection. The later queue snapshot contained 566 open PRs through +#747; main remained at `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Descriptions, source heads and file inventories were inspected for the closest +related contributions. Those implementation bytes were not imported or +independently verified here. + +The immediate pre-submission refresh contained 567 open PRs through #748. +The new #748 concerns R420 decoder source cosets and does not overlap this +JP8 backward circuit. The pinned-issue list was still empty. + +| PR | Inspected head | Relationship | +| --- | --- | --- | +| #722 | `a0766ab0fab379e1997fadc3ca157578d57986c1` | Direct sharing predecessor, forward common-source runs | +| #739 | `abb9825202dba6f9bc95c7df8d12d86088fdff1a` | Forward sharing across magnitudes; reports no backward joins | +| #696 | `5a3f983715027c4fd83f50bc9001d4b18463bed1` | Individual macro lowering | +| #723 | `d3bc41b87fc7d23f50d064a0f06f1a89e3ab02a7` | Individual signed-digit lowering | +| #734 | `ba76ba3321d000c8996b0b254bcf0d7260e1bbb6` | Prefix-bounded signed Horner and private-input replay | +| #745 | `fc6ebccca3bd61a6eaf6ec3fcbf2e99d2888c35c` | Independent reverse replay of original JP8 private centres | +| #719 | `a3d9c0aa0a16b68b1f4dd064671ad018013e6dd4` | Fixed-middle CK pair obstruction | +| #681 | `fdc2e4f3c6825530b02143b30deab5de10209479` | Raw factory resynthesis | +| #729 | `deaed262cebc50bdb0c27c6ba132b8f8289b3eef` | Standalone helper-frame lifetime audit | + +## Not executed + +Repository-wide `make verify`, selected cold supplier regeneration, fresh +native wrapper/phase replay, global invoice/admission/assembly regeneration, +Lean and remote Linux CI were not run for this isolated addition. The new +full-frame batches preserve scalar maps and lifetimes; other geometry and +physical/analytic obligations remain inherited. No existing generator, +production emitter, selected certificate, or upstream source was changed. diff --git a/research/complex-jp8-fanin/check_columns.py b/research/complex-jp8-fanin/check_columns.py new file mode 100644 index 0000000000..8c303a3d1a --- /dev/null +++ b/research/complex-jp8-fanin/check_columns.py @@ -0,0 +1,116 @@ +"""Independent grouping and exact column replay of emitted fan-in blocks. + +Sagar Thakrar with substantial OpenAI Codex assistance. Apache-2.0. +Uses the emitter under test and source admission, not their grouping or replay. +""" +from fractions import Fraction +from itertools import groupby +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from lowering import lower +from verify import read_sources + +WORK = ("W", 0) + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def independent_blocks(events): + """Partition the literal event positions, including every hard boundary.""" + labelled = [] + phase = None + for index, event in enumerate(events): + label = None + if event[0] == "phase": + phase = event[1] + if phase == "full_frame_cleanup" and event[0] == "scalar" and event[2] == 1: + op = event[1] + if op[0] == "add": + target, source = tuple(op[1]), tuple(op[2]) + q = abs(Fraction(op[3], op[4])) + if target[0] == source[0] == "L" and target != source and q not in (0, 1): + check(q.denominator & (q.denominator - 1) == 0, "non-dyadic source") + label = (target, q) + labelled.append((label, index)) + for label, run in groupby(labelled, key=lambda item: item[0]): + positions = [index for _, index in run] + if label is not None and len(positions) >= 2: + yield positions[0], positions[-1] + 1 + + +def primitive_column(program, column, positions): + """An input column is one flat vector of scalar register values.""" + values = column.copy() + for instruction in program: + tag = instruction[0] + target = positions[instruction[1]] + if tag == "clear": + check(len(instruction) == 2, "clear arity") + values[target] = Fraction(0) + elif tag == "add": + check(len(instruction) == 4, "add arity") + source, sign = positions[instruction[2]], instruction[3] + check(source != target and sign in (-1, 1), "signed-add contract") + values[target] += sign * values[source] + elif tag in ("double", "half"): + check(len(instruction) == 2, "scale arity") + values[target] *= Fraction(2) if tag == "double" else Fraction(1, 2) + else: + raise ValueError("unknown primitive: " + str(tag)) + return values + + +def check_block(block): + operations = [event[1] for event in block] + registers = sorted({tuple(op[1]) for op in operations} + | {tuple(op[2]) for op in operations} | {WORK}) + positions = {register: index for index, register in enumerate(registers)} + program = lower(block) + check(program[-1] == ("clear", WORK), "missing declared final clear") + rejected_clear_mutation = False + for incoming in range(len(registers)): + column = [Fraction(int(index == incoming)) for index in range(len(registers))] + expected = column.copy() + for op in operations: + target, source = positions[tuple(op[1])], positions[tuple(op[2])] + expected[target] += Fraction(op[3], op[4]) * expected[source] + expected[positions[WORK]] = Fraction(0) + check(primitive_column(program, column, positions) == expected, + "emitted boundary column differs") + if primitive_column(program[:-1], column, positions) != expected: + rejected_clear_mutation = True + check(rejected_clear_mutation, "omitted final clear was undetected") + baseline = 0 + for op in operations: + q = abs(Fraction(op[3], op[4])) + baseline += 3 + q.numerator.bit_length() - 1 + q.numerator.bit_count() + baseline += q.denominator.bit_length() - 1 + check(len(program) < baseline, "block does not save charged work") + return baseline, len(program), len(registers) + + +def main(): + _, programs, _, _ = read_sources() + check(list(independent_blocks(programs["forward"])) == [], "forward inventory changed") + events = programs["backward"] + blocks = list(independent_blocks(events)) + additions = sum(end - start for start, end in blocks) + baseline = lowered = columns = 0 + for start, end in blocks: + old, new, count = check_block(events[start:end]) + baseline += old + lowered += new + columns += count + check((len(blocks), additions, baseline, lowered, columns) + == (999, 3022, 18075, 8231, 5020), "independent inventory or cost differs") + print("PASS_JP8_FANIN_COLUMNS blocks=999 local_columns=5020 " + "real_saved=19688 omitted_clear_rejections=999") + + +if __name__ == "__main__": + main() diff --git a/research/complex-jp8-fanin/lowering.py b/research/complex-jp8-fanin/lowering.py new file mode 100644 index 0000000000..e5fcbe353b --- /dev/null +++ b/research/complex-jp8-fanin/lowering.py @@ -0,0 +1,85 @@ +"""One-stream reverse-Horner batching for full-frame JP8 cleanup. + +Sagar Thakrar with OpenAI Codex assistance. Apache-2.0. +Related forward coefficient sharing: ellipsi2, PR #722. +""" +from fractions import Fraction + +WORK = ("W", 0) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def key(event): + if len(event) != 3 or event[0] != "scalar" or event[2] != 1: + return None + op = event[1] + if op[0] != "add": + return None + target, source = tuple(op[1]), tuple(op[2]) + if target[0] != "L" or source[0] != "L": + return None + q = Fraction(op[3], op[4]) + require(target != source, "source aliases target") + require(q and q.denominator & (q.denominator - 1) == 0, + "coefficient must be nonzero and dyadic") + return (target, abs(q)) if abs(q) != 1 else None + + +def groups(events): + """Maximal literal runs; every non-scalar event is a hard boundary.""" + i, phase = 0, None + while i < len(events): + event = events[i] + if event[0] == "phase": + phase = event[1] + group_key = key(event) if phase == "full_frame_cleanup" else None + if group_key is None: + i += 1 + continue + end = i + 1 + while end < len(events) and key(events[end]) == group_key: + end += 1 + if end - i >= 2: + yield i, end + i = end + + +def lower(block): + """Emit clear, signed add, doubling and halving primitives.""" + require(len(block) >= 2, "batch needs at least two additions") + group_key = key(block[0]) + require(group_key is not None and all(key(e) == group_key for e in block), + "batch must share its target, magnitude and full frame") + target, q = group_key + program = [("clear", WORK)] + for event in block: + op = event[1] + sign = 1 if Fraction(op[3], op[4]) > 0 else -1 + program.append(("add", WORK, tuple(op[2]), sign)) + program.extend(("half", WORK) for _ in range(q.denominator.bit_length() - 1)) + bits = bin(q.numerator)[2:][::-1] + for index, bit in enumerate(bits): + if bit == "1": + program.append(("add", target, WORK, 1)) + if index + 1 < len(bits): + program.append(("double", WORK)) + program.append(("clear", WORK)) + return program + + +def original_cost(op): + """Real-component cost of the selected binary-Horner scalar macro.""" + if op[0] in ("clear", "copy"): + return 2 + q = Fraction(op[3], op[4]) if op[0] == "add" else Fraction(op[2], op[3]) + n, d = abs(q.numerator), q.denominator + require(n and d & (d - 1) == 0, "non-dyadic scalar") + if op[0] == "scale": + require(n & (n - 1) == 0, "scale must be a signed power of two") + return 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + require(op[0] == "add", "unknown scalar operation") + return 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) diff --git a/research/complex-jp8-fanin/verify.py b/research/complex-jp8-fanin/verify.py new file mode 100644 index 0000000000..d47209dc83 --- /dev/null +++ b/research/complex-jp8-fanin/verify.py @@ -0,0 +1,265 @@ +"""Exact finite scalar checks, costs and positive prefix envelopes. No writes. + +Sagar Thakrar with substantial OpenAI Codex assistance. Apache-2.0. +Selected scalar semantics and invoice: retained PR531/558/622/626 lineage. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from lowering import WORK, groups, lower, original_cost, require + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDER = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/" +SPEC = "research/complex-k492-owner-repair/data/SPEC.json" + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def read_sources(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + result = {} + for name, expected in pins["files"].items(): + raw = (ROOT / name).read_bytes() + payload = gzip.decompress(raw) if name.endswith(".gz") else raw + require(digest(payload) == expected["payload_sha256"], "changed source: " + name) + if name.endswith((".json", ".json.gz")): + result[name] = json.loads(payload) + spec = result[SPEC]["providers"]["jp8"] + word = result[PROVIDER + "CANONICAL-WORD.json.gz"] + programs = result[PROVIDER + "LOCAL-PROGRAMS.json.gz"] + for name, value in (("CANONICAL-WORD.json.gz", word), + ("LOCAL-PROGRAMS.json.gz", programs)): + require(digest(canonical(value)) == spec["artifact_semantic_sha256"][name], + "selected SPEC semantic identity: " + name) + require(set(programs) == {"forward", "backward"}, "orientation inventory") + require((word["v"], word["R"], word["h"]) == (112, 492, 9), "native geometry") + require(len(word["frames"][1]) == word["h"], "cleanup frame must be full") + for events in programs.values(): + for start, end in groups(events): + require(all(word["final"][event[1][side][1]] == 1 + for event in events[start:end] for side in (1, 2)), + "batch reads an early-ended register") + return word, programs, result[PROVIDER + "LOCAL-CHECKS.json"], result[PROVIDER + "INDEPENDENT-LOCAL-REPLAY.json"] + + +def add_row(target, source, coefficient): + result = dict(target) + for column, value in source.items(): + total = result.get(column, Q(0)) + coefficient * value + if total: + result[column] = total + else: + result.pop(column, None) + return result + + +def execute(program, state, envelope): + """Interpret literal unit primitives independently of the binary recipe.""" + peak = Q(0) + for op in program: + tag, target = op[:2] + if tag == "clear": + state[target], envelope[target] = {}, Q(0) + elif tag == "add": + source, sign = op[2:] + require(sign in (-1, 1) and source != target, "primitive signed-add contract") + state[target] = add_row(state[target], state[source], Q(sign)) + envelope[target] += envelope[source] + elif tag in ("double", "half"): + factor = Q(2) if tag == "double" else Q(1, 2) + state[target] = {j: value * factor for j, value in state[target].items()} + envelope[target] *= factor + else: + raise ValueError("unknown primitive") + peak = max(peak, envelope[target]) + return peak + + +def macro(op, state, envelope): + tag, target = op[0], tuple(op[1]) + peak = Q(0) + if tag == "clear": + state[target], envelope[target] = {}, Q(0) + elif tag == "copy": + source = tuple(op[2]) + state[target], envelope[target] = dict(state[source]), envelope[source] + elif tag == "scale": + q = Q(op[2], op[3]) + state[target] = {j: q * value for j, value in state[target].items()} + envelope[target] *= abs(q) + elif tag == "add": + source, q = tuple(op[2]), Q(op[3], op[4]) + require(source != target, "macro alias") + state[target] = add_row(state[target], state[source], q) + envelope[target] += abs(q) * envelope[source] + # Original Horner grows monotonically to |numerator| before halving. + peak = abs(q.numerator) * envelope[source] + state[WORK], envelope[WORK] = {}, Q(0) + else: + raise ValueError("unknown macro") + return max(peak, envelope[target]) + + +def block_check(block, program=None): + """Check all local inputs, including arbitrary incoming private work.""" + registers = sorted({tuple(e[1][1]) for e in block} | {tuple(e[1][2]) for e in block} | {WORK}) + state = {r: {i: Q(1)} for i, r in enumerate(registers)} + expected = {r: dict(row) for r, row in state.items()} + env = {r: Q(1) for r in registers} + old_env = dict(env) + for event in block: + macro(event[1], expected, old_env) + recipe = lower(block) if program is None else program + peak = execute(recipe, state, env) + require(state == expected, "wrong block boundary map or private clearing") + require(env == old_env, "wrong block endpoint envelope") + require(2 * len(recipe) < sum(original_cost(e[1]) for e in block), "no strict saving") + return peak + + +def replay(events, orientation, changed, n): + # Rows carry every arbitrary live/helper input and incoming centre/work dirt. + state = {("L", r): {r: Q(1)} for r in range(n)} + state.update({("C", r): {n + r: Q(1)} for r in range(8)}) + state[WORK] = {n + 8: Q(1)} + env = {r: Q(1) for r in state} + peak, scratch_peak, cost, index = Q(1), Q(0), 0, 0 + selected = dict(groups(events)) if changed else {} + profile = Counter() + records = [] + while index < len(events): + if index in selected: + end = selected[index] + block = events[index:end] + recipe = lower(block) + block_check(block, recipe) + sources = [tuple(e[1][2]) for e in block] + q = abs(Q(block[0][1][3], block[0][1][4])) + total = sum((env[r] for r in sources), Q(0)) + work_bound = total * max(Q(1), Q(2 ** (q.numerator.bit_length() - 1), q.denominator)) + scratch_peak = max(scratch_peak, work_bound) + peak = max(peak, execute(recipe, state, env)) + baseline = sum(original_cost(e[1]) for e in block) + cost += 2 * len(recipe) + records.append([index, end, list(block[0][1][1]), str(q), baseline, 2 * len(recipe)]) + index = end + continue + event = events[index] + if event[0] == "scalar": + cost += original_cost(event[1]) + peak = max(peak, macro(event[1], state, env)) + elif event[0] == "climb": + profile[event[5]] += 1 + elif event[0] == "center": + profile[event[4]] += 1 + else: + require(event[0] in ("phase", "adapter", "residual_adapter"), "event tag") + index += 1 + for r in range(n): + expected = {r: Q(1)} + if orientation == "backward" and r < 112: + expected[112 + r] = Q(-1) + elif orientation == "forward" and 112 <= r < 224: + expected[r - 112] = Q(1) + require(state["L", r] == expected, "all-column scalar endpoint") + require(all(not row for r, row in state.items() if r[0] != "L"), "private work or centre dirt") + return dict(real_primitives=cost, prefix_l1=str(peak), + prefix_bits=peak.numerator.bit_length() - peak.denominator.bit_length() + 1, + scratch_prefix_l1=str(scratch_peak), paid_profile=dict(sorted(profile.items())), + batches=len(records), additions=sum(b - a for a, b, *_ in records), + batch_sha256=digest(canonical(records)), + length_histogram=dict(sorted(Counter(b - a for a, b, *_ in records).items()))) + + +def controls(): + sample = [["scalar", ["add", ["L", 0], ["L", i], sign * 13, 4], 1] + for i, sign in ((1, 1), (2, -1), (3, 1))] + recipe = lower(sample) + block_check(sample) + cases = {"missing_entry_clear": recipe[1:], "missing_exit_clear": recipe[:-1], + "missing_source_read": recipe[:2] + recipe[3:]} + half = next(i for i, op in enumerate(recipe) if op[0] == "half") + double = next(i for i, op in enumerate(recipe) if op[0] == "double") + cases["missing_halving"] = recipe[:half] + recipe[half + 1:] + cases["missing_doubling"] = recipe[:double] + recipe[double + 1:] + wrong = list(recipe) + wrong[2] = ("add", WORK, ("L", 2), 1) + cases["wrong_source_sign"] = wrong + last_add = max(i for i, op in enumerate(recipe) if op[0] == "add") + cases["missing_target_accumulation"] = recipe[:last_add] + recipe[last_add + 1:] + cases["cost_inflation"] = recipe[:-1] + [("double", WORK), ("half", WORK)] * 100 + recipe[-1:] + rejected = [] + for name, program in cases.items(): + try: + block_check(sample, program) + except ValueError: + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + for name, pos, value in (("target_alias", (0, 1, 2), ["L", 0]), + ("frame_boundary", (1, 2), 0), + ("non_dyadic", (0, 1, 4), 3)): + mutated = json.loads(json.dumps(sample)) + obj = mutated + for part in pos[:-1]: + obj = obj[part] + obj[pos[-1]] = value + try: + lower(mutated) + except ValueError: + rejected.append(name) + else: + raise ValueError("invalid input accepted: " + name) + # An endpoint-neutral excursion must still increase the measured envelope. + registers = [("L", i) for i in range(4)] + [WORK] + state = {r: {i: Q(1)} for i, r in enumerate(registers)} + env = {r: Q(1) for r in registers} + excursion = recipe[:-1] + [("double", WORK)] * 10 + [("half", WORK)] * 10 + recipe[-1:] + require(execute(excursion, state, env) > block_check(sample), "prefix excursion undetected") + rejected.append("endpoint_neutral_prefix_excursion") + return rejected + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", action="store_true", help="print computed evidence instead of checking EXPECTED.json") + args = parser.parse_args() + word, programs, checks, prior = read_sources() + rows = {} + for orientation, events in programs.items(): + before = replay(events, orientation, False, 716) + after = replay(events, orientation, True, 716) + require(before["real_primitives"] == checks[orientation]["real_component_primitive_bound"], "original invoice") + require(before["prefix_l1"] == prior["local"][orientation]["prefix_l1_upper"], "original prefix") + require(after["paid_profile"] == before["paid_profile"] == {int(k): v for k, v in word["local_profile"].items()}, "paid profile") + require(Q(after["prefix_l1"]) < 2 ** prior["local"][orientation]["charged_payload_bits"], "payload allowance exceeded") + rows[orientation] = dict(before=before, after=after, + real_saved=before["real_primitives"] - after["real_primitives"]) + result = dict(status="PASS_JP8_REVERSE_HORNER_FANIN", live_columns=716, + arbitrary_private_inputs=9, orientations=rows, controls=controls()) + if args.receipt: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + require(json.loads((HERE / "EXPECTED.json").read_text()) == json.loads(json.dumps(result)), "receipt mismatch") + backward = rows["backward"] + print("PASS_JP8_REVERSE_HORNER_FANIN" + f" batches={backward['after']['batches']} additions={backward['after']['additions']}" + f" real_saved={backward['real_saved']} columns=716 controls={len(result['controls'])}") + + +if __name__ == "__main__": + main() From 7a1a3a319da359ec8b6e83230a7fcf7733fac8e5 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:37:21 +0530 Subject: [PATCH 2/2] Record completed sprint result and PR link --- research/complex-jp8-fanin/CLAIM.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/research/complex-jp8-fanin/CLAIM.md b/research/complex-jp8-fanin/CLAIM.md index e260ca1129..f536f227e5 100644 --- a/research/complex-jp8-fanin/CLAIM.md +++ b/research/complex-jp8-fanin/CLAIM.md @@ -17,3 +17,13 @@ Acceptance requires a positive fully priced saving, exact maps including arbitra During optimistic pricing, the initial two-stream recipe was simplified to one stream. Halve the signed source sum first, then scan numerator bits from least to most significant, accumulating into the target at each set bit and doubling the work stream between bits. This is the transpose direction of binary Horner sharing. It needs no added private register and explicitly credits the related forward construction in #722. Prepared for Sagar Thakrar, @thakrarsagar, with substantial OpenAI Codex assistance. Apache-2.0. + +## Result + +Completed and submitted as [PR #751](https://github.com/CrocSwap/integer-mult-bounds/pull/751). +All 999 backward cleanup batches, covering 3,022 additions, preserve their +exact maps and save 19,688 real primitives with one existing private stream. +The full backward prefix remains 101 bits. Main replay, twelve controls, +the separate 5,020-column block checker and selected-record check pass. +The contribution is a finite circuit research construction with no new kappa; +production integration and inherited global obligations remain open.