From b1577bd405f5c7ade3616486b5fe44478e0ba5cb Mon Sep 17 00:00:00 2001 From: Hiroki KUMAZAKI Date: Sat, 24 Oct 2026 00:47:31 +0900 Subject: [PATCH] Bound retained backing across literal interchange call histories --- .../interchange-retained-backing/PROOF.md | 245 +++ .../interchange-retained-backing/README.md | 143 ++ .../interchange-retained-backing/RESULT.json | 1689 +++++++++++++++++ .../interchange-retained-backing/SOURCES.json | 54 + .../interchange-retained-backing/TASK.json | 111 ++ .../interchange-retained-backing/VERIFY.json | 35 + .../independent_check.py | 289 +++ .../interchange-retained-backing/verify.py | 250 +++ 8 files changed, 2816 insertions(+) create mode 100644 research/interchange-retained-backing/PROOF.md create mode 100644 research/interchange-retained-backing/README.md create mode 100644 research/interchange-retained-backing/RESULT.json create mode 100644 research/interchange-retained-backing/SOURCES.json create mode 100644 research/interchange-retained-backing/TASK.json create mode 100644 research/interchange-retained-backing/VERIFY.json create mode 100644 research/interchange-retained-backing/independent_check.py create mode 100644 research/interchange-retained-backing/verify.py diff --git a/research/interchange-retained-backing/PROOF.md b/research/interchange-retained-backing/PROOF.md new file mode 100644 index 0000000000..791811562d --- /dev/null +++ b/research/interchange-retained-backing/PROOF.md @@ -0,0 +1,245 @@ +# Retained backing of the literal elementary interchange + +This answers the retained-backing question in JoyboyBrian's +[PR5188](../literal-elementary-interchange/README.md), at source head +`bffbe6f4b31c102bbf53d12ebbefde6c1a86337a`. It gives exact capacities for +that unchanged program's fifteen private tapes, including erased backing +across varying successful calls. Its all-width interchange semantics and +instruction bound remain predecessor results; they are not reproved here. +The input hashes and source provenance are recorded in `SOURCES.json`. + +## 1. Domain, storage measure, and history + +For one call let `H>=0`, `A,G,S>=1`, and `V=A*4^H*G*S`. The five borrowed +ports have the source's canonical binary descriptors and `V` binary payload +cells, supplied at their required heads. All borrowed and private roles are +disjoint. A live owner's fifteen private tapes have a LEFT marker at index +zero and blank bodies at each call boundary. They may retain arbitrary +finite blank backing beyond the marker. + +A successful history consists of one `init`, followed by finitely many +admitted `run` calls, each followed by successful `consume` or `install`, +and optionally the terminal `close`. The borrowed input geometry may vary +between calls. Input replacement and descriptor production belong to the +caller. In particular, `install` is the source's paid copy-back entry, which +may change SOURCE; it has the same private-storage effect as consumption. +Malformed or interrupted executions and rollback are outside this theorem. + +The storage measure is the number of retained cells in the explicit tape +arrays. In the source `machine.py`, a read beyond an array returns BLANK +without extending it; a move changes the head only; a write at index `j` +extends the array to at least `j+1`. Erasure writes BLANK and never shrinks +an array. Thus a blank cell retained after a call still counts. + +Let `a_r>=1` be the retained length of private role `r` immediately after +`init`, and `K0=sum_r a_r`. A fresh minimal owner has `a_r=1` for every +role. Arbitrarily large erased entry tails are permitted, but their capacity +is included in `K0`. The statements below bound the complete private bank; +borrowed input backing and any caller-retained old input objects must be +added separately. The fixed instruction word and finite-control encoding +are constant program memory, excluded from the tape-cell totals. These are +logical tape cells, not CPython allocator capacity or heap metadata. + +Write `b(n)=max(1, bit_length(n))`, so the canonical zero word has one bit, +and put `d=max(H-1,0)`. An allocated numerical prefix of a `w`-bit word has +length `w+2`: LEFT, its bits, and RIGHT. A payload prefix of `v` bits has +length `v+1`: LEFT and its bits; its following BLANK may remain implicit. + +## 2. Exact capacities of one successful call + +For each role define the following capacity `c_r(H,A,G,S)`. It is the +retained length reached from a fresh minimal owner after `run` and its +consumption or installation, and bounds every write during that call. + +| Private role | Capacity | +| --- | ---: | +| PRE | `b(A)+d+2` | +| GAP | `b(G)+d+2` | +| TAIL | `b(S)+d+2` | +| SCAN, REMAIN, each | `b(H)+2` | +| OUTER | `b(A)+H+1` if `H>=1`, otherwise `1` | +| BETWEEN | `b(G)+H+1` if `H>=1`, otherwise `1` | +| BITS | `b(S)+H+1` if `H>=1`, otherwise `1` | +| Q00, Q01, Q10, Q11, each | `V/4+1` if `H>=1`, otherwise `1` | +| B0 | `V+1` if `H>=1`, otherwise `1` | +| B1 | `V+1` if `H>=2`, otherwise `1` | +| OUTPUT | `V+1` | + +For the numerical roles, setup copies `A,G,S,H` into PRE,GAP,TAIL,SCAN. +It doubles GAP and TAIL exactly `d` times and copies `H` into REMAIN. +For `H>0`, pass `i=0,...,H-1` has + +```text +PRE = A*2^i, +GAP = G*2^(H-1), +TAIL = S*2^(H-1-i). +``` + +Every pass actually occurs and all these values are positive. Therefore the +maximal bit lengths of PRE,GAP,TAIL are respectively `b(A)+H-1`, +`b(G)+H-1`, `b(S)+H-1`. The three nested counters copy these values into +OUTER,BETWEEN,BITS before decrementing them, so they attain the same respective +maxima. SCAN and REMAIN start at `H` and only decrease. + +The source helpers do not introduce a larger temporary prefix. `double` +adds at most one high bit and its RIGHT marker; `half` erases the old RIGHT +before moving it left. `dec` and `normalize` erase displaced delimiters; +the zero result is `0 RIGHT` and does not exceed the original positive +word's allocation. Copies write exactly the copied bits and RIGHT. +`clear` writes through the current nonblank body, including a numerical +RIGHT, then stops at its first BLANK. It does not scan a retained blank tail. +These facts also cover the transient states between canonical endpoints. + +Each positive-width pass has volume `4*PRE*GAP*TAIL=V`. Its four queues +each receive exactly `PRE*GAP*TAIL=V/4` bits, regardless of their values. +The first pass fills B0. The second fills B1 if and only if `H>=2`; +later passes alternate those same two roles. Every filled buffer has +exactly `V` bits. The selected buffer is copied into OUTPUT and erased. +Queue and buffer erasure cannot increase their allocated prefixes. + +For `H=0`, setup still writes PRE,GAP,TAIL,SCAN,REMAIN, including the +canonical zero SCAN and REMAIN. No pass or nested counter executes: all +four queues, both buffers and the three nested counters retain only LEFT. +The identity branch copies all `V` bits directly from SOURCE to OUTPUT. +This proves the `H=0` entries and explains why B1 also remains minimal +when `H=1`. + +All stated maxima are attained: copied numerical words include every bit +and their RIGHT marker; every nonempty queue/buffer/output writes its last +payload cell. The remaining cells in the table are the initialized LEFT +markers. `consume` clears OUTPUT, while `install` clears SOURCE, copies +OUTPUT there and clears OUTPUT. Neither entry writes beyond a private +capacity in the table. Terminal `close` erases only the fifteen LEFT +markers and leaves every array length unchanged. + +## 3. Exact history formula and a distinguishing example + +Let call `i` have geometry `g_i=(H_i,A_i,G_i,S_i)`. After `k>=1` successful +calls and their consumptions or installations, the exact retained private +length is + +```text +C_r(k) = max(a_r, c_r(g_1), ..., c_r(g_k)), +K(k) = sum_r C_r(k). +``` + +The formula holds at every completed prefix of the history. Its right side +also bounds all intervening writes. To prove it, start with the blank-body +entry invariant supplied by the predecessor. At a subsequent call, implicit +blank cells and explicitly retained blank cells give identical local read +results. Consequently the unchanged program follows the same instruction +trace as it would with minimal blank backing. The call writes through +exactly the prefixes in the table, and the machine extends only when a write +passes the old end. Cleanup restores the blank-body invariant without +shrinking either prefix. Induction gives the rolewise maxima. `close` does +not alter the result. + +The sum must be taken **after** the separate maxima. The maximum of the +single-call total capacities can be too small, even at fixed width and +volume. Take the three calls + +```text +(H,A,G,S) = (1,64,1,1), (1,1,64,1), (1,1,1,64). +``` + +All have `V=256`. The seven payload roles together retain `775` cells: +four queues of `65`, B0 and OUTPUT of `257`, and B1 of `1`. For each call +alone, two numerical roles have capacity `9` and the other six capacity +`3`, giving `775+36=811` cells. In order, the large role pairs are +PRE/OUTER, GAP/BETWEEN, and TAIL/BITS. On one owner their capacities +accumulate, so the total is `811`, then `823`, then `835`. At the end, +all private data are blank and all private heads are at one. + +This is a counterexample to replacing `sum_r max_i c_r(g_i)` by +`max_i sum_r c_r(g_i)`, not a failure of the predecessor interchange or +cleanup contract. Its written table derivation is corroborated by literal +short program runs; the receipt records that finite evidence separately. + +## 4. A grant uniform in the number of calls + +Let `Vmax=max_i V_i>=1` and `w=b(Vmax)`. Every numerical value appearing +in a call is at most its `V_i`: this follows directly from the three +pass values above, `A,G,S>=1`, and `H<=4^H<=V` for `H>=1`. At `H=0`, +the descriptor value zero still requires only one bit. The eight numerical +roles therefore each have capacity at most `w+2` over the entire history. + +Each queue has capacity at most `Vmax/4+1`: inactive `H=0` calls need +only its marker. B0, B1 and OUTPUT each need at most `Vmax+1`. For a fresh +minimal owner this yields + +```text +K(k) <= 8(w+2) + 4(Vmax/4+1) + 3(Vmax+1) + = 4Vmax + 8b(Vmax) + 23. +``` + +There is no factor `k`. Independent maxima in different calls are already +covered by the individual role grants. For arbitrary erased entry backing, +the exact rolewise formula in ยง3 applies. Since each `a_r>=1`, a convenient +safe total is + +```text +K(k) <= K0 + 4Vmax + 8b(Vmax) + 8. +``` + +This follows by bounding each role's possible growth beyond its initially +allocated marker; it does not discard the existing `K0` cells. A grant +using only the latest call's volume is not valid after a larger prior call. + +Allocated backing and visited cells are different measures. All private +head positions during one call lie between zero and `c_r`, inclusive: +the extra position is the first blank beyond a full allocated prefix. +The helper descriptions above give this bound for clear/copy/end probes; +init, close and unused-role checks visit at most positions zero and one. +Hence the union of private visited cells over a fresh-owner history is +conservatively bounded by + +```text +sum_r (max_i c_r(g_i)+1) <= 4Vmax + 8b(Vmax) + 38. +``` + +This is only a visited-cell upper bound, not a claim of exact equality. +Unvisited preexisting backing still belongs in an allocation grant. + +## 5. Analytic application at the retained CRT callee + +PR5188's declared actual u/back geometry is `H=2,A=1,G=1024,S=12`, +so `V=196608`. Substitution into the table gives numerical capacities + +```text +PRE GAP TAIL SCAN REMAIN OUTER BETWEEN BITS + 4 14 7 4 4 4 14 7 +``` + +Their sum is `58`. Each queue has `49153` cells, and B0, B1 and OUTPUT +each have `196609`. Thus the exact fresh private capacity is + +```text +58 + 4*49153 + 3*196609 = 786497 cells. +``` + +The uniform bound gives `786599` since `b(196608)=18`. This application +is arithmetic derived from the quantified proof, **not a new replay** of +the predecessor's approximately 64-million-instruction fixture. The +bounded new checks use smaller histories and separately test the capacities, +cleanup, retained tails and changed geometry. They do not constitute an +all-size proof by enumeration. + +## Attribution and remaining limits + +JoyboyBrian/#5188 supplies the unchanged literal program and the explicit +space handoff. PR5162 and Jose Manuel's physical ordinary wrapper supply +the retained callee/source refinement, with PR2809/PR2753 stream and +cardinality lineage. Cinna Davis supplies the CRT context; Hiroki KUMAZAKI, +Douglas Colkitt/OpenAI and the source archives retain their credited +contributions and notices. Ross Richardson's separate numerical-arena and +packet-backing audits already use historical capacity accounting; the new +claim binds this actual callee's extents, not that general principle. +This capacity audit is by Hiroki KUMAZAKI +(@kumagi), with substantial OpenAI Codex assistance, under Apache-2.0. + +The result bounds one private tape bank in the existing five-symbol model. +It neither initializes arbitrary dirty storage nor supplies borrowed +descriptors, a recursive/global allocator, a binary alphabet lowering, +raw/ROM/repair composition, a new time tariff, or a complete multiplication +supplier. The selected frontier and all predecessor sources are unchanged. +No independent human review or proof-kernel verification is claimed. diff --git a/research/interchange-retained-backing/README.md b/research/interchange-retained-backing/README.md new file mode 100644 index 0000000000..634ef15d65 --- /dev/null +++ b/research/interchange-retained-backing/README.md @@ -0,0 +1,143 @@ +# Retained backing across literal interchange calls + +The existing elementary interchange erases its scratch but retains its backing +arrays. This package answers [PR5188](https://github.com/CrocSwap/integer-mult-bounds/pull/5188) +open question 2 with an exact per-tape capacity theorem and a grant for any +finite successful call history. It audits the unchanged 4,589-instruction +program; it adds no new interchange implementation or multiplication bound. + +A fixed-volume example shows why the grant must use separate tape maxima: + +| Call `(H,A,G,S)` | Fresh owner alone | Same owner after this call | +| --- | ---: | ---: | +| `(1,64,1,1)` | 811 | 811 | +| `(1,1,64,1)` | 811 | 823 | +| `(1,1,1,64)` | 811 | 835 | + +Every call has volume 256, restores private heads and erases all private data. +Different numerical roles attain their maxima in different calls. Therefore +the maximum standalone total, 811, undercounts the retained history by 24 cells. +This is a counterexample to an accounting shortcut, not a source-program bug. + +## Quantified result and boundary + +For each admitted call, `H>=0`, `A,G,S>=1`, `V=A*4^H*G*S`. Let `c_r` be the +exact fresh capacity of private role `r` in [PROOF.md](PROOF.md)'s table, and +let `a_r>=1` be that role's already allocated, blank entry backing after init. +For every finite successful history, including consumption or paid installation +of every output, its retained private capacity is exactly + +```text +K(k) = sum_r max(a_r, c_r(call1), ..., c_r(callk)). +``` + +The table includes all eight numerical and seven payload roles, LEFT/RIGHT +markers, H=0's owned identity, H=1's unused B1, transient numerical writes, +repeated calls and terminal close. Erasure and close do not shrink backing. +Given maximum historical volume `Vmax>=1`, a fresh minimal bank satisfies + +```text +K(k) <= 4Vmax + 8 bit_length(Vmax) + 23. +``` + +For arbitrary blank entry backing of total `K0`, a sufficient grant is +`K0 + 4Vmax + 8 bit_length(Vmax) + 8`. Neither bound grows with the number +of calls. A bound using only the latest call's volume is invalid after a +larger call. The private visited span has a separate conservative fresh bound +`4Vmax + 8 bit_length(Vmax) + 38`: reads/moves can reach an implicit blank +cell without allocating it. This is not an equality between visited and +allocated cells. + +At the predecessor's actual CRT u/back geometry `(2,1,1024,12)`, the exact +fresh private capacity is **786,497 cells**, below the uniform grant 786,599. +This is an arithmetic application of the quantified theorem, **not a new +execution** of the 196,608-bit caller. + +The theorem assumes canonical disjoint borrowed ports and successful calls. +Input descriptor production/replacement, borrowed arrays and caller-retained +old inputs remain separately owned and charged. Dirty entry storage, failures, +interruptions and rollback are excluded. These are logical tape cells, not +CPython heap capacity or metadata. The fixed instruction word is constant +program memory. Source endpoint correctness and time bounds remain inherited; +no new binary alphabet lowering, recursive/global reserve, whole raw/repair +composition, supplier admission or selected-frontier change is claimed. + +## Evidence and reproduction + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/interchange-retained-backing --check-only +python3.12 -B scripts/research_package.py --package research/interchange-retained-backing +``` + +The registered runner executes ordinary and optimized modes. Direct portable +replay is `python3.12 -I -O -W error -B research/interchange-retained-backing/verify.py`. +It authenticates six live predecessor files before compiling their captured +source bytes; it does not import predecessor bytecode or run its full verifier. +Ordinary replay is read-only and compares the complete typed +[RESULT.json](RESULT.json). `--write-result` is explicit authoring mode. + +The primary checker executes the original machine on 110 fresh geometries +(H0..3 with A/G/S1..3, plus H4/H5), every order of the three fixed-volume +calls, and shrinking-volume and preallocated-owner histories. It checks each +output against a coordinate oracle, protected inputs, private cleanup/head +return, exact per-role retained lengths and the visited-span allowance. +A capacity guard intercepts every actual allocation; omitting the OUTPUT +marker's cell makes the real H0/V1 execution fail. + +The separately authored [independent checker](independent_check.py) represents +nonblank cells sparsely and retains allocation lengths separately. It imports +no geometry/cap formula or source interpreter. On fresh and warm mixed +histories, it compares all 16 entry boundaries with the original machine: +full allocated contents including blanks, lengths, heads, returned status and +exact instruction/read/write/move counts. An additional primitive probe +separates implicit-blank reads/moves from allocating writes. Executing the +same source word under wrong accounting that allocates reads or releases +erased backing is rejected. Other controls detect max-of-totals, discarded +entry backing, erased-content-only and current-volume-only grants. + +Finite checks corroborate the source proof; they do not prove all histories +by enumeration. No historical suite, full source-sized caller, Lean/Docker, +selected supplier replay or physical heap benchmark was run. + +## Task and overlap + +[Task metadata](TASK.json) refines priority 7 `uniform-transfer-audit` to the +explicit #5188 capacity handoff. Canonical base is +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`; exact blobs/SHA256 pins are in +[SOURCES.json](SOURCES.json). The canonical claim/result is +[Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19148693). + +The historical-maximum principle is already present in Ross Richardson's +[numerical-arena](../selected-numerical-arena-backing/README.md) and +[packet-backing](../selected-packet-retained-backing/README.md) audits. Those +concern different allocators/owners. The new result derives this literal +callee's exact extents and an actual mixed-history discriminator. The live +#4990 descriptor-production work, fixed-alphabet translation and complete +raw/repair composition are distinct tasks. + +## Open next questions + +The family decision is **narrow, then stop**. The next useful question is a +complete caller bank grant: identify one raw CRT call sequence, combine this +bank with simultaneously live borrowed/output/descriptor/ROM roles, and retain +object identities and old input ownership at every boundary. The current +private-bank theorem alone does not supply that global ledger. A fixed-block +binary translation must also charge its encoded backing; this result gives +cells in the existing five-symbol model only. [TASK.json](TASK.json) records +first steps and blockers. + +## Credit + +JoyboyBrian/#5188 supplies the literal program and open capacity question; +#5162, Jose Manuel's physical ordinary wrapper and the retained +PR2809/PR2753 stream/cardinality lineage supply its source context. Cinna Davis, +Hiroki KUMAZAKI, Douglas Colkitt/OpenAI and all archived notices retain their +CRT/physical-source credit. Ross Richardson's separate backing audits retain +their accounting-method credit. All predecessor bytes are unchanged. + +Prepared by Hiroki KUMAZAKI (@kumagi) with substantial OpenAI Codex assistance, +including separately authored proof/interpreter checks. This is not independent +human or proof-kernel acceptance. Apache-2.0. Selected conditional kappa remains +`.00302015`. diff --git a/research/interchange-retained-backing/RESULT.json b/research/interchange-retained-backing/RESULT.json new file mode 100644 index 0000000000..6b4e516abd --- /dev/null +++ b/research/interchange-retained-backing/RESULT.json @@ -0,0 +1,1689 @@ +{ + "actual_caller_derived_not_executed": { + "per_role": { + "B0": 196609, + "B1": 196609, + "BETWEEN": 14, + "BITS": 7, + "GAP": 14, + "OUTER": 4, + "OUTPUT": 196609, + "PRE": 4, + "Q00": 49153, + "Q01": 49153, + "Q10": 49153, + "Q11": 49153, + "REMAIN": 4, + "SCAN": 4, + "TAIL": 7 + }, + "shape": [ + 2, + 1, + 1024, + 12 + ], + "total": 786497, + "uniform_grant": 786599, + "volume": 196608 + }, + "authenticated_inputs": 6, + "controls": { + "actual_history_total": 835, + "allocation_guard_rejected": true, + "current_volume_only_rejected": true, + "erased_content_only_rejected": true, + "ignored_initial_backing_rejected": true, + "max_standalone_total": 811, + "missing_cells": 24, + "omitted_marker_rejected": true, + "typed_receipt_checked": true + }, + "independent": { + "controls": { + "erase_releases_backing": "retained length mismatch: PRE", + "read_allocates": "retained length mismatch: PRE" + }, + "fresh": [ + { + "actions": { + "moves": 15, + "reads": 15, + "status": "initialized", + "steps": 46, + "writes": 15 + }, + "call": null, + "canonical_compared": true, + "complete_snapshot_sha256": "c34afbad40ab72051315963d1842554d4c3de12c6f974cec797dbd63908645c0", + "entry": "init", + "growth_writes_total": 15, + "lengths": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "outside_moves_total": 15, + "outside_reads_total": 15, + "visited_span_total": 30 + }, + { + "actions": { + "moves": 29640, + "reads": 30079, + "status": "returned", + "steps": 82711, + "writes": 8540 + }, + "call": 0, + "canonical_compared": true, + "complete_snapshot_sha256": "2d86db444c877a307eded621cf6b402e3de837ac98a9e3d4d59c4a3d997c6c0a", + "entry": "run", + "growth_writes_total": 811, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "output_backing_sha256": "93b0e495cb95fdc56e4c10c3fe367d0e111244e98aada7485cb54603093941b6", + "outside_moves_total": 1586, + "outside_reads_total": 1601, + "visited_span_total": 825 + }, + { + "actions": { + "moves": 516, + "reads": 515, + "status": "consumed", + "steps": 1800, + "writes": 256 + }, + "call": 0, + "canonical_compared": true, + "complete_snapshot_sha256": "77a593606edcfa37e66567886fdf4e8bd07192a90e5f20df822ad67f993e87bf", + "entry": "consume", + "growth_writes_total": 811, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "outside_moves_total": 1587, + "outside_reads_total": 1602, + "visited_span_total": 825 + }, + { + "actions": { + "moves": 24344, + "reads": 25339, + "status": "returned", + "steps": 69341, + "writes": 6560 + }, + "call": 1, + "canonical_compared": true, + "complete_snapshot_sha256": "9ea6b96367c69beb3ac89a6afef01fe41c8376520632d6f737b05d6c65d3cdb0", + "entry": "run", + "growth_writes_total": 823, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "output_backing_sha256": "1c0663577d799f13d6ed8010e8997d94ab75285636090245d1cd0ff2ad7c318a", + "outside_moves_total": 2131, + "outside_reads_total": 2139, + "visited_span_total": 836 + }, + { + "actions": { + "moves": 516, + "reads": 515, + "status": "consumed", + "steps": 1800, + "writes": 256 + }, + "call": 1, + "canonical_compared": true, + "complete_snapshot_sha256": "133eb83be237dd68ec6736062fbdfdbf67328aa998ae8ad8208ef518ac4e4d63", + "entry": "consume", + "growth_writes_total": 823, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "outside_moves_total": 2132, + "outside_reads_total": 2140, + "visited_span_total": 836 + }, + { + "actions": { + "moves": 13752, + "reads": 15853, + "status": "returned", + "steps": 42601, + "writes": 2600 + }, + "call": 2, + "canonical_compared": true, + "complete_snapshot_sha256": "deb7e713da81a097c8e43d823e705177b590f0a781affd38cd16624554f17b27", + "entry": "run", + "growth_writes_total": 835, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "output_backing_sha256": "8a68ffca91c26cbf1e6f772fa205f9bf2108b12f2fc6f683f3e3478f91e065b8", + "outside_moves_total": 2163, + "outside_reads_total": 2164, + "visited_span_total": 847 + }, + { + "actions": { + "moves": 516, + "reads": 515, + "status": "consumed", + "steps": 1800, + "writes": 256 + }, + "call": 2, + "canonical_compared": true, + "complete_snapshot_sha256": "8a60fa19519515eba85ff830c0f76d175b35457d6dbe46003348d8cb3d0911d6", + "entry": "consume", + "growth_writes_total": 835, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "outside_moves_total": 2164, + "outside_reads_total": 2165, + "visited_span_total": 847 + }, + { + "actions": { + "moves": 30, + "reads": 30, + "status": "closed", + "steps": 76, + "writes": 15 + }, + "call": null, + "canonical_compared": true, + "complete_snapshot_sha256": "87efaa15fe1909166c8a38e0160bd1ad878c1d81cb371a21c38f31f4e2481b9b", + "entry": "close", + "growth_writes_total": 835, + "lengths": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "outside_moves_total": 2165, + "outside_reads_total": 2166, + "visited_span_total": 847 + } + ], + "primitive_allocation_probe": { + "entries": [ + { + "actions": { + "moves": 1, + "reads": 2, + "status": "returned", + "steps": 4, + "writes": 0 + }, + "after_length": 0, + "before_length": 0, + "entry": "observe", + "visited_span": 2 + }, + { + "actions": { + "moves": 0, + "reads": 0, + "status": "consumed", + "steps": 2, + "writes": 1 + }, + "after_length": 2, + "before_length": 0, + "entry": "write_blank", + "visited_span": 2 + } + ], + "role": "PRE" + }, + "receipt_sha256": "a6baa79f81b886dcc385a1332197649901d85c5659fc2c879827ea9dd67ebb71", + "warm_install": [ + { + "actions": { + "moves": 15, + "reads": 15, + "status": "initialized", + "steps": 46, + "writes": 15 + }, + "call": null, + "canonical_compared": true, + "complete_snapshot_sha256": "7477458263e4b0fb8595f44a6b10b8243166f40d952fa25472a4586d8bd1827f", + "entry": "init", + "growth_writes_total": 0, + "lengths": { + "B0": 1, + "B1": 4096, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 73, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "outside_moves_total": 13, + "outside_reads_total": 0, + "visited_span_total": 30 + }, + { + "actions": { + "moves": 29640, + "reads": 30079, + "status": "returned", + "steps": 82711, + "writes": 8540 + }, + "call": 0, + "canonical_compared": true, + "complete_snapshot_sha256": "786322e9ec8d6ccb9282a29c576221056662f00d83f45c7547455aa31a502615", + "entry": "run", + "growth_writes_total": 788, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "output_backing_sha256": "93b0e495cb95fdc56e4c10c3fe367d0e111244e98aada7485cb54603093941b6", + "outside_moves_total": 1577, + "outside_reads_total": 1577, + "visited_span_total": 825 + }, + { + "actions": { + "moves": 2060, + "reads": 2440, + "status": "installed", + "steps": 7190, + "writes": 768 + }, + "call": 0, + "canonical_compared": true, + "complete_snapshot_sha256": "e68162a6f54e12b7f0b836254dd1ff4126226d91acceaf85da2536b859ca68b4", + "entry": "install", + "growth_writes_total": 788, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "outside_moves_total": 1579, + "outside_reads_total": 1579, + "visited_span_total": 825 + }, + { + "actions": { + "moves": 24344, + "reads": 25339, + "status": "returned", + "steps": 69341, + "writes": 6560 + }, + "call": 1, + "canonical_compared": true, + "complete_snapshot_sha256": "971646bea3faed5d3625f4d9dd3c05c48874bf77da1f3fe5728adefe7be17912", + "entry": "run", + "growth_writes_total": 800, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "output_backing_sha256": "1c0663577d799f13d6ed8010e8997d94ab75285636090245d1cd0ff2ad7c318a", + "outside_moves_total": 2123, + "outside_reads_total": 2115, + "visited_span_total": 836 + }, + { + "actions": { + "moves": 2060, + "reads": 2442, + "status": "installed", + "steps": 7190, + "writes": 768 + }, + "call": 1, + "canonical_compared": true, + "complete_snapshot_sha256": "59de890ba866f6a37b65f0de1b211b6b865528c9ff820593151931fa14ce5c84", + "entry": "install", + "growth_writes_total": 800, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "outside_moves_total": 2125, + "outside_reads_total": 2117, + "visited_span_total": 836 + }, + { + "actions": { + "moves": 13752, + "reads": 15853, + "status": "returned", + "steps": 42601, + "writes": 2600 + }, + "call": 2, + "canonical_compared": true, + "complete_snapshot_sha256": "20e8b61b55123bdc6b90825b5b7ec71c95e228057e8952c809784087095386ee", + "entry": "run", + "growth_writes_total": 812, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "output_backing_sha256": "8a68ffca91c26cbf1e6f772fa205f9bf2108b12f2fc6f683f3e3478f91e065b8", + "outside_moves_total": 2156, + "outside_reads_total": 2140, + "visited_span_total": 847 + }, + { + "actions": { + "moves": 2060, + "reads": 2440, + "status": "installed", + "steps": 7190, + "writes": 768 + }, + "call": 2, + "canonical_compared": true, + "complete_snapshot_sha256": "4ad0e865073c1d50949f9c1f7ccee8271402dba2d8e7239c350454af0651c044", + "entry": "install", + "growth_writes_total": 812, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "outside_moves_total": 2158, + "outside_reads_total": 2142, + "visited_span_total": 847 + }, + { + "actions": { + "moves": 30, + "reads": 30, + "status": "closed", + "steps": 76, + "writes": 15 + }, + "call": null, + "canonical_compared": true, + "complete_snapshot_sha256": "6610d21815b909be229c9dbe81a957ab9fda0ab907b07499af4e42ef53572187", + "entry": "close", + "growth_writes_total": 812, + "lengths": { + "B0": 257, + "B1": 4096, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 73, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "outside_moves_total": 2158, + "outside_reads_total": 2142, + "visited_span_total": 847 + } + ] + }, + "program_sha256": "479f477b1e94564ea6abbad304095dc266db50dc0eb1318a94e980c8ee354052", + "shrinking_history": { + "calls": [ + { + "grant": 4207, + "output_sha256": "6036857bfd18643aa511fc7ff393e026260bc753bc838e2013d43ca2f854f468", + "retained": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 3, + "OUTER": 1, + "OUTPUT": 1025, + "PRE": 13, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 1059, + "shape": [ + 0, + 1024, + 1, + 1 + ], + "visited_span_total": 1074, + "volume": 1024 + }, + { + "grant": 4207, + "output_sha256": "bd93488966ea871290fe0eac8e095f7cfca7a6139cb32eab247c929db3681a17", + "retained": { + "B0": 17, + "B1": 17, + "BETWEEN": 4, + "BITS": 4, + "GAP": 4, + "OUTER": 4, + "OUTPUT": 1025, + "PRE": 13, + "Q00": 5, + "Q01": 5, + "Q10": 5, + "Q11": 5, + "REMAIN": 4, + "SCAN": 4, + "TAIL": 4 + }, + "retained_total": 1120, + "shape": [ + 2, + 1, + 1, + 1 + ], + "visited_span_total": 1129, + "volume": 16 + }, + { + "grant": 4207, + "output_sha256": "6b1e73a0094b7b812d3b9e22cffb4f8239319847522c4fa103753b6950020f93", + "retained": { + "B0": 17, + "B1": 17, + "BETWEEN": 4, + "BITS": 4, + "GAP": 4, + "OUTER": 4, + "OUTPUT": 1025, + "PRE": 13, + "Q00": 5, + "Q01": 5, + "Q10": 5, + "Q11": 5, + "REMAIN": 4, + "SCAN": 4, + "TAIL": 4 + }, + "retained_total": 1120, + "shape": [ + 1, + 1, + 1, + 1 + ], + "visited_span_total": 1129, + "volume": 4 + }, + { + "grant": 4207, + "output_sha256": "4bf5122f344554c53bde2ebb8cd2b7e3d1600ad631c385a5d7cce23c7785459a", + "retained": { + "B0": 17, + "B1": 17, + "BETWEEN": 4, + "BITS": 4, + "GAP": 4, + "OUTER": 4, + "OUTPUT": 1025, + "PRE": 13, + "Q00": 5, + "Q01": 5, + "Q10": 5, + "Q11": 5, + "REMAIN": 4, + "SCAN": 4, + "TAIL": 4 + }, + "retained_total": 1120, + "shape": [ + 0, + 1, + 1, + 1 + ], + "visited_span_total": 1129, + "volume": 1 + } + ], + "entries": 10, + "final_retained": { + "B0": 17, + "B1": 17, + "BETWEEN": 4, + "BITS": 4, + "GAP": 4, + "OUTER": 4, + "OUTPUT": 1025, + "PRE": 13, + "Q00": 5, + "Q01": 5, + "Q10": 5, + "Q11": 5, + "REMAIN": 4, + "SCAN": 4, + "TAIL": 4 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": false, + "steps": 33093 + }, + "single_call_bits": 19640, + "single_call_cases": 110, + "single_call_receipt_sha256": "475208a1c3880d675f79431f5c4bd3c85197fb4680a3cfd2001645427f8a5986", + "status": "PASS_INTERCHANGE_RETAINED_BACKING", + "varying_histories": [ + { + "calls": [ + { + "grant": 1119, + "output_sha256": "3f1acb5525375177cd1d42f64e25e0095063d58c2e469ef0cb4f04b23f0daa32", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 811, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "64860fb4f3ee7a36902aa514e7cdb2052267d98283afa33d2a80ca621c18b449", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 823, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "40011ffc9732c4c57f5c8dbe6fe4f72f7d014816c911e877279a2109f6afa033", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": false, + "steps": 200175 + }, + { + "calls": [ + { + "grant": 1119, + "output_sha256": "3f1acb5525375177cd1d42f64e25e0095063d58c2e469ef0cb4f04b23f0daa32", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 811, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "f98f6356521eb973e727f7d5caef82ed6ba4e603a64ea962d0a7a6c4f9ec396f", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 9, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 823, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "d57ff46cb2480295951d01487a7f6614b993ff8033159b8bd11f1a79be268070", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": true, + "steps": 216345 + }, + { + "calls": [ + { + "grant": 1119, + "output_sha256": "d57ff46cb2480295951d01487a7f6614b993ff8033159b8bd11f1a79be268070", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 811, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "40b80013827a6fda2af8e4473ba62c130643903faa6fe890a45feacbe36f495d", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 823, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "40011ffc9732c4c57f5c8dbe6fe4f72f7d014816c911e877279a2109f6afa033", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": false, + "steps": 200175 + }, + { + "calls": [ + { + "grant": 1119, + "output_sha256": "d57ff46cb2480295951d01487a7f6614b993ff8033159b8bd11f1a79be268070", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 3, + "GAP": 9, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 811, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "f98f6356521eb973e727f7d5caef82ed6ba4e603a64ea962d0a7a6c4f9ec396f", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 823, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "3f1acb5525375177cd1d42f64e25e0095063d58c2e469ef0cb4f04b23f0daa32", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": true, + "steps": 216345 + }, + { + "calls": [ + { + "grant": 1119, + "output_sha256": "40011ffc9732c4c57f5c8dbe6fe4f72f7d014816c911e877279a2109f6afa033", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 9, + "GAP": 3, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 811, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "40b80013827a6fda2af8e4473ba62c130643903faa6fe890a45feacbe36f495d", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 9, + "GAP": 3, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 823, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "d57ff46cb2480295951d01487a7f6614b993ff8033159b8bd11f1a79be268070", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": false, + "steps": 200175 + }, + { + "calls": [ + { + "grant": 1119, + "output_sha256": "40011ffc9732c4c57f5c8dbe6fe4f72f7d014816c911e877279a2109f6afa033", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 3, + "BITS": 9, + "GAP": 3, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 811, + "shape": [ + 1, + 1, + 1, + 64 + ], + "visited_span_total": 825, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "64860fb4f3ee7a36902aa514e7cdb2052267d98283afa33d2a80ca621c18b449", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 3, + "OUTPUT": 257, + "PRE": 3, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 823, + "shape": [ + 1, + 1, + 64, + 1 + ], + "visited_span_total": 836, + "volume": 256 + }, + { + "grant": 1119, + "output_sha256": "3f1acb5525375177cd1d42f64e25e0095063d58c2e469ef0cb4f04b23f0daa32", + "retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "retained_total": 835, + "shape": [ + 1, + 64, + 1, + 1 + ], + "visited_span_total": 847, + "volume": 256 + } + ], + "entries": 8, + "final_retained": { + "B0": 257, + "B1": 1, + "BETWEEN": 9, + "BITS": 9, + "GAP": 9, + "OUTER": 9, + "OUTPUT": 257, + "PRE": 9, + "Q00": 65, + "Q01": 65, + "Q10": 65, + "Q11": 65, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 9 + }, + "initial": { + "B0": 1, + "B1": 1, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 1, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": true, + "steps": 216345 + } + ], + "warm_history": { + "calls": [ + { + "grant": 4202, + "output_sha256": "6e340b9cffb37a989ca544e6bb780a2c78901d3fb33738768511a30617afa01d", + "retained": { + "B0": 1, + "B1": 4096, + "BETWEEN": 1, + "BITS": 1, + "GAP": 3, + "OUTER": 73, + "OUTPUT": 2, + "PRE": 3, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 4193, + "shape": [ + 0, + 1, + 1, + 1 + ], + "visited_span_total": 41, + "volume": 1 + }, + { + "grant": 4254, + "output_sha256": "91a2d4ccf52f4536e24988cffdf4061f250758f1f031cdb400aed38d6c87feee", + "retained": { + "B0": 9, + "B1": 4096, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 73, + "OUTPUT": 9, + "PRE": 4, + "Q00": 3, + "Q01": 3, + "Q10": 3, + "Q11": 3, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "retained_total": 4221, + "shape": [ + 1, + 2, + 1, + 1 + ], + "visited_span_total": 71, + "volume": 8 + } + ], + "entries": 6, + "final_retained": { + "B0": 9, + "B1": 4096, + "BETWEEN": 3, + "BITS": 3, + "GAP": 3, + "OUTER": 73, + "OUTPUT": 9, + "PRE": 4, + "Q00": 3, + "Q01": 3, + "Q10": 3, + "Q11": 3, + "REMAIN": 3, + "SCAN": 3, + "TAIL": 3 + }, + "initial": { + "B0": 1, + "B1": 4096, + "BETWEEN": 1, + "BITS": 1, + "GAP": 1, + "OUTER": 73, + "OUTPUT": 1, + "PRE": 1, + "Q00": 1, + "Q01": 1, + "Q10": 1, + "Q11": 1, + "REMAIN": 1, + "SCAN": 1, + "TAIL": 1 + }, + "install": false, + "steps": 3475 + } +} diff --git a/research/interchange-retained-backing/SOURCES.json b/research/interchange-retained-backing/SOURCES.json new file mode 100644 index 0000000000..8fa8281280 --- /dev/null +++ b/research/interchange-retained-backing/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/literal-elementary-interchange/PROOF.md", + "usage": "input", + "git_blob": "d4e14bba3fe10e0f269b0891b0e196b723b651cf", + "sha256": "507684173bde7865161d641bbffc6862c1e825407c42efa70747c763dadd03af" + }, + { + "path": "research/literal-elementary-interchange/README.md", + "usage": "input", + "git_blob": "b8305335be0124f0e5a3e3e997e7a7618fcf58f1", + "sha256": "49949811fcdf66151a02b5681eb723e68d18308f5346882086eb7b9874b7cee7" + }, + { + "path": "research/literal-elementary-interchange/RESULT.json", + "usage": "input", + "git_blob": "d2f4588b53837d22be39636c6661772196b594e9", + "sha256": "a8d4746eb333ea0fcb1d6f613f09b122f7d7a029390dab0df07a4cefb7164c73" + }, + { + "path": "research/literal-elementary-interchange/TASK.json", + "usage": "input", + "git_blob": "dbecea04476fad2c191b2fceb06a7d129ceb0cc2", + "sha256": "6af67f5e67ce3353a6734079f00849e37ccd4ea2c43e4a0e3736b12ebf498ba0" + }, + { + "path": "research/literal-elementary-interchange/machine.py", + "usage": "input", + "git_blob": "78dc14bf1c995b5ea348d2e753cf9f56dbdb480b", + "sha256": "66b5c371ff4aebd4391d71b95c59769a067e0a04910521b4881f074f986327bf" + }, + { + "path": "research/literal-elementary-interchange/program.py", + "usage": "input", + "git_blob": "c606ed51a06409a648d3fd385b0dfdaa5e096720", + "sha256": "3b83fbe3451000b00030ff3156222def23ce15d17d00c7d09a324aea5fd92e72" + } + ] +} diff --git a/research/interchange-retained-backing/TASK.json b/research/interchange-retained-backing/TASK.json new file mode 100644 index 0000000000..479f306243 --- /dev/null +++ b/research/interchange-retained-backing/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "PR5188 open question 2: exact per-role retained-backing envelope for successful literal elementary-interchange calls and arbitrary varying call histories.", + "scope_change_reason": "The source supplies an all-width literal program but explicitly separates fixed role count from retained array capacity. A local mixed-history discriminator shows that max of standalone total backing undercounts retained capacity.", + "bottleneck_link": "Closes one fixed-tape capacity premise for the actual all-width interchange callee, including erased backing. It does not compile the surrounding CRT caller or admit a full supplier.", + "budget_minutes": 60, + "stop_rule": "Prove exact per-role allocation caps and a history-wise maximum-volume grant; validate small varying histories and adverse accounting controls. Stop before binary lowering, full raw/repair execution, caller descriptor generation or selected-frontier changes.", + "outcome": "completed", + "evidence": "PROOF.md proves exact per-role history capacities and the maximum-volume private-bank grant. RESULT.json records110 fresh geometries, six varying fixed-volume histories, shrinking/warm controls and an independent sparse interpreter comparison. The source-sized786497-cell application is derived, not executed.", + "author": "Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; proof and independent accounting review delegated to separate agents. No human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "What is the complete simultaneously live backing grant of one actual raw CRT caller using this bank?", + "why_it_matters": "The fifteen private tapes exclude borrowed payload, descriptors, ROM and caller-retained old inputs; a local grant alone cannot admit global space.", + "first_step": "Pin one successful raw call sequence and keep the same object identities through input replacement, owned-output installation and terminal disposal; add every live and retained role to the ledger.", + "blocked_by": "An explicit complete caller ownership/lifecycle contract and fresh overlap check." + }, + { + "question": "What backing grant survives a fixed-block two-symbol translation of this exact program?", + "why_it_matters": "This theorem counts cells in the existing five-symbol model; encoding and alignment scratch must be charged separately.", + "first_step": "Use one admitted fixed-block translator, identify its per-role encoded extents and alignment/control scratch, and derive the translated historical maxima.", + "blocked_by": "The separate binary-translation program and complete source/target representation contract; this contribution does not claim that task." + } + ], + "family_decision": { + "decision": "narrow", + "milestone": "scoped source-capacity proof and independently implemented finite accounting check", + "proved": "Exact retained private role capacities, rolewise historical maxima, initial-backing charge and maximum-volume grant for successful calls.", + "inherited": "All-width endpoint, typed entry/cleanup, five-symbol instruction semantics and source time tariff.", + "unknown": "Simultaneous complete caller/recursive storage, borrowed input retention/transport, binary encoded space and full supplier admission.", + "reason": "The predecessor explicitly leaves retained arrays open; the actual mixed-history example falsifies max standalone total, and the new table supplies its missing local grant.", + "stop": "No new implementation family or complete caller run follows automatically." + }, + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19148693", + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T15:38:46+00:00", + "relevant_changes": "Final fetched canonical main remains the round base. Core guidance, selected record and all six source inputs unchanged." + }, + "selection": { + "handoff": "PR5188 open question2; current Discussion4709 comment19144824", + "reason": "A named missing capacity implication with an actual fixed-volume counterexample; distinct from the claimed #4990 descriptor successor.", + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY using research_selected_baseline.py; selected kappa .00302015 unchanged.", + "initial_overlap": { + "local_head_note_paths": 7091, + "complete_local_inventory": true, + "open_pr_bodies": 339, + "open_pr_fetched_at": "2026-10-23T15:18:26.299176+00:00", + "discussion_records": 4536, + "discussion_fetched_at": "2026-10-23T15:26:01.683570+00:00", + "complete_remote_pagination": true + }, + "limits": "Title/body/Discussion/local-note checks and targeted live handoffs; not arbitrary diffs or unpublished work." + } +} diff --git a/research/interchange-retained-backing/VERIFY.json b/research/interchange-retained-backing/VERIFY.json new file mode 100644 index 0000000000..422e2ca622 --- /dev/null +++ b/research/interchange-retained-backing/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/literal-elementary-interchange/PROOF.md", + "research/literal-elementary-interchange/README.md", + "research/literal-elementary-interchange/RESULT.json", + "research/literal-elementary-interchange/TASK.json", + "research/literal-elementary-interchange/machine.py", + "research/literal-elementary-interchange/program.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate six source inputs; execute exact source program with capacity guards, varied and warm histories; compare an independent sparse interpreter; reject accounting shortcuts and compare frozen typed receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticate six source inputs; execute exact source program with capacity guards, varied and warm histories; compare an independent sparse interpreter; reject accounting shortcuts and compare frozen typed receipt." + } + ] +} diff --git a/research/interchange-retained-backing/independent_check.py b/research/interchange-retained-backing/independent_check.py new file mode 100644 index 0000000000..bb9b9dec6a --- /dev/null +++ b/research/interchange-retained-backing/independent_check.py @@ -0,0 +1,289 @@ +"""Checker-only sparse execution of the retained local-symbol instruction word. + +No geometry, capacity formula, assembler or source-machine module is imported. +Nonblank symbols, allocated prefix length and visited head span are separate +state: in particular a blank write allocates, while a read or move does not. +""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class SparseMachine: + """An independent interpreter with exact array-allocation observations. + + ``load_borrowed`` replaces only the supplied roles with encoded arrays and + head 1. ``initialize_private`` sets initially blank backing and head 0. + ``execute`` returns the same five counters/status as the canonical machine. + ``snapshot`` reports cumulative head spans and allocation-event counters. + """ + + def __init__(self, code, entries, roles, blank=4): + self.code, self.entries, self.blank = code, entries, blank + self.roles = tuple(roles) + require(len(set(self.roles)) == len(self.roles), "distinct roles") + self.cells = {role: {} for role in self.roles} + self.lengths = dict.fromkeys(self.roles, 0) + self.heads = dict.fromkeys(self.roles, 0) + self.spans = dict.fromkeys(self.roles, 1) + self.growth_writes = dict.fromkeys(self.roles, 0) + self.outside_reads = dict.fromkeys(self.roles, 0) + self.outside_moves = dict.fromkeys(self.roles, 0) + + def initialize_private(self, lengths): + for role, length in lengths.items(): + require(role in self.cells and type(length) is int and length >= 0, + "nonnegative initial private length") + self.cells[role] = {} + self.lengths[role], self.heads[role], self.spans[role] = length, 0, 1 + + def load_borrowed(self, encoded, head=1): + for role, values in encoded.items(): + require(role in self.cells, "known borrowed role") + values = tuple(values) + require(type(head) is int and head >= 0, "nonnegative borrowed head") + self.cells[role] = {i: value for i, value in enumerate(values) + if value != self.blank} + self.lengths[role] = len(values) + self.heads[role], self.spans[role] = head, head + 1 + self.growth_writes[role] = 0 + self.outside_reads[role] = 0 + self.outside_moves[role] = 0 + + def execute(self, entry, max_steps=1000000000): + pc = self.entries[entry] if isinstance(entry, str) else entry + counts = dict(steps=0, reads=0, writes=0, moves=0) + while counts["steps"] < max_steps: + require(type(pc) is int and 0 <= pc < len(self.code), "program counter") + op, *args = self.code[pc] + counts["steps"] += 1 + if op == "halt": + return dict(status=args[0], **counts) + if op == "jump": + pc = args[0] + continue + role = args[0] + require(role in self.cells, "instruction role") + head = self.heads[role] + self.spans[role] = max(self.spans[role], head + 1) + if op == "test": + _, symbol, yes, no = args + if head >= self.lengths[role]: + self.outside_reads[role] += 1 + value = self.cells[role].get(head, self.blank) + counts["reads"] += 1 + pc = yes if value == symbol else no + continue + if op == "write": + symbol = args[1] + if head >= self.lengths[role]: + self.lengths[role] = head + 1 + self.growth_writes[role] += 1 + if symbol == self.blank: + self.cells[role].pop(head, None) + else: + self.cells[role][head] = symbol + counts["writes"] += 1 + elif op == "move": + target = head + args[1] + require(target >= 0, "left boundary") + self.heads[role] = target + self.spans[role] = max(self.spans[role], target + 1) + if target >= self.lengths[role]: + self.outside_moves[role] += 1 + counts["moves"] += 1 + else: + raise ValueError("unknown local instruction") + pc += 1 + raise ValueError("independent observer watchdog") + + def compare_snapshot(self, tapes, heads, roles=None): + """Compare all allocated cells, including erased retained tails.""" + for role in self.roles if roles is None else roles: + require(self.lengths[role] == len(tapes[role]), + "retained length mismatch: " + role) + require(self.heads[role] == heads[role], "head mismatch: " + role) + require(all(self.cells[role].get(i, self.blank) == value + for i, value in enumerate(tapes[role])), + "allocated cell mismatch: " + role) + require(all(0 <= i < self.lengths[role] for i in self.cells[role]), + "sparse cell outside backing: " + role) + + def snapshot(self, roles=None): + chosen = self.roles if roles is None else tuple(roles) + return { + "lengths": {r: self.lengths[r] for r in chosen}, + "heads": {r: self.heads[r] for r in chosen}, + "visited_spans": {r: self.spans[r] for r in chosen}, + "growth_writes": {r: self.growth_writes[r] for r in chosen}, + "outside_reads": {r: self.outside_reads[r] for r in chosen}, + "outside_moves": {r: self.outside_moves[r] for r in chosen}, + } + + +def exercise_history(code, entries, canonical_execute, borrowed_calls, *, + private_roles, initial_lengths=None, endings=None, + max_steps=1000000000, output_role="OUTPUT", + observer_mutation=None): + """Compare two executors after every entry of a bounded encoded history. + + ``borrowed_calls`` contains dictionaries role -> complete encoded array; + it supplies no H/A/G/S geometry to this checker. ``endings`` optionally + chooses consume/install per call. Returned snapshots include the complete + OUTPUT backing at each returned cut, for a separate payload oracle. + ``observer_mutation``, used only by the negative controls below, changes + the independent accounting state before its canonical comparison. + """ + calls = tuple(borrowed_calls) + require(calls, "nonempty bounded history") + borrowed = tuple(calls[0]) + private = tuple(private_roles) + require(not set(borrowed) & set(private), "disjoint borrowed/private roles") + require(all(set(call) == set(borrowed) for call in calls), "fixed borrowed roles") + lengths = dict.fromkeys(private, 0) + if initial_lengths is not None: + require(set(initial_lengths) <= set(private), "private initial backing only") + lengths.update(initial_lengths) + require(all(type(n) is int and n >= 0 for n in lengths.values()), + "nonnegative integer initial backing") + endings = tuple(endings) if endings is not None else ("consume",) * len(calls) + require(len(endings) == len(calls) and all(x in ("consume", "install") for x in endings), + "one permitted disposal entry per call") + roles = borrowed + private + sparse = SparseMachine(code, entries, roles) + sparse.initialize_private(lengths) + tapes = {r: [sparse.blank] * lengths[r] for r in private} + heads = dict.fromkeys(private, 0) + snapshots = [] + + def load(call): + sparse.load_borrowed(call) + for role, encoded in call.items(): + tapes[role], heads[role] = list(encoded), 1 + + def run(entry, call_index): + actual = canonical_execute(code, tapes, heads, entries[entry], max_steps=max_steps) + independent = sparse.execute(entry, max_steps=max_steps) + require(actual == independent, "independent action/status mismatch: " + entry) + if observer_mutation is not None: + observer_mutation(sparse, entry) + sparse.compare_snapshot(tapes, heads) + expected = {"init": "initialized", "run": "returned", "consume": "consumed", + "install": "installed", "close": "closed"}[entry] + require(actual["status"] == expected, "successful source entry: " + entry) + record = dict(entry=entry, call=call_index, actions=actual, + canonical_compared=True, **sparse.snapshot(private)) + if entry == "run": + record["output_cells"] = list(tapes[output_role]) + snapshots.append(record) + + load(calls[0]) + run("init", None) + for i, (call, ending) in enumerate(zip(calls, endings)): + if i: + load(call) + run("run", i) + run(ending, i) + run("close", None) + return snapshots + + +def run_checks(code, entries, canonical_execute, roles, private, borrowed, + borrowed_calls, initial_lengths): + """Root-verifier adapter; all geometries remain outside this module.""" + from hashlib import sha256 + import json + + require(set(roles) == set(private) | set(borrowed), "complete role inventory") + require(all(set(call) == set(borrowed) for call in borrowed_calls), + "complete encoded borrowed inputs") + fresh = exercise_history(code, entries, canonical_execute, borrowed_calls, + private_roles=private) + warm = exercise_history(code, entries, canonical_execute, borrowed_calls, + private_roles=private, initial_lengths=initial_lengths, + endings=["install"] * len(borrowed_calls)) + + class AllocatingRead(dict): + def __init__(self, values, owner, role): + super().__init__(values) + self.owner, self.role = owner, role + + def get(self, index, default=None): + self.owner.lengths[self.role] = max(self.owner.lengths[self.role], index + 1) + return super().get(index, default) + + def read_allocates(owner, entry): + if entry == "init": + for role in private: + owner.cells[role] = AllocatingRead(owner.cells[role], owner, role) + + def erase_releases(owner, entry): + if entry == "consume": + for role in private: + owner.lengths[role] = max(owner.cells[role], default=-1) + 1 + + controls = {} + for name, mutation in (("read_allocates", read_allocates), + ("erase_releases_backing", erase_releases)): + try: + exercise_history(code, entries, canonical_execute, borrowed_calls[:1], + private_roles=private, observer_mutation=mutation) + except ValueError as error: + require("retained length mismatch:" in str(error), + "accounting control rejected for its intended reason") + controls[name] = str(error) + else: + raise ValueError("accounting mutant accepted: " + name) + + # Use one admitted role and the canonical instruction interpreter itself. + # First read/move over implicit blanks; only the second entry writes one. + role = private[0] + probe_code = (("test", role, 4, 1, 6), ("move", role, 1), + ("test", role, 4, 3, 6), ("halt", "returned"), + ("write", role, 4), ("halt", "consumed"), ("halt", "rejected")) + probe_entries = {"observe": 0, "write_blank": 4} + probe = SparseMachine(probe_code, probe_entries, (role,)) + probe_tapes, probe_heads = {role: []}, {role: 0} + probe_records = [] + for entry in ("observe", "write_blank"): + before = len(probe_tapes[role]) + actual = canonical_execute(probe_code, probe_tapes, probe_heads, probe_entries[entry]) + independent = probe.execute(entry) + require(actual == independent, "primitive action/status agreement") + require(actual["status"] == ("returned" if entry == "observe" else "consumed"), + "implicit blank probe accepted") + probe.compare_snapshot(probe_tapes, probe_heads) + probe_records.append(dict(entry=entry, before_length=before, + after_length=len(probe_tapes[role]), + visited_span=probe.spans[role], actions=actual)) + require(probe_records[0]["after_length"] == 0 and + probe_records[1]["before_length"] == 0 and + probe_records[1]["after_length"] == 2 and + probe_tapes[role] == [4, 4], + "implicit reads/moves preserve backing; blank write allocates") + + def serialized(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + def compact(records): + answer = [] + for record in records: + summary = {key: record[key] for key in + ("entry", "call", "actions", "lengths", "canonical_compared")} + summary["complete_snapshot_sha256"] = sha256(serialized(record)).hexdigest() + for source, target in (("visited_spans", "visited_span_total"), + ("growth_writes", "growth_writes_total"), + ("outside_reads", "outside_reads_total"), + ("outside_moves", "outside_moves_total")): + summary[target] = sum(record[source].values()) + if "output_cells" in record: + summary["output_backing_sha256"] = sha256(bytes(record["output_cells"])).hexdigest() + answer.append(summary) + return answer + + result = {"fresh": compact(fresh), "warm_install": compact(warm), "controls": controls, + "primitive_allocation_probe": {"role": role, "entries": probe_records}} + result["receipt_sha256"] = sha256(serialized(result)).hexdigest() + return result diff --git a/research/interchange-retained-backing/verify.py b/research/interchange-retained-backing/verify.py new file mode 100644 index 0000000000..5424d03a06 --- /dev/null +++ b/research/interchange-retained-backing/verify.py @@ -0,0 +1,250 @@ +"""Source-bound retained-backing audit for PR5188's literal interchange. + +Hiroki KUMAZAKI (@kumagi), substantial OpenAI Codex assistance. Apache-2.0. +Geometry, capacity arithmetic and endpoint oracles are observers only. +""" +from __future__ import annotations + +import argparse +import hashlib +from itertools import permutations, product +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PARENT = 'research/literal-elementary-interchange/' +NUMERIC = ('PRE', 'GAP', 'TAIL', 'SCAN', 'REMAIN', 'OUTER', 'BETWEEN', 'BITS') + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def load(name, filename, raw): + module = types.ModuleType(name) + module.__file__ = str(filename) + sys.modules[name] = module + exec(compile(raw, str(filename), 'exec'), module.__dict__) + return module + + +def authenticate(): + captured = {} + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': + continue + raw = (ROOT/row['path']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256 mismatch: '+row['path']) + need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'source Git blob mismatch: '+row['path']) + captured[row['path']] = raw + need(len(captured) == 6, 'six declared source inputs') + return captured + + +def volume(shape): + h, a, g, s = shape + need(type(h) is int and h >= 0 and all(type(v) is int and v >= 1 for v in (a, g, s)), + 'admitted geometry') + return a*4**h*g*s + + +def caps(shape): + """Exact largest written index plus one, from a fresh blank private bank.""" + h, a, g, s = shape + v, d = volume(shape), max(h-1, 0) + widths = dict(zip(('PRE', 'GAP', 'TAIL'), (x.bit_length()+d+2 for x in (a, g, s)))) + result = dict(widths) + result.update(SCAN=max(1, h.bit_length())+2, REMAIN=max(1, h.bit_length())+2) + result.update({counter: widths[word] if h else 1 + for counter, word in zip(('OUTER', 'BETWEEN', 'BITS'), ('PRE', 'GAP', 'TAIL'))}) + result.update({r: 1+v//4 if h else 1 for r in ('Q00', 'Q01', 'Q10', 'Q11')}) + result.update(B0=v+1 if h else 1, B1=v+1 if h > 1 else 1, OUTPUT=v+1) + return result + + +def grant(v): + need(type(v) is int and v >= 1, 'positive historical maximum') + return 4*v+8*v.bit_length()+23 + + +class BoundedArray(bytearray): + """Observer guard: the original machine alone performs all tape writes.""" + def extend(self, data): + data = bytes(data) + need(len(self)+len(data) <= self.limit, 'private capacity exceeded') + super().extend(data) + + +class Heads(dict): + def __init__(self, values): + super().__init__(values) + self.peak = dict(values) + + def __setitem__(self, key, value): + need(value >= 0, 'head crossed origin') + self.peak[key] = max(self.peak.get(key, 0), value) + super().__setitem__(key, value) + + +def borrowed(shape, program, salt=0): + h, a, g, s = shape + bits = [((i*13) ^ (i//3) ^ (i//7) ^ salt) & 1 for i in range(volume(shape))] + result = {'SOURCE': bytearray([program.LEFT]+bits)} + for name, value in zip(('H', 'A', 'G', 'S'), shape): + result[name] = bytearray([program.LEFT]+[int(x) for x in reversed(bin(value)[2:])]+[program.RIGHT]) + return result, bits + + +def endpoint(bits, shape): + h, a, g, s = shape + n = 1 << h + # Independent direct coordinate gather; no digit pass or queue construction. + return bytearray(bits[((((prefix*n+y)*g+middle)*n+x)*s+tail)] + for prefix in range(a) for x in range(n) for middle in range(g) + for y in range(n) for tail in range(s)) + + +def run_history(program, machine, code, entries, shapes, initial=None, install=False, undergrant=None): + initial = initial or {r: 1 for r in program.PRIVATE} + tapes = {r: BoundedArray([program.BLANK]*initial[r]) for r in program.PRIVATE} + expected = {r: max(1, initial[r]) for r in program.PRIVATE} + for r in program.PRIVATE: + tapes[r].limit = expected[r] + heads = Heads({r: 0 for r in program.PRIVATE}) + events, records = [], [] + + def invoke(name): + row = machine.execute(code, tapes, heads, entries[name], max_steps=30000000) + need(row['status'] == {'init':'initialized','run':'returned','consume':'consumed', + 'install':'installed','close':'closed'}[name], 'entry '+name) + events.append(row) + + def empty(closed=False): + for r in program.PRIVATE: + need(heads[r] == 1 and tapes[r][0] == (program.BLANK if closed else program.LEFT) + and all(x == program.BLANK for x in tapes[r][1:]), 'private cleanup '+r) + + invoke('init') + vmax = 0 + for ordinal, shape in enumerate(shapes): + inputs, bits = borrowed(shape, program, ordinal) + for r, cells in inputs.items(): + tapes[r] = cells + heads[r] = 1 + before = {r: bytes(tapes[r]) for r in program.BORROWED} + call_caps = caps(shape) + expected = {r: max(expected[r], call_caps[r]) for r in program.PRIVATE} + for r in program.PRIVATE: + tapes[r].limit = expected[r] - (r == undergrant) + invoke('run') + answer = endpoint(bits, shape) + need(tapes['OUTPUT'][1:1+len(bits)] == answer, 'actual output endpoint') + need(all(x == program.BLANK for x in tapes['OUTPUT'][1+len(bits):]), 'output blank tail') + need(all(bytes(tapes[r]) == before[r] and heads[r] == 1 for r in program.BORROWED), + 'borrowed bytes and heads') + invoke('install' if install else 'consume') + if install: + need(tapes['SOURCE'][1:] == answer and heads['SOURCE'] == 1, 'paid source installation') + empty() + actual = {r: len(tapes[r]) for r in program.PRIVATE} + need(actual == expected, 'exact rolewise history identity') + touched = {r: heads.peak[r]+1 for r in program.PRIVATE} + need(all(touched[r] <= expected[r]+1 for r in program.PRIVATE), 'one boundary cell visit allowance') + vmax = max(vmax, volume(shape)) + warm_grant = sum(max(1, initial[r])-1 for r in program.PRIVATE)+grant(vmax) + need(sum(actual.values()) <= warm_grant, 'complete maximum-volume grant') + records.append({'shape':shape,'volume':volume(shape),'retained':actual, + 'retained_total':sum(actual.values()),'visited_span_total':sum(touched.values()), + 'grant':warm_grant,'output_sha256':hashlib.sha256(answer).hexdigest()}) + invoke('close') + empty(True) + need({r:len(tapes[r]) for r in program.PRIVATE} == expected, 'close does not release backing') + return {'initial':initial,'install':install,'calls':records,'final_retained':expected, + 'steps':sum(r['steps'] for r in events),'entries':len(events)} + + +def accounting_controls(program, machine, code, entries, witness, shrinking, warm): + rows = witness['calls'] + standalone = [sum(caps(tuple(r['shape'])).values()) for r in rows] + need(standalone == [811]*3 and [r['retained_total'] for r in rows] == [811,823,835], + 'fixed-volume history discriminator') + need(rows[-1]['retained_total'] > max(standalone), 'max standalone total wrongly accepted') + need(rows[-1]['retained_total'] > len(program.PRIVATE), 'erased nonblank-only count wrongly accepted') + last = shrinking['calls'][-1] + need(last['retained_total'] > grant(last['volume']), 'current-volume-only grant wrongly accepted') + last = warm['calls'][-1] + need(last['retained_total'] > grant(last['volume']), 'fresh grant ignored initial backing') + try: + run_history(program,machine,code,entries,[(0,1,1,1)],undergrant='OUTPUT') + except ValueError as exc: + need('private capacity exceeded' in str(exc), 'actual undergrant failure reason') + else: + raise ValueError('actual machine accepted omitted OUTPUT marker capacity') + try: + a = BoundedArray([program.BLANK]);a.limit = 1;a.extend([program.BLANK]) + except ValueError as exc: + need('capacity exceeded' in str(exc), 'capacity guard failure reason') + else: + raise ValueError('capacity guard inactive') + need(canonical({'n':1}) != canonical({'n':True}) != canonical({'n':1.0}), 'typed receipt control') + return {'max_standalone_total':811,'actual_history_total':835,'missing_cells':24, + 'erased_content_only_rejected':True,'current_volume_only_rejected':True, + 'ignored_initial_backing_rejected':True,'omitted_marker_rejected':True, + 'allocation_guard_rejected':True,'typed_receipt_checked':True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + captured = authenticate() + p = load('program', ROOT/(PARENT+'program.py'), captured[PARENT+'program.py']) + m = load('retained_source_machine', ROOT/(PARENT+'machine.py'), captured[PARENT+'machine.py']) + code, entries = p.assemble() + need(len(code) == 4589 and m.validate(code,entries) == 3, 'pinned finite program') + source_result = json.loads(captured[PARENT+'RESULT.json']) + need(hashlib.sha256(canonical((code,entries)).encode()).hexdigest() == source_result['program_sha256'], + 'source program receipt') + fixtures = [run_history(p,m,code,entries,[(h,a,g,s)]) for h,a,g,s in product(range(4),range(1,4),range(1,4),range(1,4))] + fixtures.extend(run_history(p,m,code,entries,[shape]) for shape in ((4,1,1,1),(5,1,1,1))) + varied = ((1,64,1,1),(1,1,64,1),(1,1,1,64)) + histories = [run_history(p,m,code,entries,list(order),install=(i % 2 == 1)) + for i,order in enumerate(permutations(varied))] + shrinking = run_history(p,m,code,entries,[(0,1024,1,1),(2,1,1,1),(1,1,1,1),(0,1,1,1)]) + initial = {r:1 for r in p.PRIVATE};initial['B1']=4096;initial['OUTER']=73 + warm = run_history(p,m,code,entries,[(0,1,1,1),(1,2,1,1)],initial=initial) + controls = accounting_controls(p,m,code,entries,histories[0],shrinking,warm) + actual = (2,1,1024,12) + result = {'status':'PASS_INTERCHANGE_RETAINED_BACKING','authenticated_inputs':len(captured), + 'program_sha256':source_result['program_sha256'],'single_call_cases':len(fixtures), + 'single_call_bits':sum(x['calls'][0]['volume'] for x in fixtures), + 'single_call_receipt_sha256':hashlib.sha256(canonical(fixtures).encode()).hexdigest(), + 'varying_histories':histories,'shrinking_history':shrinking,'warm_history':warm, + 'controls':controls,'actual_caller_derived_not_executed':{'shape':actual,'volume':volume(actual), + 'per_role':caps(actual),'total':sum(caps(actual).values()),'uniform_grant':grant(volume(actual))}} + # The separately authored sparse interpreter checks the same unchanged instruction table. + independent = load('independent_backing_check', HERE/'independent_check.py', (HERE/'independent_check.py').read_bytes()) + result['independent'] = independent.run_checks(code,entries,m.execute,p.ROLES,p.PRIVATE,p.BORROWED, + [{k:bytes(v) for k,v in borrowed(shape,p,i)[0].items()} for i,shape in enumerate(varied)], initial) + encoded = json.dumps(result,indent=2,sort_keys=True)+'\n' + receipt = HERE/'RESULT.json' + if args.write_result: + receipt.write_text(encoded) + else: + need(receipt.read_text() == encoded, 'frozen RESULT.json differs; nothing rewritten') + print(result['status']) + print('110 fresh geometries; six fixed-volume mixed histories; shrinking and warm-owner controls') + print('811 -> 823 -> 835 retained cells; source-sized 786497-cell cap derived, not replayed') + + +if __name__ == '__main__': + main()