Sparse RAM register stores on Turing tapes #
This module exposes the representation boundary used by the RAM-to-Turing- machine simulation. A canonical finite list of nonzero address/value pairs decodes to the RAM model's total register file. Functional reads and writes are exact, every finite-support register file has a canonical representation, and the self-delimiting binary snapshot codec round-trips.
The concrete length theorem is the first resource bridge for the reverse
simulation: if the program counter, entry count, addresses, and values all have
bit-width at most w, a snapshot with m entries occupies at most
(m + 1) * (4 * w + 2) tape cells.
Sparse writing implements functional update exactly when addresses are unique.
Decoding after a sparse write is exactly functional update.
Materializing any finite-support register file gives a canonical exact representation.
The canonical public-input store has at most one entry per initialized register.
One sparse write increases the actual encoded store by at most the code of the address/value pair being written. Replacement and deletion can only make this estimate smaller.
The explicit finite public-input snapshot decodes to RAM.initCfg.
Materializing a finite-support RAM configuration gives a canonical exact snapshot.
Decoding commutes exactly with one sparse interpreter instruction.
One sparse interpreter instruction grows the intrinsic width only to the maximum of the old width plus one, its fixed literal width, and its charged logarithmic runtime width.
A selected sparse step is bounded by the fixed program's literal width and the RAM step's logarithmic charge.
Each RAM instruction materializes at most one additional sparse entry.
Along a canonical sparse run, width grows linearly with executed fuel, the fixed program literal width, and accumulated logarithmic RAM time.
The live sparse-store code has amortized growth controlled by the resources actually charged by the RAM run. In particular, this avoids the spurious product of the number of entries and the maximum entry width: each executed instruction pays once for its fixed destination width and for the operand/result bits in its logarithmic cost.
A width-w, m-entry RAM snapshot occupies at most
(m + 1) * (4 * w + 2) Turing-tape cells.
A snapshot code is bounded by its actual live-entry encoding plus the two
header words. This is the width-sensitive alternative to the product envelope
Snapshot.sizeBound.
Combining the actual live-store charge with the width invariant gives a linear-in-accumulated-cost representation bound for every canonical sparse run, relative to the initial sparse encoding.
The materialized public-input store occupies at most one fixed-width entry
per initialized register. This records the current ABI's explicit
O(n log n) initialization term.
Public-input specialization of the amortized live-representation bound.
The accumulated part is linear in charged RAM time; the separate
n * bitlen n term comes from eagerly materializing all nonzero input
registers in the current snapshot ABI.
The canonical code of every reachable snapshot has an explicit product bound: entry count grows by at most one per step, while width grows only with fixed program literals and charged logarithmic RAM time.
Eliminating actual step count via unitTimeUpto ≤ logTimeUpto gives a
pure logarithmic-time tape-size envelope. This is the quadratic representation
bound needed by the RAM-to-TM simulation.
From the public RAM ABI, every reachable snapshot code has an explicit quadratic envelope in input length, logarithmic RAM time, and one fixed program constant.