diff --git a/research/qq16-scratch-travel/README.md b/research/qq16-scratch-travel/README.md new file mode 100644 index 0000000000..7caf6d2985 --- /dev/null +++ b/research/qq16-scratch-travel/README.md @@ -0,0 +1,292 @@ +# Exact QQ16 scratch-sweep head travel + +The two scalar sweeps of ywz65's [PR #2709](https://github.com/CrocSwap/integer-mult-bounds/pull/2709) +have the following exact total head travel for every positive integer `N`: + +| Placement of all 112 banks on each tape | Closed word-address steps | +|---|---:| +| Bank-major, `address(bank, site) = bank*N + site` | `8564*N^2 + 306*N - 2` | +| Site-major, `address(bank, site) = 112*site + bank` | `9300*N - 432` | + +Both execute the same scalar operations at every site. Their difference is +`(N-1)*(8564*N-430)`, positive for `N >= 2` and zero at `N = 1`. +For `N = 2`, the exact bills are 34,866 and 18,168 steps. + +One bounded variant also permits linear travel in **bank-major** storage: +replace eight scratch-to-scratch subtractions by restored dirty bridges +through existing Z0 and stream each scalar instruction across all sites. +It costs exactly `11866*N - 2840` address steps and **24 additional unit +ADDs**, with no extra payload array in this model. It requires exclusive +W-bank availability throughout each complete window, rather than releasing +one owner's scratch before processing the next owner. + +This is a proved tariff for a specified access protocol. It answers one part +of PR #2709's open movement obligation. It does not price the complete decoder, +establish a minimum over other schedules, or improve the selected supplier or +kappa. In particular, **constructing the site-major layout is not free**. + +## Boundary and access protocol + +Pin PR #2709 at `d7749c49e967b214537c0bd832e435e177e21d4f`. +Its input is commdata2338's PR #2651, pinned at +`a3b82e6f4ddcf999f8b6dcd3a6dfc3a9543a1533`, retaining ywz65's +PR #2540 `630d557af5088f66b45c447969cee9576600e50b`. +The compressed [literal source word](source-word.json.gz) is a mathematical +input, not an executable dependency. [SOURCES.json](SOURCES.json) records its +original path, commit, Git blob and decompressed SHA256. The verifier imports +no predecessor code. Different gzip containers with the same payload pass. + +There are two independently movable word-address tapes, one holding the +112 owned Z output banks and the other the 112 owned W output banks. +Each bank contains `N` aligned physical scalar sites in the same order. +A site can combine an owner index with a payload component index. No X or Y +borrowed input occurs in these two windows. The borrowed output slices are +W0 in the L2 window and W0 through W15 in the F0-inverse window. + +For each window, visit sites in increasing order and preserve its literal +scalar instruction order at each site. An ADD reads its source, then updates +its destination; a CLEAR updates its target. Each access touches the named +word address once. Project this ordered access sequence onto each tape. +Count the sum of the two heads' absolute address differences. Each head starts +at address zero and returns there after each window. These are separately +closed windows, not an optimized joint endpoint schedule. + +The address model allows one scalar source register and in-place scalar +arithmetic at the destination. G-to-F ADDs read and update two W words in that +order. No extra payload array is needed in this model. A scalar register can +contain a precision-dependent number of bits; this is **not** a finite-control +two-tape implementation or a claim that staging, bit arithmetic, carries, +instruction fetches or in-word scans cost zero. The tariff counts word-address +movement only. A bit-level implementation needs those additional charges. + +Aligned scalar access and exclusive disposable W storage are premises, as in +PR #2709's owner-access contract. A common frame label alone does not prove +physical layout or alignment. All banks on a tape use the stated pitch of +112 in the site-major layout, including W16 through W111, which the windows +do not touch. The two layouts represent the same logical values initially; +the comparison excludes the conversion between them. + +## Proof and source-bound constants + +The zero-based inclusive markers in the pinned word are 633 through 1066 for +L2 and 1172 through 2125 for F0 inverse. Every interior event is a pointwise +ADD or CLEAR. There is no native operation, cover map or owner permutation +inside either body. The verifier validates these facts and field bounds. + +Operations at distinct aligned sites touch disjoint cells and commute. +Exchanging only such operations changes the source event-major sweep into +the site-major sweep without changing any site's event order. This proves +equality on arbitrary scalar inputs and disposable dirty output contents. +The final scratch clears and later output clears remain. PR #2709's native, +frame, lifetime and full decoder theorems are inherited, not independently +proved here. The movement calculation itself needs only these scalar bodies. + +For one tape, let `q` be its bank-number sequence for one site, let `a` and +`b` be its first and last banks, and let +`V = sum(abs(q[j+1]-q[j]))`. Extracting the literal source gives: + +| Window / tape | Touches per site | a | b | V | +|---|---:|---:|---:|---:| +| L2 / Z | 416 | 76 | 107 | 2485 | +| L2 / W | 432 | 0 | 0 | 0 | +| F0 inverse / Z | 912 | 76 | 110 | 4396 | +| F0 inverse / W | 944 | 0 | 15 | 1603 | + +Bank-major placement contributes an initial seek of `Na`, `N` within-site +walks of length `NV`, `N-1` inter-site walks of length `abs(N(a-b)+1)`, +and a final return of `Nb+N-1`. Its exact total is therefore + +```text +T_bank = N^2*V + (N-1)*abs(N*(a-b)+1) + N*(a+b) + N-1. +``` + +For `a < b`, integer `N >= 1` gives +`abs(N(a-b)+1) = N(b-a)-1`. Substitution yields +`T_bank = (V+b-a)*N^2 + 2*a*N`. +For `a >= b`, substitution instead yields +`T_bank = (V+a-b)*N^2 + (2*b+2)*N - 2`. +This includes L2/W with `a=b=V=0`, whose bill is `2*N-2`. + +Site-major placement contributes an initial seek of `a`, `N` within-site +walks of length `V`, `N-1` inter-site walks of length `112+a-b`, and +a return of `112*(N-1)+b`. Since `0 <= a,b < 112`, every inter-site +distance is positive. Thus + +```text +T_site = (V+224+a-b)*N + 2*b-224. +``` + +Adding the two tapes gives the following exact polynomials: + +| Window | Bank-major | Site-major | +|---|---:|---:| +| L2 | `2516*N^2 + 154*N - 2` | `2902*N - 234` | +| F0 inverse | `6048*N^2 + 152*N` | `6398*N - 198` | + +Their sum proves the opening result for every positive integer `N`. +Sampling was not used to fit these coefficients. For the prescribed touch +sequence, direct walks between consecutive addresses attain the tariff; +triangle inequality excludes a shorter walk that visits them in that order. +Different site orders, scalar resynthesis, caching and layout choices are +outside this statement. + +## Bank-major streaming with a restored dirty bridge + +The original word contains exactly eight same-tape ADDs, at source events +1637, 1686, 1735, 1784, 1833, 1882, 1931 and 1980. Each is +`W[k] -= W[k+8]`, for `k=0..7`. Replace it with the following four ADDs: + +```text +Z0 += W[k+8] +W[k] -= Z0 +Z0 -= W[k+8] +W[k] += Z0 +``` + +For arbitrary initial `(Z0,W[k],W[k+8])=(z,f,g)`, the result is `(z,f-g,g)`. +Thus Z0 restores exactly and need not start at zero. Every ADD uses distinct +source and target in the common current frame. Z0 is an existing owned output. +No native operation or other original instruction intervenes between these +four replacements. The identity is standard dirty workspace borrowing; the +contribution is this exact source-bound application and bill. + +Every resulting ADD crosses between the Z and W tapes. Execute the body in +event-major order: for one scalar instruction, sweep sites `0..N-1`, then +perform the next instruction. Each ADD uses the source register for one site +and updates that site's destination before advancing both relevant heads. +The projection onto either tape therefore visits one bank's contiguous sites +for each instruction that touches that tape. Same-tape source/destination +ADDs would invalidate this streaming projection without further storage; +the verifier explicitly excludes them after the bridge rewrite. + +This schedule changes the access premise. All W0 through W15 banks must +remain exclusively available across the entire F0-inverse window. Partial +scratch values at many sites coexist between passes. They occupy existing +owned output banks, so no additional payload array is allocated, but their +whole-window ownership and retention are required. Z0 is temporarily modified +between bridge passes and restores before the next original instruction. +This is not the predecessor's one-owner-at-a-time release schedule. + +For one tape let `q` now denote the bank sequence projected from one pass +through the rewritten *instructions*, with length `m`, endpoints `a,b`, and +successive differences `delta`. The exact bank-major head travel is + +```text +T_stream = N*a + m*(N-1) + + sum(abs((delta-1)*N+1)) + N*b + N-1. +``` + +If `delta >= 1`, its summand is `(delta-1)*N+1`. If `delta <= 0`, its +summand is `(1-delta)*N-1`. These identities hold for all integer `N >= 1`, +including zero-length transitions at `N=1`. Thus this tariff is linear +without polynomial fitting. The literal rewritten instruction projections +give: + +| Window | Z tape | W tape | Sum | +|---|---:|---:|---:| +| L2 | `2700*N-32` | `864*N-864` | `3564*N-896` | +| F0 inverse | `5412*N-800` | `2890*N-1144` | `8302*N-1944` | + +The total is `11866*N-2840`, or 20,892 steps at `N=2`. It has lower travel +than the unchanged site-ordered bank-major protocol for every `N >= 2`; +it costs 158 more steps at `N=1`. This is a comparison of declared protocols, +not a lower bound over other schedules or caching strategies. + +Replacing eight ADDs by 32 adds 24 unit ADDs. At the pinned +[QQ16 scalar prices](../joint-query/verify_scalar.py), this adds 192 real +scalar primitives. The complete added local decoder allowance changes from +840 unit ADDs, 832 quarter ADDs and 288 CLEARs, totaling 17,280, to +864 unit ADDs, 832 quarter ADDs and 288 CLEARs, totaling **17,472**. +No native event, cover map or original CLEAR changes. The inherited F0/B1 +work remains additional. Scalar primitives and address steps are separate +units; this package does not add them to claim a runtime improvement. +The layout-conversion assumption is avoided by this variant, but whole-window +retention, bit arithmetic, instruction control and surrounding native costs +still need implementation and pricing. + +## Reproduce and verification limits + +From the repository root, standard-library Python 3.12 or later: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-scratch-travel +``` + +The registered replay runs the verifier normally and with optimization, then +four artifact tests. Its result is + +```text +PASS_QQ16_SCRATCH_TRAVEL bank=8564*N^2+306*N-2 site=9300*N-432 no_new_kappa +PASS_QQ16_DIRTY_BRIDGE_STREAM bank=11866*N-2840 extra_unit_adds=24 no_new_kappa +``` + +The verifier derives every coefficient from the authenticated source, checks +literal address walks at `N=1..32,64`, and compares event-major and site-major +exact rational dirty-state execution at `N=2,3,5`. Wrong-site reads disagree. +The bridge variant also derives and checks its linear coefficients against +literal bank-major instruction sweeps, compares every output cell with the +original event-major body, and rejects a wrong dirty-restoration sign. +Controls detect omitted touches, omitted head returns, substituted layouts, +native events inside a scalar sweep, borrowed X/Y access, inactive W slices +and aliased ADD roles. Artifact tests exercise a read-only Git-free export, +source-byte corruption, type-sensitive receipt corruption and a recompressed +identical source payload. Finite tests support the quantified proof above. + +No predecessor verifier, actual native kernel, selected full cold replay, +Lean theorem or complete physical caller was checked. The source remains a +pending dependency. Its 224 output banks, sixteen retained early values and +native/scalar invoice remain inherited. Producing and consuming either layout +can change the surrounding native movement bill even when native event counts +stay fixed. There is no whole-construction saving claim. + +Implementation bounds are explicit: at most 256,000 decompressed source bytes, +2,415 source events, 2,000 projected touches per tape, 64 literal sites and five +semantic fixture sites. New functions stay below 60 lines. Runtime contracts +remain active under `-O`; warnings are errors in the registered commands. +Power of Ten rule 3 has a bounded managed-runtime deviation here: Python JSON, +integer and Fraction operations allocate dynamically, with those enforced +capacities limiting live data. Replacing this offline verifier with a fixed +capacity native implementation is necessary only if allocation-free execution +becomes a requirement. This does not claim an allocation-free tape program. + +## Task, overlap and freshness + +The base is canonical main `c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5`, +priority revision 5. The chooser drew recursive interfaces with nonce +`8fbde7a90a030e7b3455c3218d1d828f`. [TASK.json](TASK.json) refines +`joint-query-controller` to this explicit missing access bill. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2617#discussioncomment-18955159) +joins the existing scratch/retention investigation. + +Live overlap identified PR #2709 before implementation, so the scratch-reuse +construction was not repeated. Its stated open seeks/staging obligation is +the exact distinction. Complete cached overlap at 18:10 UTC covered 767 open +PRs and 1,334 Discussion records, supplemented by recent live PR/Discussion +and exact dependency reads. Searches for QQ16 head travel, bank-major, +site-major and the predecessor package found no separate tariff. Coverage +does not prove novelty. Final upstream and overlap freshness are recorded in +TASK.json. The family decision is to stop at this cost lemma and its bounded +bridge variant, with no supplier admission or dependent construction campaign. + +## Open next questions + +Can a complete caller produce and consume the site-major layout without +repaying this local movement difference? Pin one caller's input/native/output +schedule, then price its entry and exit layout conversions under the same +address protocol. The missing complete layout and native-placement ledger +block a whole-decoder comparison. [TASK.json](TASK.json) records this question. +For the bank-major streaming alternative, first check whole-window exclusive +W ownership in that same caller, then price its retention and bit-level +source-register implementation. The two protocols have different contracts; +neither complete bill follows from its address tariff alone. + +## Credit + +Nick Petalas. New work is Apache-2.0. +Credit ywz65 for PR #2709's conditional slice-access construction and +PR #2540's complete local decoder, commdata2338 for PR #2651's early-bank +coalescing, and the retained QQ16 lineage of Ali Romman, starship-s, +Sagar Thakrar, Ross Richardson and the native/geometry contributors. +Their source and proof claims retain their original attribution and scope. +The contribution here is the source-bound movement tariff and checker. +No independent human or maintainer review is claimed. diff --git a/research/qq16-scratch-travel/RESULT.json b/research/qq16-scratch-travel/RESULT.json new file mode 100644 index 0000000000..c8a554f75a --- /dev/null +++ b/research/qq16-scratch-travel/RESULT.json @@ -0,0 +1,154 @@ +{ + "touch_invariants": { + "L2": { + "Z": [ + 416, + 76, + 107, + 2485 + ], + "W": [ + 432, + 0, + 0, + 0 + ] + }, + "F0_inverse": { + "Z": [ + 912, + 76, + 110, + 4396 + ], + "W": [ + 944, + 0, + 15, + 1603 + ] + } + }, + "polynomials": { + "L2": { + "bank-major": [ + 2516, + 154, + -2 + ], + "site-major": [ + 0, + 2902, + -234 + ] + }, + "F0_inverse": { + "bank-major": [ + 6048, + 152, + 0 + ], + "site-major": [ + 0, + 6398, + -198 + ] + } + }, + "total_bank_major": [ + 8564, + 306, + -2 + ], + "total_site_major": [ + 0, + 9300, + -432 + ], + "literal_site_cases": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 64 + ], + "semantic_site_cases": [ + 2, + 3, + 5 + ], + "scope": "two scalar sweeps, closed word-address protocol, no new kappa", + "streaming_variant": { + "L2": { + "bridges": 0, + "extra_unit_adds": 0, + "polynomial": [ + 0, + 3564, + -896 + ], + "tape_touches": { + "Z": 416, + "W": 432 + } + }, + "F0_inverse": { + "bridges": 8, + "extra_unit_adds": 24, + "polynomial": [ + 0, + 8302, + -1944 + ], + "tape_touches": { + "Z": 944, + "W": 960 + } + } + }, + "streaming_total": [ + 0, + 11866, + -2840 + ], + "source_scalar_bill": { + "unit_adds": 840, + "quarter_adds": 832, + "clears": 288, + "real_scalar_primitives": 17280 + }, + "streaming_scalar_bill": { + "unit_adds": 864, + "quarter_adds": 832, + "clears": 288, + "real_scalar_primitives": 17472 + } +} diff --git a/research/qq16-scratch-travel/SOURCES.json b/research/qq16-scratch-travel/SOURCES.json new file mode 100644 index 0000000000..e96ad90b0f --- /dev/null +++ b/research/qq16-scratch-travel/SOURCES.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "base_commit": "c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/joint-query/verify_scalar.py", + "usage": "provenance", + "git_blob": "7a7051fa8a70f48589fa1fccd5c38fccb5eacbf7", + "sha256": "33bdbad17a0531fe527aff306eb235d9c38c1629db4fd167b989725930b0327a" + } + ], + "pending_source": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2709", + "author": "ywz65", + "commit": "d7749c49e967b214537c0bd832e435e177e21d4f", + "path": "research/qq16-output-slice-scratch/WORD.json", + "archive": "source-word.json.gz", + "uncompressed_bytes": 202523, + "sha256": "5854aae388d1f11d201b8a02db92dd9b688827dc24280f753c3dc5db069704c5", + "git_blob": "90cd824dbb7cd3d37e519fc1e188e3c944c41119" + } +} diff --git a/research/qq16-scratch-travel/TASK.json b/research/qq16-scratch-travel/TASK.json new file mode 100644 index 0000000000..a35e465a67 --- /dev/null +++ b/research/qq16-scratch-travel/TASK.json @@ -0,0 +1,142 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 5, + "base_commit": "c3c94c2ea2ebcd5d69d1e51b5fe8a36bf79819f5", + "original_card": { + "id": "joint-query-controller", + "question": "Can one unresolved retention, output-consumer, hosting or physical-cost obligation complete a pinned QQ16 controller proposal within budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Design and price one consumer or retained-state boundary for a pinned local decoder, including final restoration.", + "Audit one claimed physical invoice or prove a target-specific obstruction for its explicit retention/hosting contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the QQ16 row in research-family-status.md. The fixed-first-pair witness remains scoped; pending #2540 adds early records and claims a complete local native decoder, but not a favorable global controller. Read its output-frame and ownership contract before designing another inverse.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Check live claims and pin the newest relevant completed local word (starting lead #2540). Choose one unresolved consumer, retention, whole-cover movement, hosting or precision obligation. Price the complete proposal and test that obligation; do not repeat its claimed local inverse or native reconstruction unless providing distinct independent verification.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact head travel for PR2709 scalar sweeps in two layouts and one bounded dirty-Z0 bridge variant allowing bank-major event streaming.", + "scope_change_reason": "PR2651 early bank coalescing and PR2709 output-slice scratch reuse already exist. Price their explicit missing seek obligation rather than repeat either construction. One bounded variation permits 24 extra unit ADDs and exclusive whole-window W-bank access to avoid layout conversion; it is compared under the same address model, without supplier expansion.", + "bottleneck_link": "QQ16 output scratch reuse needs paid physical access. This isolates exact layout-dependent address movement; initial layout conversion and complete consumer costs remain open.", + "budget_minutes": 60, + "stop_rule": "Stop after two source-pinned scalar windows, quantified tariff proof, exact replay and failure controls; do not expand into a supplier construction.", + "outcome": "completed", + "evidence": "README proof and verify.py source-bound exact traces, polynomial identities, site commutation checks and semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Assistance disclosure omitted under the donor no-attribution instruction.", + "open_questions": [ + { + "question": "Can a complete QQ16 caller provide the site-major Z/W layout without repaying the local movement saving?", + "why_it_matters": "The linear sweep tariff excludes producing, converting and consuming the layout.", + "first_step": "Pin one caller and price its entry/exit transpose and native-map access under the same word-address protocol.", + "blocked_by": "No complete caller layout or native-placement ledger is supplied here." + }, + { + "question": "Can a complete caller retain exclusive W0..W15 ownership for every instruction pass of the bank-major bridge schedule?", + "why_it_matters": "The bridge avoids layout conversion by retaining partial scratch values across entire banks, which changes the predecessor access contract.", + "first_step": "Pin the caller lifetime schedule and price whole-window retention plus an actual precision-dependent source register.", + "blocked_by": "No full caller ownership, bit-machine or hosting implementation is supplied." + } + ], + "selection": { + "seed": "8fbde7a90a030e7b3455c3218d1d828f", + "track": "recursive-interfaces", + "scope_key": "b8872a10540bed52f194" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2617#discussioncomment-18955159", + "declared_milestone": "scoped movement-cost audit", + "unknown_costs": [ + "initial/final layout conversions", + "scalar bit arithmetic and staging implementation", + "instruction dispatch and tape encodings", + "native operations outside windows", + "retention, hosting, complete consumer and all-size admission" + ], + "family_decision": "Narrow to one access-cost lemma; no dependent construction round.", + "streaming_variant": { + "changed_premise": "All W0..W15 site slices remain exclusively available through each complete scalar window; Z0 may be borrowed and restored during each four-pass bridge. Unlike one-owner-at-a-time borrowing, all sites may hold scratch values between instruction passes.", + "extra_unit_adds": 24, + "extra_real_scalar_primitives": 192, + "complete_local_scalar_allowance": 17472, + "address_steps": "11866*N-2840", + "unknown_costs": "Whole-window retention, bit arithmetic, instruction control and all surrounding native/caller costs remain additional." + }, + "freshness": { + "checked_at_utc": "2026-10-15T18:22:37.670066+00:00", + "canonical_main": "78ceed4139bc61be797f6d38f21a03d972bb3290", + "priority_revision": 5, + "relevant_guidance_or_input_changes": "None between base c3c94c2ea and checked main; newer unrelated integrations are outside this package. Frozen source inputs and historical provenance stay pinned.", + "predecessor_heads": { + "2709": "d7749c49e967b214537c0bd832e435e177e21d4f", + "2651": "a3b82e6f4ddcf999f8b6dcd3a6dfc3a9543a1533" + }, + "overlap_coverage": { + "open_prs": { + "fetched_at": "2026-10-15T18:21:21.275395+00:00", + "complete_pagination": true, + "records": 762 + }, + "discussions": { + "fetched_at": "2026-10-15T18:17:55.288879+00:00", + "complete_pagination": true, + "records": 1337 + } + }, + "overlap_warnings": [], + "overlap_limitations": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission." + }, + "verification": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64", + "registered_command": "python3.12 -I -B scripts/research_package.py --package research/qq16-scratch-travel", + "result": "PASS normal and optimized replay; 4 artifact tests PASS", + "additional_python": "3.14 direct -X dev -W error replay and artifact tests PASS", + "lint": "ruff 0.17.1 check --select E,F,B,UP,SIM: PASS", + "review": "Separate internal primary-source and final code review found no blocker; no independent human or maintainer review claimed.", + "unrun": [ + "selected full cold replay", + "actual native kernels", + "Lean", + "bit-machine arithmetic, control and physical caller implementation" + ] + } +} diff --git a/research/qq16-scratch-travel/VERIFY.json b/research/qq16-scratch-travel/VERIFY.json new file mode 100644 index 0000000000..647ab645ef --- /dev/null +++ b/research/qq16-scratch-travel/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source, source-touch invariants, exact polynomial coefficients, literal traces, site commutation, dirty-bridge streaming, full scalar delta and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Acceptance checks remain enabled under Python optimization." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/test_artifacts.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only export; source and typed receipt rejection; recompressed identical payload acceptance." + } + ] +} diff --git a/research/qq16-scratch-travel/source-word.json.gz b/research/qq16-scratch-travel/source-word.json.gz new file mode 100644 index 0000000000..d6f1503718 Binary files /dev/null and b/research/qq16-scratch-travel/source-word.json.gz differ diff --git a/research/qq16-scratch-travel/test_artifacts.py b/research/qq16-scratch-travel/test_artifacts.py new file mode 100644 index 0000000000..d7a5ad2d52 --- /dev/null +++ b/research/qq16-scratch-travel/test_artifacts.py @@ -0,0 +1,84 @@ +"""Exercise the published verifier through its standalone command.""" + +import gzip +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +class ArtifactChecks(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory() + self.package = Path(self.temporary.name) / "package" + shutil.copytree( + HERE, self.package, ignore=shutil.ignore_patterns("__pycache__") + ) + + def tearDown(self): + for path in self.package.iterdir(): + path.chmod(0o644) + self.package.chmod(0o755) + self.temporary.cleanup() + + def replay(self): + return subprocess.run( + [ + sys.executable, + "-I", + "-B", + "-W", + "error", + str(self.package / "verify.py"), + ], + cwd=self.temporary.name, + capture_output=True, + text=True, + timeout=30, + check=False, + ) + + def test_git_free_read_only_replay(self): + before = {p.name: p.read_bytes() for p in self.package.iterdir() if p.is_file()} + for path in self.package.iterdir(): + path.chmod(0o444) + self.package.chmod(0o555) + result = self.replay() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_QQ16_SCRATCH_TRAVEL", result.stdout) + self.assertEqual( + before, {p.name: p.read_bytes() for p in self.package.iterdir()} + ) + + def test_source_corruption_rejects(self): + path = self.package / "source-word.json.gz" + raw = gzip.decompress(path.read_bytes()).replace(b'"W0"', b'"W1"', 1) + path.write_bytes(gzip.compress(raw, mtime=0)) + result = self.replay() + self.assertNotEqual(result.returncode, 0) + self.assertIn("source SHA256", result.stderr) + + def test_typed_receipt_corruption_rejects(self): + path = self.package / "RESULT.json" + result = json.loads(path.read_text()) + result["literal_site_cases"][0] = True + path.write_text(json.dumps(result)) + run = self.replay() + self.assertNotEqual(run.returncode, 0) + self.assertIn("typed result receipt", run.stderr) + + def test_compression_metadata_is_not_mathematical_evidence(self): + path = self.package / "source-word.json.gz" + raw = gzip.decompress(path.read_bytes()) + path.write_bytes(gzip.compress(raw, compresslevel=1, mtime=1)) + result = self.replay() + self.assertEqual(result.returncode, 0, result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-scratch-travel/verify.py b/research/qq16-scratch-travel/verify.py new file mode 100644 index 0000000000..e2b3a5dcfc --- /dev/null +++ b/research/qq16-scratch-travel/verify.py @@ -0,0 +1,366 @@ +#!/usr/bin/env python3 +"""Exact word-address travel for two pinned QQ16 scalar sweeps. Apache-2.0.""" + +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +WINDOWS = ((633, 1066, "L2"), (1172, 2125, "F0_inverse")) +BANKS = 112 +MAX_SITES = 64 +MAX_BYTES = 256_000 +EXPECTED = { + "L2": {"Z": [416, 76, 107, 2485], "W": [432, 0, 0, 0]}, + "F0_inverse": {"Z": [912, 76, 110, 4396], "W": [944, 0, 15, 1603]}, +} +POLYNOMIALS = { + "L2": {"bank-major": [2516, 154, -2], "site-major": [0, 2902, -234]}, + "F0_inverse": {"bank-major": [6048, 152, 0], "site-major": [0, 6398, -198]}, +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_word(): + source = json.loads((HERE / "SOURCES.json").read_text())["pending_source"] + require(source["archive"] == "source-word.json.gz", "fixed archive path") + require((HERE / source["archive"]).stat().st_size <= MAX_BYTES, "archive bound") + with gzip.open(HERE / source["archive"], "rb") as stream: + raw = stream.read(MAX_BYTES + 1) + require(len(raw) == source["uncompressed_bytes"] <= MAX_BYTES, "source size") + require(hashlib.sha256(raw).hexdigest() == source["sha256"], "source SHA256") + header = b"blob " + str(len(raw)).encode() + b"\0" + require( + hashlib.sha1(header + raw).hexdigest() == source["git_blob"], "source Git blob" + ) + word = json.loads(raw) + require(type(word) is list and len(word) == 2415, "literal word extent") + return word + + +def field(name): + require(isinstance(name, str) and 1 <= len(name) <= 4, "bounded field name") + require(name[0] in "ZW" and name[1:].isdigit(), "owned output field") + bank = int(name[1:]) + require(0 <= bank < BANKS and name == name[0] + str(bank), "canonical bank") + return name[0], bank + + +def body_and_trace(word, start, end, name): + begin, finish = word[start], word[end] + require( + begin["op"] == "output_slices_begin" and begin["name"] == name, + "source begin marker", + ) + require( + finish["op"] == "output_slices_end" and finish["name"] == name, + "source end marker", + ) + expected = ["W0"] if name == "L2" else [f"W{i}" for i in range(16)] + require(begin["fields"] == finish["fields"] == expected, "scratch bank order") + body = word[start + 1 : end] + traces = {"Z": [], "W": []} + for event in body: + op = event["op"] + require(op in ("add", "clear"), "pointwise scalar-only window") + if op == "clear": + require(event["frame"] in ("current", "identity"), "local clear frame") + roles = [event["field"]] + else: + require( + event["coefficient"] in ("1", "-1", "1/4", "-1/4"), + "scalar coefficient alphabet", + ) + require(event["src"] != event["dst"], "distinct ADD fields") + roles = [event["src"], event["dst"]] + for role in roles: + tape, bank = field(role) + require(tape != "W" or role in expected, "active W slice only") + traces[tape].append(bank) + return body, traces + + +def invariants(sequence): + require(0 < len(sequence) <= 2000, "bounded nonempty tape trace") + variation = sum(abs(b - a) for a, b in zip(sequence, sequence[1:], strict=False)) + return [len(sequence), sequence[0], sequence[-1], variation] + + +def coefficients(summary, layout): + _, first, last, variation = summary + if layout == "site-major": + return [0, variation + 2 * BANKS + first - last, 2 * last - 2 * BANKS] + require(layout == "bank-major", "known layout") + if first < last: + return [variation + last - first, 2 * first, 0] + return [variation + first - last, 2 * last + 2, -2] + + +def evaluate(polynomial, sites): + require(type(sites) is int and sites > 0, "positive site count") + square, linear, constant = polynomial + return square * sites * sites + linear * sites + constant + + +def closed_distance(sequence, sites, layout, return_home=True): + require(type(sites) is int and 1 <= sites <= MAX_SITES, "literal trace site bound") + require(layout in ("bank-major", "site-major"), "known layout") + head, distance = 0, 0 + for site in range(sites): + for bank in sequence: + address = ( + bank * sites + site if layout == "bank-major" else BANKS * site + bank + ) + distance += abs(address - head) + head = address + return distance + (head if return_home else 0) + + +def execute(body, sites, site_major, wrong_owner=False): + """Exact dirty-state scalar execution; no native or predecessor code imported.""" + require(type(sites) is int and 1 <= sites <= 5, "semantic fixture site bound") + rows = { + f"{tape}{bank}": [ + Fraction((bank + 3) ** 2 * (site + 1) + offset, 8) for site in range(sites) + ] + for tape, offset in (("Z", 0), ("W", 10000)) + for bank in range(BANKS) + } + # A site-major sweep moves only disjoint-site events, preserving each site's order. + for outer in range(sites if site_major else len(body)): + for inner in range(len(body) if site_major else sites): + site, index = (outer, inner) if site_major else (inner, outer) + event = body[index] + if event["op"] == "clear": + rows[event["field"]][site] = Fraction(0) + else: + src_site = (site + 1) % sites if wrong_owner else site + rows[event["dst"]][site] += ( + Fraction(event["coefficient"]) * rows[event["src"]][src_site] + ) + return rows + + +def bridge_body(body): + """Restore an existing dirty Z0 bank after each W-to-W unit subtraction.""" + out, bridges = [], 0 + for event in body: + if event["op"] == "add" and event["src"][0] == event["dst"][0] == "W": + require(event["coefficient"] == "-1", "unit scratch subtraction") + src, dst = event["src"], event["dst"] + out.extend( + [ + {"op": "add", "src": src, "dst": "Z0", "coefficient": "1"}, + {"op": "add", "src": "Z0", "dst": dst, "coefficient": "-1"}, + {"op": "add", "src": src, "dst": "Z0", "coefficient": "-1"}, + {"op": "add", "src": "Z0", "dst": dst, "coefficient": "1"}, + ] + ) + bridges += 1 + else: + out.append(dict(event)) + require( + all(e["src"][0] != e["dst"][0] for e in out if e["op"] == "add"), + "streaming ADDs cross the two tapes", + ) + return out, bridges + + +def stream_trace(body): + traces = {"Z": [], "W": []} + for event in body: + roles = ( + [event["field"]] if event["op"] == "clear" else [event["src"], event["dst"]] + ) + for role in roles: + tape, bank = field(role) + traces[tape].append(bank) + return traces + + +def stream_coefficients(sequence): + """Each tape visits each instruction's full contiguous site range in order.""" + count, first, last, _ = invariants(sequence) + linear, constant = first + last + 1 + count, -count - 1 + for before, after in zip(sequence, sequence[1:], strict=False): + delta = after - before + linear += delta - 1 if delta >= 1 else 1 - delta + constant += 1 if delta >= 1 else -1 + return [0, linear, constant] + + +def stream_distance(sequence, sites): + require(type(sites) is int and 1 <= sites <= MAX_SITES, "stream site bound") + head, distance = 0, 0 + for bank in sequence: + for site in range(sites): + address = bank * sites + site + distance += abs(address - head) + head = address + return distance + head + + +def check_stream(body, name): + candidate, bridges = bridge_body(body) + require(bridges == (0 if name == "L2" else 8), "exact bridge inventory") + traces = stream_trace(candidate) + parts = [stream_coefficients(traces[tape]) for tape in ("Z", "W")] + total = [sum(part[i] for part in parts) for i in range(3)] + require( + total == ([0, 3564, -896] if name == "L2" else [0, 8302, -1944]), + "stream polynomial coefficients", + ) + for sites in (*range(1, 33), MAX_SITES): + distance = sum(stream_distance(seq, sites) for seq in traces.values()) + require(distance == evaluate(total, sites), "literal streaming distance") + for sites in (2, 3, 5): + require( + execute(candidate, sites, False) == execute(body, sites, False), + "dirty bridge restores every field under event-major execution", + ) + if bridges: + wrong = [dict(e) for e in candidate] + first = next( + i + for i, e in enumerate(wrong) + if e.get("src") == "W8" and e.get("dst") == "Z0" + ) + wrong[first + 2]["coefficient"] = "1" + require( + execute(wrong, 3, False) != execute(body, 3, False), + "dirty restoration control", + ) + return { + "bridges": bridges, + "extra_unit_adds": 3 * bridges, + "polynomial": total, + "tape_touches": {tape: len(seq) for tape, seq in traces.items()}, + } + + +def scalar_bill(word, extra_unit_adds): + adds = Counter( + str(abs(Fraction(e["coefficient"]))) for e in word if e["op"] == "add" + ) + clears = sum(e["op"] == "clear" for e in word) + require(adds == {"1": 840, "1/4": 832} and clears == 288, "source scalar invoice") + # These fixed prices are the pinned PR2651/QQ16 scalar contract, not head travel. + return { + "unit_adds": adds["1"] + extra_unit_adds, + "quarter_adds": adds["1/4"], + "clears": clears, + "real_scalar_primitives": 8 * (adds["1"] + extra_unit_adds) + + 12 * adds["1/4"] + + 2 * clears, + } + + +def check_window(word, start, end, name): + body, traces = body_and_trace(word, start, end, name) + summaries = {tape: invariants(sequence) for tape, sequence in traces.items()} + require(summaries == EXPECTED[name], "literal touch invariants") + for layout in ("bank-major", "site-major"): + parts = [coefficients(summaries[tape], layout) for tape in ("Z", "W")] + total = [sum(part[i] for part in parts) for i in range(3)] + require(total == POLYNOMIALS[name][layout], "derived polynomial coefficients") + for sites in (*range(1, 33), MAX_SITES): + distance = sum( + closed_distance(traces[tape], sites, layout) for tape in ("Z", "W") + ) + require(distance == evaluate(total, sites), "literal travel equals formula") + for sites in (2, 3, 5): + baseline = execute(body, sites, False) + require(execute(body, sites, True) == baseline, "disjoint-site commutation") + require(execute(body, sites, True, True) != baseline, "wrong-owner control") + return summaries, check_stream(body, name) + + +def controls(word): + """Exercise omitted touches/returns, wrong placement, and illegal scalar sites.""" + for start, end, name in WINDOWS: + _, traces = body_and_trace(word, start, end, name) + require( + invariants(traces["Z"][1:]) != EXPECTED[name]["Z"], "missing-touch control" + ) + for layout in ("bank-major", "site-major"): + open_path = sum( + closed_distance(seq, 3, layout, False) for seq in traces.values() + ) + require( + open_path != evaluate(POLYNOMIALS[name][layout], 3), + "return-home control", + ) + require( + closed_distance(traces["Z"], 3, "bank-major") + != closed_distance(traces["Z"], 3, "site-major"), + "layout control", + ) + for edit in ("native", "cross-family", "inactive-scratch", "same-field"): + changed = [dict(event) for event in word] + if edit == "native": + changed[634] = {"op": "current_map", "field": "W0", "port": 0} + elif edit == "cross-family": + changed[635]["src"] = "X76" + elif edit == "inactive-scratch": + changed[635]["dst"] = "W16" + else: + changed[635]["src"] = changed[635]["dst"] + try: + body_and_trace(changed, 633, 1066, "L2") + except ValueError: + continue + raise ValueError("control accepted: " + edit) + + +def main(): + word = load_word() + checked = { + name: check_window(word, start, end, name) for start, end, name in WINDOWS + } + summaries = {name: row[0] for name, row in checked.items()} + controls(word) + totals = { + layout: [ + sum(POLYNOMIALS[name][layout][i] for _, _, name in WINDOWS) + for i in range(3) + ] + for layout in ("bank-major", "site-major") + } + stream_total = [ + sum(row[1]["polynomial"][i] for row in checked.values()) for i in range(3) + ] + extra_adds = sum(row[1]["extra_unit_adds"] for row in checked.values()) + result = { + "touch_invariants": summaries, + "polynomials": POLYNOMIALS, + "total_bank_major": totals["bank-major"], + "total_site_major": totals["site-major"], + "literal_site_cases": [*range(1, 33), MAX_SITES], + "semantic_site_cases": [2, 3, 5], + "streaming_variant": {name: row[1] for name, row in checked.items()}, + "streaming_total": stream_total, + "source_scalar_bill": scalar_bill(word, 0), + "streaming_scalar_bill": scalar_bill(word, extra_adds), + "scope": "two scalar sweeps, closed word-address protocol, no new kappa", + } + expected = json.loads((HERE / "RESULT.json").read_text()) + require( + json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "typed result receipt", + ) + print("PASS_QQ16_SCRATCH_TRAVEL bank=8564*N^2+306*N-2 site=9300*N-432 no_new_kappa") + print( + "PASS_QQ16_DIRTY_BRIDGE_STREAM bank=11866*N-2840 " + "extra_unit_adds=24 no_new_kappa" + ) + + +if __name__ == "__main__": + main()