Execute resident SCALE 2 on one ribbon with 14,212 fewer operations

research/resident-scale-ribbon/ENGINEERING.md

@@ -0,0 +1,47 @@
+# Verification and implementation bounds
+
+Playbook: autonomous local run. Exit predicate: one original, verified resident
+SCALE transition saving, packaged for independent review. Stop after that step.
+Build the Lever led to a retained physical compiler and deterministic verifier.
+Prove It Works led to literal metered execution and full endpoint comparisons.
+
+The new call graph is acyclic. Compiler loops are bounded by W <= 64, D <= 64,
+at most 24320 gates and 220000 emitted instructions. Each unit seek has a bound
+from the fixed tape capacity. Tape storage is allocated once at construction,
+with at most 131072 bits per tape. Transfer length is at most 8192 bits. The
+scientific suite has 129 basis columns, 1364 legal pairs, 252 bounded
+width/dimension cases and 24 full physical comparisons. The seven expected
+rejections and three semantic controls have explicit finite domains.
+
+Rule 3, managed allocation deviation. Python lists, tuples and arbitrary-size
+integers allocate during compilation and execution. Directly forbidding that
+allocation conflicts with the supplied CPython replay interface. Scope is this
+fixed finite compiler/verifier only. Explicit width/dimension, route and tape
+capacities bound live payloads; one comparison fixture runs at a time. The
+largest full owner fixture is 99072 bits. The runtime's internal allocations
+are not separately instrumented. A lower-level fixed-storage executor is a
+separate integration step, required before a uniform physical runtime claim.
+
+Rules 8/9, authenticated source loading deviation. The comparison compiler is
+loaded from one hash-checked retained Python file by importlib. Its only
+invoked scientific path is compile_route on the single 380-gate SCALE 2
+circuit and its fixed certificate. There is no arbitrary module selection,
+network fetch or predecessor whole-word replay. Its original code is frozen.
+Source compiler loops operate on the fixed authenticated row, width 64 and
+finite heads. Replacing this adapter is unnecessary for the new construction;
+an eventual standalone lower-level implementation can consume its literal
+instruction output instead.
+
+New functions remain below sixty physical lines. Runtime guards validate
+compiler capacities, tape boundaries, legal instructions and restored finite
+control. The gate-count assertion is supplementary; every scientific check
+and contract uses optimization-preserved exceptions. New code is warning-strict
+and syntax-checked, and the complete verifier also runs under optimized Python.
+No repository Python linter is installed in the available environment. Shared
+diagnostics configuration and immutable source files are unchanged.
+
+The tariff counts logical tape reads, writes and unit moves. A read/XOR is one
+read, and a conditional flip is a read plus write under the same finite-control
+model as the predecessor. Python compilation, fixture construction, snapshots,
+metadata hashing and host interpreter overhead are outside this operation bill.
+The result is not a wall-clock measurement or an encoded-D machine compiler.

research/resident-scale-ribbon/NOTICE

@@ -0,0 +1,7 @@
+Resident SCALE 2 construction produced by Nick Petalas.
+Apache-2.0.
+
+Retained PR6530 source bytes are by Ali Romman and their credited predecessors.
+Their original notice is in inputs/PR6530-NOTICE. Original credit lines in
+source files are unchanged. The new adjacent-swap resident compiler and its
+traffic proof are distinguished from the retained interface and scalar circuit.

research/resident-scale-ribbon/ORIGINS.json

@@ -0,0 +1,37 @@
+{
+  "repository": "aliromman/integer-mult-bounds",
+  "commit": "fadaba3bb16a6965fa5e9c2c7af3a9df6ddf01bf",
+  "source_directory": "research/p104-exclusive-field-cache",
+  "files": [
+    {
+      "path": "CERTIFICATES.json.gz",
+      "sha256": "87bbb8aa68a6f212e479ccfd70340ccb613782b3be6e8942112f4efbf3ca7698",
+      "git_blob": "13d8cef654794318d11e655a63ce95a78f0043a8",
+      "source_path": "inputs/CERTIFICATES.json.gz"
+    },
+    {
+      "path": "CIRCUITS64.json.gz",
+      "sha256": "1652edd8c29d4cf6ca2ad6b771d9c5b0ba5a74cbcea999b1ee1f935a1a89255b",
+      "git_blob": "50ce55861aa769a23d60886418d4e9ec543a8cfb",
+      "source_path": "inputs/CIRCUITS64.json.gz"
+    },
+    {
+      "path": "PR6530-PROOF.md",
+      "sha256": "8ec44a09040a88bd0e43b60ebb8c3f282d6bed63692c48e6d7aa7b4852af69ca",
+      "git_blob": "35698b776e1eb0532bf6a3b4b741c31003d49f10",
+      "source_path": "PROOF.md"
+    },
+    {
+      "path": "cache.py",
+      "sha256": "c7ada185cb2337dec80e1ef8c60045b57d104a9e4a719bd7391b5566dcd37df4",
+      "git_blob": "19822f46079c3cb7890a402cdf272d9eb4ae755c",
+      "source_path": "inputs/cache.py"
+    },
+    {
+      "path": "PR6530-NOTICE",
+      "source_path": "NOTICE",
+      "sha256": "e875893efa14fd80e3e86a0a900de652123492e95d2797edc54adf1ebeb3e83a",
+      "git_blob": "332a64b9e2282a6a3b01f8d474f8f08820edf3a6"
+    }
+  ]
+}

research/resident-scale-ribbon/PROOF.md

@@ -0,0 +1,147 @@
+# Resident doubling on one physical ribbon
+
+This scoped circuit construction and traffic proof was produced by Nick Petalas.
+The construction answers the same-ribbon SCALE question in Ali Romman's PR6530.
+It does not supply a new complete caller bill or a new kappa.
+
+## Contract
+
+Fix a record width W >= 2 and a positive payload dimension D. One resident
+complex field occupies 2D consecutive W-bit two's-complement records on a
+single ribbon, in the predecessor's interleaved real/imaginary order. Each
+signed component x satisfies -2^(W-2) <= x < 2^(W-2), the exact-doubling
+no-overflow condition. The other resident ribbon is arbitrary. Both evacuated
+owner slots are zero. All ribbon heads and the clean finite-control bits begin
+at zero. The owner head may be anywhere legal.
+
+The output doubles every component exactly, returns the active ribbon head
+and control bits to zero, and leaves the other ribbon, all owner cells, the
+owner head and the separate carry tape unchanged. The compiled schedule uses
+one of the two available finite-control bits. It needs no new tape, clean
+payload field, read from an evacuated owner, or field movement.
+
+The written construction applies to every finite W and D. The supplied emitter
+admits 2 <= W <= 64 and 1 <= D <= 64 to bound its materialized instruction list.
+Finite tests cover the explicitly reported domains, not every admitted input.
+
+## Bit map and exact inverse
+
+Write a record as bits b_0,...,b_(W-1), least significant first. Swap adjacent
+positions (W-2,W-1), then (W-3,W-2), down to (0,1). This is the left cyclic
+rotation
+
+    (b_(W-1), b_0, b_1, ..., b_(W-2)).
+
+Each swap is the three CNOTs i->i+1, i+1->i, i->i+1. Finally apply CNOT
+W-1->0. The resulting low bit is b_(W-1) XOR b_(W-2); every higher bit is
+the previous lower bit. The no-overflow condition makes the top two input
+bits equal. Consequently the new low bit is zero and this is exact signed
+doubling. On arbitrary bit strings it remains an invertible linear map.
+Reverse the full CNOT sequence to obtain its two-sided inverse.
+
+The retained source SCALE 2 circuit performs the same cyclic rotation by
+successive swaps with position zero, followed by the same sign-clearing
+CNOT, separately in its two records. The new schedule changes the rotation
+factorization to neighboring swaps and puts both records on one ribbon.
+The source circuit, its arithmetic contract and its previous two-ribbon
+control-cache result retain their predecessor credit. The verifier compares
+the new map, the literal retained source route and a separate logical gate
+interpreter on all 129 basis columns, including the source carry coordinate.
+This is a dependency check for the new construction, not a new predecessor
+audit or a claim to its original result.
+
+For a CNOT c->t, read c into a zero control bit, seek t, read and conditionally
+write t, seek c and read c again to clear the control bit. The target differs
+from the control, so the second control read restores the control bit. The
+operation is reversible for arbitrary data. All seeks expand to unit moves.
+The schedule is fixed by W,D and the instruction pointer; no payload-dependent
+head index, numeric cardinality oracle or hidden payload access is used.
+
+## Exact new traffic
+
+There are 3(W-1)+1 = 3W-2 CNOTs per record. Each costs three reads and one
+write. For N = 2D records, reads are D(18W-12) and writes are D(6W-4).
+
+In the first record, the adjacent swaps cost 8(W-1) moves, with W-2 initial
+moves and W-2 moves between successive swaps. The final long CNOT costs
+3(W-1). Thus the first record costs 13W-15 moves and ends at W-1. Every
+subsequent record costs 13W-14 moves, because its first control is W-1
+positions beyond the preceding exit. The final head return costs NW-1.
+The total movement is N(14W-14)-2 = 28D(W-1)-2.
+
+Adding reads, writes and moves gives
+
+    new(W,D) = D(52W-44)-2.
+    new(64,D) = 3284D-2.
+
+The predecessor's retained width-64 SCALE 2 route costs 9840D before its
+staging transfers. The new resident circuit therefore saves 6556D+2 even
+against that local term alone. This is an operation count, not wall time.
+
+## A complete comparison with identical entry and exit
+
+Use the actual selected word's adjacent events 10481..10483, with zero-based
+indices:
+
+    ADD   256 <- 256 - (1/2)257
+    SCALE 257 <- 2*257
+    ADD   257 <- 257 + (3/2)256
+
+Both named fields can be resident before SCALE and are needed again by the
+following ADD. For the comparison fixture, field 256 occupies bank zero,
+field 257 bank one, and the owner head is at the end of field 256. This is
+a legal entry. We do not claim a patched full predecessor policy.
+
+The old normalized path evicts both fields, executes the retained SCALE
+staging/circuit, reacquires both fields into the same respective banks, and
+returns the owner head to its entry. Try both eviction orders and both
+acquisition orders. The other field's arbitrary data and all unrelated owner
+cells are preserved. This supplies exactly the new path's physical endpoint.
+The next ADD can bind its target/source tape arguments to those banks as in
+PR6530. No physical bank swap is implied or free.
+
+Here is the complete affine calculation for all D >= 1. Let L=128D. From
+the end of field i to the start of field j the distance is
+abs((j-i-1)L+1). Its affine coefficients are 128*abs(j-i-1) and +1 when
+j-i-1 >= 0, or -1 otherwise. A whole-field clean transfer, including ribbon
+rewind, costs 1152D-3 in addition to this seek. It performs six accesses per
+bit and three traversals of L-1 cells.
+
+The inherited SCALE staging costs its entrance seek plus
+2688D-267, before the 9840D local circuit. To derive that staging term,
+the source transfer reads/writes total 24WD. Its moves, excluding entrance
+seek, are 3(2DW-1)+8(DW-1)+4(D-1)W = 18WD-11-4W.
+This is the explicit increasing-record staging path, including all rewinds.
+After reacquisition, returning from the end of field j to the end of field
+256 costs abs(j-256)L. Every sign in these absolute values is fixed on
+D >= 1, so these are affine proofs, rather than extrapolation from samples.
+
+For eviction/acquisition orders 01/01, 01/10, 10/01, 10/10 the complete
+costs are respectively
+
+    17776D-280, 17776D-282, 17776D-278, 17776D-280.
+
+The best stated normalized flush path costs 17776D-282. The resident circuit
+costs 3284D-2, saving 14492D-280, positive for every D >= 1. At D=1 the
+complete comparison is 17494 versus 3282, a saving of 14212 operations.
+This is a minimum over those four explicit normalization paths only.
+The verifier executes all four paths at D=1,2,3 with two payloads each,
+checks their full tapes and heads, and matches the affine bills exactly.
+
+## Limits and credit
+
+Classical adjacent transpositions, CNOT swaps, reversible finite control and
+two's-complement arithmetic retain their usual credit. The new contribution
+is their charged same-ribbon SCALE implementation under this exact exclusive
+owner contract. Ali Romman supplies PR6530's interface, open question and
+comparison policy, PR6527's staging and PR6513/6511's scalar/tape lineage.
+Credit Nick Petalas for the retained scalar circuits, Sagar Thakrar / PR3241
+for metered tape work, DreamingOfClouds / PR6030 and all retained native,
+owner, precision and compiler predecessors. Original source files and credit
+lines are preserved in inputs.
+
+Only SCALE 2 is implemented here. The full caller policy is not reoptimized;
+native and reset flushes retain their original obligations. Uniform encoded-D
+control, native semantics, precision/stock admission, complete supplier funding
+and outer transfer remain open. No new kappa, selected-frontier change,
+independent human acceptance or formal proof-kernel result is claimed.

research/resident-scale-ribbon/README.md

@@ -0,0 +1,86 @@
+# Resident SCALE 2 without a whole-cache flush
+
+This scoped circuit construction and written traffic proof was produced by
+Nick Petalas. It answers Ali Romman's released same-ribbon question in
+[PR6530](https://github.com/CrocSwap/integer-mult-bounds/pull/6530).
+
+A resident width-64 complex field can be doubled on its existing ribbon for
+exactly **3284D-2** reads, writes and unit head moves. The other resident field,
+both zero owner slots, the owner head and the carry tape remain unchanged.
+There is no additional payload workspace. Signed components must satisfy the
+retained exact-doubling no-overflow condition.
+
+The retained source local circuit costs 9840D before staging. A complete
+comparison for fields 256/257, with identical entry and exit, reduces the best
+of four explicit flush/scale/reacquire paths from 17776D-282 to 3284D-2.
+The saving is **14492D-280** for every positive D. At D=1 it is 14212 operations.
+This is an exact operation count under the predecessor's tape tariff, not a
+wall-clock speedup or a new complete caller bill.
+
+The new schedule rotates each record through neighboring CNOT swaps, then
+clears the duplicated sign bit. Its inverse reverses the same gates.
+[PROOF.md](PROOF.md) proves the bit map, ownership, all-D count and the precise
+comparison class. [ribbon.py](ribbon.py) emits and executes the physical route.
+The implementation bounds W at 64 and D at 64; the written construction holds
+for arbitrary finite W >= 2 and positive D.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/resident-scale-ribbon/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/resident-scale-ribbon/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/resident-scale-ribbon
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/resident-scale-ribbon --check-source-history
+```
+
+Both registered commands are read-only. The optional `--receipt /absolute/path`
+writes a generated result bound to all fifteen package-file hashes. No receipt
+is handwritten. Expected final line: `PASS_RESIDENT_SCALE_RIBBON`.
+
+The complete finite replay checks 129 source/new basis columns, 1364 exhaustive
+legal small-width complex pairs with exact inverses, 252 arbitrary-bit
+width/dimension roundtrips with exact traffic, and 24 full physical comparison
+paths with all tape cells and heads checked. Seven invalid-domain/instruction
+controls reject, and three semantic controls distinguish sign clearing,
+rotation direction and the CNOT swap identity. The source's compiler is used
+only to obtain this comparison circuit; its whole-word verifier and policy
+optimizer are not run. No predecessor result is claimed as a new audit.
+
+The selected word is a declared source-pinned input. The exact three-event
+window at indices 10481..10483 needs the two fields on both sides of SCALE.
+This establishes a relevant legal local contract, not a globally spliced
+replacement for the source policy. ORIGINS.json binds the retained external
+source bytes and their original Git blobs at PR6530's exact head. Those
+committed copies make replay independent of the unmerged source branch's
+ancestry; full predecessor history is not claimed.
+
+## Limits
+
+Only SCALE 2 is supplied. The complete caller policy is not reoptimized.
+Initial allocation, native/reset implementation, uniform encoded-D control,
+numerical admission, stock, full supplier funding and outer transfer remain
+open. A component improvement does not raise kappa or change the selected
+frontier. The five selected framework assumptions remain. Independent human
+and formal proof-kernel review are unclaimed. Lean, Docker and a selected
+supplier cold replay are outside scope.
+
+## Open next questions
+
+The structured questions in [TASK.json](TASK.json) concern integrating this
+exact edge into a complete certified policy, then one different SCALE
+coefficient with its full transition charged. Neither is reserved here.
+
+## Credit
+
+Ali Romman supplies PR6530's exclusive-owner contract, released question and
+comparison policy, PR6527's staging and PR6513/6511's physical scalar lineage.
+Credit Nick Petalas for the retained scalar circuits, Sagar Thakrar / PR3241,
+DreamingOfClouds / PR6030 and the retained native, owner, precision and compiler
+authors. Classical adjacent swaps, CNOT identities and two's-complement
+arithmetic retain their usual credit. Original source credit lines are retained
+unchanged in inputs. This contribution is under Apache-2.0.
+
+The replay-runtime card is explicitly changed to physical operation count.
+The first verified resident transition improvement ended the construction work.

research/resident-scale-ribbon/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"
+    }
+  ]
+}