Emit a complete packed TM backend with exact simulation costs (no κ)

research/emitted-packed-tm/PROOF.md

@@ -0,0 +1,187 @@
+# Simulation theorem for the emitted packed backend
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Fix a deterministic finite multitape machine with k tapes, alphabet
+{0,...,A-1}, blank 0, Q states and initial state 0. A transition maps a state
+and the simultaneous k observed symbols to a new state, k symbols and k moves
+in {-1,0,1}. A missing transition halts without changing the tapes. All heads
+begin at signed coordinate zero. Tape i initially has its supplied finite word
+at coordinates 0 through ell_i-1 and blanks elsewhere. Let N=sum ell_i. The
+requested output is exactly m raw symbols at positions 0,...,m-1 on one fixed
+output tape, including blanks. It is not a blank-terminated integer codec.
+
+The RAM input is the house-standard length-prefixed list whose body is
+
+    [n, m, ell_0, tape_0..., ..., ell_(k-1), tape_(k-1)...].
+
+Here n>=0 is a scale parameter controlling packing. It is neither execution
+fuel nor a supplied time horizon. It may be tied to the input length by a
+particular caller; no such identification is needed for the simulation.
+The header length and all fields must be well formed. This program does not
+validate malformed payloads, discover their lengths or reject invalid symbols.
+
+RAM memory and registers share one bounded-word address space, initially zero.
+The operations are modular-word SET, ADD, monus SUB, Boolean AND/OR/NOT, shifts,
+indirect LOAD/STORE, branches, word READ/WRITE and terminal HALT. A shift by at
+least the word width yields zero. Successful instructions cost one. HALT costs
+no successful instruction. Code and the program counter are distinct from data.
+No TM step, packed access, multiplication or division is a primitive.
+
+Set c to 1 for A<=2 and 2 for 3<=A<=4. Thus c is the fixed symbol-field width.
+Define
+
+    lambda = floor(log2(n+2)),
+    q = floor(lambda/(8c)),
+    B = largest power of two <= q, or 1 if q=0,
+    b = log2(B), H = least power of two >=2k, R=128.
+
+The shipped emitter accepts 1<=k<=4, 1<=A<=4, 1<=Q<=16 and at most one million
+emitted instructions. The same argument applies to arbitrary fixed finite
+shapes with a base R above their controls and an adequate emitted-code bound.
+Only the stated implementation caps are claimed for the supplied code.
+
+Let T be a finite number of simulated transitions, L the emitted code length,
+and S=n+N+T+m+k+3. A sufficient word-width condition is
+
+    w >= max(10, bit_length(2R+H(S+1)), bit_length(L)).
+
+This is the conservative bound implemented by width_bound. It depends on a
+proved execution envelope, not information read by the emitted program.
+The helper accepts n<2^256 and lengths, T,m<=10^6; it is a bounded convenience
+interface, not part of the RAM's runtime. RAM replay accepts widths <=512.
+
+## Packing and initialization
+
+Encode signed heads by pi(z)=2z for z>=0 and pi(z)=-2z-1 for z<0. Decode
+u=pi(z)>>1 and tag=2i+(pi(z) AND 1). Then u=z on the nonnegative bank and
+u=-z-1 on the negative bank, including both 0 and -1 correctly. The symbol
+for tape i at z is the c-bit field at offset c(u mod B) in word
+
+    R + H floor(u/B) + tag.
+
+Equality of two natural word addresses forces equal block and equal tag,
+since the tag difference has absolute value below H. Different fields of one
+word have disjoint c-bit masks. This proves distinct tapes and signs cannot
+alias, and proves the shared-register/data separation since every data address
+is at least R and all controls are below 48.
+
+packing_init computes lambda by right-shifting n+2 until it is below two.
+It divides lambda by 8c by a fixed shift. It doubles B from one while the next
+double is at most q, recording b. Thus it computes precisely the stated B,
+including q=0 and q=1, with one fixed emitted program independent of n and w.
+
+If B=1 then cB=c<=w. Otherwise cB<=lambda/8<w. The width condition also fits
+n+2, the outer list length, head encodings, all masks and every effective tape
+address. In particular H>=2 bounds every head encoding by the available span.
+The trial double in the B loop is at most 2B and fits. Consequently all
+arithmetic used for addressing agrees with natural arithmetic; the modular
+word semantics does not wrap or truncate a live field.
+
+GET computes the address and offset in nine ordinary instructions, then
+loads, sets the field mask, shifts and masks in four more. SET shares the
+nine-instruction address calculation, then loads, sets the mask, shifts it,
+complements, masks out the old field, shifts the new symbol, ORs and stores.
+These are exactly 13 and 17 instructions. The Boolean mask identity proves
+SET changes only its selected field, preserving every neighboring field,
+unused high bit and other word.
+
+emit_input reads every length and every symbol and performs a SET at each
+successive nonnegative position. It increments encoded POS by two. All heads
+are explicitly set to zero. Induction on the input loops gives exactly the
+specified initial tapes, with uninitialized tape fields blank by the memory
+premise. Arbitrary unused high bits are also allowed. Arbitrary dirty fields
+that will later be read as blanks are not allowed by this ABI.
+
+## One transition and halt
+
+At label (state,q), the invariant is that the RAM has TM state q, every encoded
+head equals pi of its TM head, and every tape field has the corresponding TM
+symbol. Values of local scratch registers are immaterial; ONE, TWO, ZERO, b
+and B-1 retain their fixed meanings.
+
+The program first GETs every current head symbol into distinct retained
+symbol registers. No tape write occurs in this phase. Dispatch uses only the
+retained symbols and TEMP, trying each of the A^k possible tuples in a fixed
+order. Two strict comparisons implement equality for each symbol. For a
+well-formed alphabet, exactly the matching branch is reached.
+
+If that transition exists, all k literal writes are SET at the old head
+coordinates. Their order cannot change another tape's field. Each signed
+head is then updated. For an odd encoding, moving left adds two; moving
+right subtracts two except that encoding one becomes zero. For an even
+encoding, moving right adds two; moving left subtracts two except that zero
+becomes one. These are exactly pi(z+d) for d=-1 or 1. A stationary head is
+untouched. Jumping to the next state therefore reestablishes the invariant.
+This covers simultaneous writes and moves, crossing either side of zero,
+block boundaries and every finite sequence of transitions. Induction gives
+all-input simulation, rather than extrapolation from the finite fixtures.
+
+If the transition is missing, dispatch jumps to output. No tape or head is
+changed. The output loop GETs exactly m nonnegative fields of the chosen tape,
+starting at zero, and WRITEs each raw symbol. For m=0 no tape field is read.
+After those writes it reaches an actual terminal HALT instruction. Thus a
+halting TM produces the stated output and halts; a nonhalting TM returns to
+successive state boundaries indefinitely on an ideal unbounded-width model.
+At a fixed finite width the claim covers only prefixes satisfying the width
+condition. No finite width is asserted to simulate an unbounded trajectory.
+
+The output loop changes scratch, packing POS and the output counter only.
+All final tapes remain exactly the TM's final tapes. The program does not
+restore controls or erase its owned RAM storage. Such cleanup would require
+additional work in a caller with that stronger contract.
+
+## Complete successful-instruction envelope
+
+Initialization through packing setup costs exactly
+
+    16 + 4 lambda + 5b.
+
+Each tape's input-loop setup and final branch costs four instructions, and
+each initial symbol costs 26. The final jump into state zero costs one.
+Reading the simultaneous tuple costs 18k. Dispatch costs at most 3k A^k.
+Writing costs 22k, head motion costs at most 5k and the next-state jump costs
+one. The first missing-transition dispatch is bounded by the same quantity.
+The output loop costs 22m+2, including its initial POS assignment and final
+conditional branch. Therefore a halting run with T transitions executes at
+most
+
+    19 + 4 lambda + 5b + 4k + 26N
+       + (T+1)(45k + 3k A^k + 1) + 22m
+
+successful instructions. The same upper bound covers a prefix ending after
+T transitions. The verifier checks this envelope on every new-emitter case.
+For a fixed machine the cost is O(T+N+m+log(n+2)). This is constant overhead
+per TM transition, not a logarithmic simulation speedup.
+
+All nonnegative initialization/output coordinates and absolute head positions
+are below D=N+T+m+1. At most 2k ceil(D/B) tape words can consequently be touched,
+plus the fixed control bank. This counts words, not the numeric address span
+and not emitted code storage. For fixed c and sufficiently large caller scale,
+B=Theta(log(n+2)). A caller must supply a polynomial time/address envelope to
+obtain w=O(log(n+2)); choosing a large scale for a small fixture is not a time
+or bit-complexity improvement.
+
+## Evidence boundary and predecessor credit
+
+PR4538 by David Ganz / Dugongue supplies the representation, GET/SET kernels,
+unpacked compiler and explicitly open complete-backend question. The new step
+is the actual joined primitive program, invariant, raw-output contract and
+complete envelope above. The finite verifier uses a separately written signed
+TM model and twelve paired runs of the pinned source's unpacked compiler.
+Those pairs check the new program's conformance; they do not audit the source's
+scientific claims or replay its existing check suite. PR4883's retained-read
+access improvement is credited context and is not integrated here.
+
+Classical packing, finite-control compilation and simulation retain their
+classical status. The RamStd/Problem 1.8 and Szymon Torunczyk simulation lineage
+credited in PR4538 remains authoritative. PR4541's stronger tabulated transfer
+and PR4724's portfolio construction are separate operational-model results.
+No stronger asymptotic transfer or literature-priority claim is made.
+
+Finite replay does not prove the universal induction or certify RamStd.step
+in Lean. No physical multiplier, selected supplier, native operator, dirty
+helper restoration, rounding/recovery bound, framework-assumption discharge,
+new kappa or selected-frontier update follows from this result.

research/emitted-packed-tm/README.md

@@ -0,0 +1,151 @@
+# Complete emitted packed TM backend
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped simulation proof with exact finite corroboration.
+The package completes the emitted constant-overhead backend left open in
+David Ganz / Dugongue's [PR4538](https://github.com/CrocSwap/integer-mult-bounds/pull/4538).
+It joins packed input initialization, simultaneous observation, finite dispatch,
+signed head motion, fixed-window raw output and genuine halt into ordinary
+bounded-word RAM instructions. No host TM-step or access macro remains in the
+emitted program. Shared code and predecessor packages are unchanged.
+
+The new dense fixture initializes 256 tape cells in 128 packed data words.
+This is an exact storage count for that fixture, not a runtime benchmark.
+The all-input statement rests on the induction in [PROOF.md](PROOF.md).
+For k tapes, alphabet size A, N initial symbols, m output symbols and T steps,
+its complete successful-instruction upper bound is
+
+```text
+19 + 4 lambda + 5 log2(B) + 4k + 26N
+   + (T+1)(45k + 3k A^k + 1) + 22m.
+```
+
+Here lambda=floor(log2(n+2)), c is the fixed symbol-field width and B is the
+largest power of two at most floor(lambda/(8c)), with B=1 below that cutoff.
+The input includes the scale n; it is not execution fuel. At most
+2k ceil((N+T+m+1)/B) tape words are touched, plus the fixed control bank.
+The proof states the nonwrapping word-width condition and distinguishes
+that word footprint from the address span and emitted code.
+
+## Evidence and reproduction
+
+The new-emitter checks cover 294 cases: 277 halting runs, 17 nonhalting
+prefixes, 1,907 literal TM transitions and 419,591 successful RAM instructions.
+Every state boundary is compared with a separate signed-coordinate TM model,
+including the entire finite possibly affected tape interval. Packed block
+sizes 1,2,4,8,16, both zero crossings, multi-block excursions, four tapes,
+all supported alphabets, simultaneous cross-copy, nonzero output-tape choices,
+zero output and terminal halt are exercised. All fixtures retain arbitrary
+unused high bits and one exterior word.
+
+Twelve additional paired fixtures compare new-emitter outputs with the pinned
+unpacked compiler from PR4538. Its scientific tests and counts are not replayed
+or claimed as new coverage. Six actual emitted-code mutations are rejected,
+as are eight invalid machine specifications. The source bytes are authenticated
+before scientific execution. [SOURCES.json](SOURCES.json) pins those inputs and
+historical catalogue/selected-record provenance.
+
+Run from the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/emitted-packed-tm/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/emitted-packed-tm/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/emitted-packed-tm
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/emitted-packed-tm --check-source-history
+```
+
+Expected markers are PASS_EMITTED_PACKED_TM, PASS_REGISTERED_RESEARCH_PACKAGE
+and PASS_RESEARCH_COMMIT_BYTES. Another host's CPython 3.12 path can replace the
+shown interpreter. VERIFY.json registers both direct modes with 180-second
+limits. The direct verifier prints a generated JSON receipt bound to every
+package file's SHA256. Optional `--receipt /absolute/new/external/file.json`
+saves the same receipt and refuses to overwrite. Nothing is generated in the
+checkout. An official package export retains the three declared predecessor
+inputs at their repository paths for the paired comparison.
+
+## Interface and limits
+
+compiler.py exposes Machine, compile_machine and width_bound. The returned
+immutable instruction tuple is the actual finite program. ram.py executes only
+primitive instructions. The prototype reference interpreter is for this
+research certificate; it is not the installed RamStd.step formalization.
+
+The emitter accepts one through four tapes, alphabets of size one through four,
+one through sixteen states, and at most one million emitted instructions.
+Its input is a well-formed length-prefixed list of a scale, output extent,
+then each tape length and symbols. Tape fields begin blank; arbitrary dirty
+future blank fields require initialization. The output is exactly m raw
+symbols, including zeros. The program preserves its final simulated tapes but
+does not erase its control or tape storage. A surrounding cleanup or integer
+codec has its own costs. No arbitrary-bit codec, access fusion or tabulation is
+silently included.
+
+A particular caller must justify its scale, execution/address envelope, width,
+input presentation, output interpretation and any cleanup. No complete
+multiplication machine or selected supplier is materialized. Native costs,
+dirty-helper restoration, rounded arithmetic, stock, precision, analytic
+recovery and all five inherited framework assumptions remain open.
+No new kappa, selected-frontier change, unconditional multiplication theorem,
+Lean proof or independent human/proof-kernel acceptance is claimed.
+
+## Provenance and overlap
+
+The question source is PR4538, whose representation and unpacked compiler are
+credited. Classical packing and simulation methods are not new results here.
+Retain the RamStd/Problem 1.8 formalization and Szymon Torunczyk compositional
+simulation lineage credited there, together with its native, physical, precision,
+compiler and analytic predecessors. Nick Petalas's older PR4883 supplies a
+local retained-read access improvement, which this complete emitter does not
+yet integrate. Dugongue's PR4541 gives a stronger tabulated asymptotic transfer
+as an operational model; PR4724 gives a portfolio construction. Neither is
+replaced by this constant-overhead emitted backend.
+
+Canonical base is 2485805a6d47f36ea83ddde6327d453ac82d44dc, priority revision 8.
+Selected conditional kappa is .003125804. The selected source-binding first
+command passed; no predecessor scientific suite was run as the deliverable.
+The uniform-transfer-audit card explicitly changes to this model-transfer side
+result. [TASK.json](TASK.json) records the precise scope and next questions.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292016)
+was posted before implementation.
+
+Overlap checks covered live open PRs, 319 account PRs since October 23, active
+Discussions, recent handoffs, merged packed-backend terms and main README
+searches. The cached helper searched 97 of 8,722 main notes; arbitrary code
+diffs and unpublished work remain outside that coverage. No novelty conclusion
+rests on an absent search match.
+
+## Open next questions
+
+- Can PR4883's retained-read slabs survive the complete dispatcher's clobbers?
+  Start by retaining one cache per distinct tape and checking every live cell.
+  This could reduce access instructions; cache preservation is the blocker.
+- Can a materialized multiplication caller instantiate this backend's actual
+  scale, word width and IO contract? Start with its complete finite machine and
+  polynomial tape/time envelope. The absent full caller and separately charged
+  conversion/cleanup prevent an application claim here.
+
+## Verification bounds
+
+The verifier has no recursion and executes each fixture within the displayed
+instruction envelope, capped at ten million successful instructions. Generated
+programs are capped at one million instructions. Each new fixture has at most
+four tapes, 128 initialized symbols per tape and at most 80 simulated steps;
+the two-tape dense fixture has 128 symbols per tape. Alphabet products have at
+most 256 tuples, and the directed machines have at most sixteen states. All
+functions are below sixty physical lines. Explicit require checks remain
+enabled under -O. Warning-strict normal/optimized execution, source compilation
+and the package/publication checks provide the recurring diagnostics.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python tuples, integers,
+dictionaries and JSON allocate during compilation/replay. The fixed caps above,
+512-bit RAM words and one live compiled fixture bound this use; the verifier
+does not claim allocation-free operation. A fixed-array interpreter is the
+follow-up if that property becomes a caller requirement. Rule 8 has a narrow
+source-loading deviation: exactly the hash-authenticated PR4538 Python source
+is compiled into an isolated namespace for twelve paired fixtures. It runs no
+predecessor test entry point. Ordinary local imports and dataclass construction
+are the only other runtime registration. Rule 9 permits the two fixed source
+comparison targets compile_tm and VM in that namespace. No input selects an
+arbitrary callable. The emitted program itself uses only the enumerated direct
+RAM operations; it contains none of this host source loading.