diff --git a/research/pr4541-packed-transfer-check/.gitattributes b/research/pr4541-packed-transfer-check/.gitattributes new file mode 100644 index 0000000000..2189fda474 --- /dev/null +++ b/research/pr4541-packed-transfer-check/.gitattributes @@ -0,0 +1 @@ +PR4541-PROOF.md -text diff --git a/research/pr4541-packed-transfer-check/PR4541-PROOF.md b/research/pr4541-packed-transfer-check/PR4541-PROOF.md new file mode 100644 index 0000000000..43a6afbe1b --- /dev/null +++ b/research/pr4541-packed-transfer-check/PR4541-PROOF.md @@ -0,0 +1,112 @@ +# A complete packed-input simulation bound + +Prepared by Dugongue with substantial OpenAI Codex assistance and three parallel agents. Apache-2.0. This is an informal universal construction proof, supported by finite exact operational-model checks. It is not a Lean theorem or a complete emitted RamStd program. + +## Theorem and conventions + +Fix a deterministic finite-alphabet k-tape Turing machine M with Q states, blank 0 and finite transition table. k, Q and the alphabet are fixed before the input; they are not additional variable-size inputs. One transition reads all tapes, writes their new symbols and moves each head by -1, 0 or 1. A missing transition is genuine halt. Let the total binary input length be n, let the requested binary output cap be m, and suppose the actual execution halts after T transitions. Assume fixed constants a>=8, d>=1 give + + T+n+m+16 <= 2^(a-4) (n+2)^d. + +The machine receives packed binary input in power-of-two chunks as specified below. Its conventional TM input protocol uses two nonblank bit symbols distinct from blank, at fixed tape origins; its output is an MSB-first binary word at a fixed origin, terminated by blank or occupying the whole m-cell cap. A fixed alphabet relabeling and ordinary linear-time TM protocol conversion can arrange this standard interface. Such conversion time is part of T, not an uncharged oracle. + +There is a uniform finite-program Word RAM algorithm, fixed before n and independent of actual T and physical word width, with word width w >= C_M (floor(log2(n+2))+1), that produces exactly the same integer output in fixed-width packed LSB form. It uses only literal assignment, indirect LOAD/STORE, ADD, natural SUB, Boolean operations, shifts, branches and word input/output. It uses no multiplication/division instruction, supplied lookup table, advice string, randomization or unit-cost exact complex cell. Its total cost is + + O_M((T+n+m)/log(n+2) + (n+2)^(1/16) log(n+2)). (1) + +All constants and the fixed program may depend on M and the chosen envelope constants a,d; the M subscript below includes those fixed constants. Every address and intermediate value fits in a word. A nonhalting TM computation is not converted to a halt by an artificial epoch boundary: every finite prefix within the same numerical envelope is simulated faithfully. The halting theorem itself assumes the stated finite T. + +The RAM memory starts identically zero, as in the actual Problem 1.8 RamStd model used in PR #4538. All newly allocated table, tape, IO, descriptor and scratch arenas are disjoint. The numeric span of memory is polynomial in n; zero initialization of that model is not a clearing algorithm for arbitrary dirty storage. + +## 1. Uniform parameter choice and complete setup + +Let lambda=floor(log2(n+2)), ell=lambda+1. Choose c, a fixed power of two, large enough to encode the fixed alphabet, and c>=2 so blank and the two bit codes fit. Let K be the least power of two at least k and s=max(1,ceil(log2 Q)). Define + + q = floor(lambda/(64 K c)); + r = largest power of two <= max(1,q); + B = 4r; L = 2r+1. + +Because 64Kc is a power of two, q is obtained by a right shift; r is obtained by a doubling loop. lambda is computed by repeatedly right-shifting n+2. This costs O(log(n+2)) word operations. r is Theta_M(log(n+2)), with the small-input cutoff absorbed in machine-dependent constants; in particular r >= lambda/(128Kc) when lambda>=1. + +The local table has one row for every bit pattern consisting of a state field and k windows of L consecutive c-bit symbols. Its key size is + + b = s + kc(2r+1). + +For lambda >= max(64Kc,64s), we have r>=1, 64kcr<=lambda and 64s<=lambda. Since 2r+1<=3r, + + 16b <= 16s + 48kcr <= lambda. + +Thus all 2^b rows, including invalid/unreachable state or symbol patterns, number at most (n+2)^(1/16). The finitely many smaller inputs have a fixed table-size bound depending only on M. No universal statement about an arbitrary Q is inferred from the Q=3 parameter tests; the state-bit cutoff is explicit. + +For each row, place each local head at offset r in its window and simulate up to r literal M transitions, stopping at the first missing transition. Save the terminal state, a true-halt flag, elapsed transition count, all k updated windows, and the k final local head offsets. Missing transitions on invalid patterns may be defined as halt; valid runs never use invalid encodings. Dispatch over the fixed finite transition table costs a machine-dependent constant per local step. Construction therefore costs O_M(r 2^b) operations. Store each row in a fixed power-of-two stride of at least 2k+3 words, so its address is formed by a shift and an addition. Every entry is generated during the run from M and r; no table is supplied for free. + +The binary codec tables in PACKED-IO.md contain O(2^r+2^(cr)) rows and take O(r 2^(cr)) setup. Their exponent is smaller than b, so they fit the same startup bound. This pays setup for every input, without amortizing over an unspecified batch of inputs. + +## 2. Ordinary coordinates, packed words and address safety + +Use a fixed polynomial origin + + H = 2^(a+d*ell). + +This is computed by a shift whose exponent uses fixed-constant repeated addition. The program knows a,d as machine constants; it does not receive T or a time-horizon advice string. A signed TM coordinate z is represented at nonnegative position H+z. The envelope implies H is more than sufficient for every visited position and the margin r; no truncating subtraction of a left window origin changes its intended value. + +A tape word stores B fields. Take a fixed power-of-two interleaving stride J>=k. Tape i, block u, is stored at + + dataBase + J*u + i. + +The table base is a fixed machine-dependent power of two above every reserved register/scratch cell (at least 512 in the model); the data base lies above all table and reserved cells. This remains valid for large fixed k, rather than assuming a 512-cell prefix suffices for every machine. Dividing a position by B and reducing it modulo B are right shift and AND because B is a power of two. Different tapes and blocks have different addresses; all metadata, rows, IO buffers and descriptors have separate arenas. + +A window of L<=B consecutive cells spans at most two packed words. If its first word supplies a fields, read its suffix and, only if needed, the low L-a fields of the next word. Shift, OR and mask these fields into one word. To write it back, clear only the corresponding field masks and OR in the two fragments. The Boolean identities prove preservation of every neighboring field and every unused high bit, with arbitrary dirty values there. This is a constant-size additive/Boolean operation sequence per tape, even when a window crosses a packed block boundary. The implementation provides generalized bounded-length chunks for input/output as well. + +This ordinary-coordinate representation matters: a signed interval is not a contiguous bitstring under the unpacked compiler's zigzag mapping. No strided gather, negative-bank reversal or arbitrary bit permutation is assumed to cost one operation. + +To see a logarithmic width suffices globally, note that key bits are at most s+3kc+lambda/32 for all inputs, table row size is fixed, H has a+d*ell+1 bits, and every visited coordinate lies within the supplied polynomial envelope. Multiplying a block index by the fixed interleaving stride is a shift. Adding all IO/descriptor arenas and margins still has polynomial numeric span. A sufficiently large fixed C_M bounds all these exponents and literals. For example, uniform_parameters in tabulated_tm.py uses the conservative coefficient a+d+s+rowLog+strideLog+4kc+32 for its table/tape envelope; a caller includes its fixed IO arena constants in C_M. Word width also exceeds 4cr+1, so masks, reservoirs and all shifted fields fit. At every greater physical word width, the same intended operations and output are obtained. This is bounded-word computation, not an unbounded-register simulation. + +## 3. One macro step and genuine halt + +Maintain the invariant: the saved state is M's state, head i is H plus its signed TM position, and every represented tape field equals its TM symbol. Initially encoded input fields establish the invariant, and every uninitialized field is blank because RAM memory is zero. + +At a macro boundary, fetch all k windows centered on the current heads before performing any tape writes. Form their concatenated key with the current state and fetch the generated row in O_M(1) word operations. Apply every updated window at its old position and set + + newHead_i = oldHead_i + savedLocalHead_i - r. + +All subtractions are safe under the polynomial-origin bound. During r TM transitions a head moves at most r, so it never reads or writes outside the supplied 2r+1-cell window; the final move may reach an endpoint, still inside the window. The local table's literal transition simulation and the all-reads-before-writes discipline therefore preserve the full invariant, including distinct tapes at coincident coordinates. Applying a returned complete window also preserves every cell outside it. + +If a missing transition is seen before r successful transitions, the true-halt flag is set and elapsed counts only actual transitions. If the r-th transition reaches a halting configuration, the next macro detects that missing transition with elapsed zero. Thus at most floor(T/r)+1 macro calls are needed for a halting run. An epoch completing r transitions without a flag does not itself halt. This proves both exact halting semantics and O_M(T/r+1) simulation cost. + +The operational model records its displayed primitive operations, not exact fully emitted RamStd instruction counts. All source loops are over fixed k or the explicit bounded table/epoch counters. Fixed-size dispatch, register assignment and branch lowering alter only machine-dependent constants. No local table lookup is counted as a whole TM step oracle: the complete table construction is explicit and charged above. + +## 4. Packed external ABI, including partial chunks + +Let each operand arrive as exactly ceil(length/r) little-endian r-bit digit words, with unused high bits zero; the logical lengths are supplied as bounded headers. The physical list-length prefix is also paid and fits in a word. For w=Theta(log n), this is an ordinary constant-density packing of the binary input. The format is determined by n, not by the unknown physical w, so it works at all sufficiently large word widths. Input bit length n is the declared padded binary length, not the number of list entries or the numerical value of an all-zero operand. + +The codec explicitly tabulates expansion from binary r-bit chunks into c-bit codes 1/2, and decoding from c-bit chunks to binary values with prefix lengths and validity. It handles reversed chunk order for MSB input and reversed output descriptors for fixed LSB output. Read, store, reverse and masked-insert O(n/r) chunks. Separate operands may use separate tapes. If they share a tape, use one continuous reservoir across operands and delimiters; concatenating separately padded partial chunks would insert blank cells and is incorrect. A fixed binary length header costs only O(log n) cells and fits the startup allowance. + +The output decoder reads at most ceil(m/r) coded chunks, stops at the first blank or cap, reverses the retained descriptors, writes exactly ceil(m/r) LSB digit words, and pads only high bits with zeros. This preserves the numeric value even for leading zeros, zero itself and a short terminated prefix. A full-width output need not expose its following terminator. No bit-by-bit external IO pass costing Theta(n) is hidden here. The detailed reservoir and first-blank proofs are in PACKED-IO.md. + +Counting generated setup, simulation, input and output now gives + + O_M(r 2^b + log(n+2) + T/r + (n+m)/r + 1), + +which implies (1). The total buffer footprint and the polynomial numeric address envelope were included above. Arbitrary dirty reuse would require separately paid initialization; the theorem does not silently change the zero-initialized RamStd model. + +## Corollary: the supplied multiplication bound + +Suppose a fixed deterministic multitape machine multiplies two padded n-bit integers in + + T(n) = O(n (log n)^(1-kappa)), 0=n log n because its input scan costs n. We use the method as precedent and supply the packed-input/packed-output construction explicitly for the sub-n-log-n regime; that theorem's original hypothesis is not simply dropped. PR #4538 supplies this project's exact bounded-word machine and packed-field refinement precedents. The current proof and code do not claim to have invented tabulation or established worldwide priority for the corollary. + +Sources and inspected overlap are recorded in OVERLAP.md and OVERLAP-SOURCES.json. The finite implementations check the displayed model; an emitted complete RamStd program, formal compiler refinement, isolated Linux execution and a new TM paid-profile witness are separate future work. They are not assumed as hidden mathematical gadgets in the algorithm above. diff --git a/research/pr4541-packed-transfer-check/README.md b/research/pr4541-packed-transfer-check/README.md new file mode 100644 index 0000000000..d16b8b6ff1 --- /dev/null +++ b/research/pr4541-packed-transfer-check/README.md @@ -0,0 +1,61 @@ +# Independent check of #4541: packed Word RAM transfer, §1–§3 + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** + +Dugongue's #4541 (head `46ca24a8`) proves an informal bounded-word RAM bound `O((T+n+m)/log(n+2) + (n+2)^(1/16) log(n+2))` for a fixed TM. It uses generated tables of r-step local transitions over packed tape words. With a conditional TM multiplication bound, it gives `O(n/(log n)^κ)` RAM operations. This package checks the parameter arithmetic of §1 and the macro-step invariant and halting semantics of §§2–3. The verifier was written from #4541's `PROOF.md` text alone, vendored here as `PR4541-PROOF.md` with blob `43a6afbe` and its SHA256 pinned. Nothing is imported from #4541's code. + +## Results + +All checked claims are confirmed. + +**A. §1 parameters.** These are exact integer checks over 720,240 cases: `k ≤ 8`, `c ∈ {2, 4, 8}`, `s ≤ 10`, `0 ≤ λ ≤ 3000`. +- `16b ≤ λ` whenever `λ ≥ max(64Kc, 64s)`. So all `2^b` table rows number at most `(n+2)^(1/16)`, and setup `r·2^b` fits the startup term. +- `128Kc·r ≥ λ` for `λ ≥ 1`, so `r = Θ(log n)`. +- `L = 2r+1 ≤ B = 4r`, so a window spans at most two words. +- The codec exponent satisfies `cr < b`. + +The origin `H = 2^(a+dℓ)` satisfies `H ≥ 2^a (n+2)^d > 2·2^(a−4)(n+2)^d` for `a = 8`, `d ≤ 3` and all `n < 2^12` (12,288 cases). So every coordinate `H+z` with `|z| ≤ T+r` stays positive without truncating subtraction. + +**B. §§2–3 by an independent packed simulator.** The simulator follows the proof's description: +- `B = 4r` c-bit fields per word, with random dirty bits above the fields; +- tapes interleaved at `dataBase + J·u + i`; +- signed positions at origin H; +- `L`-cell windows read across at most two words, with all reads done before any write; +- a lazily generated local table of up to r literal steps, with invalid patterns treated as halt; +- the update `newHead = oldHead + localHead − r`. + +It ran 486 random k-tape machines (`k ≤ 3`, `Q ≤ 5`, alphabet ≤ 4, `r ∈ {1, 2, 4}`) against direct execution: + +| Case | Count | Compared against direct execution | +|------|------:|-----------------------------------| +| Halting runs | 263 | Exact state, transition count, heads and every tape cell | +| Nonhalting runs | 223 | Exact state, count and heads at every macro boundary | +| Halts found at an epoch boundary with elapsed zero (r > 1) | 46 | | +| Runs that visit negative coordinates | 323 | | +| Windows that cross a block boundary | 11,090 | | + +- **Dirty high bits.** These are preserved in every word. +- **Rejection control.** Writing windows back one cell off is caught in 19 of 20 runs. + +**C. Binding.** The verifier checks that the vendored `PROOF.md` states the formulas it tests verbatim (9 statements). + +I also replayed #4541's registered package at its head: `PASS_REGISTERED_RESEARCH_PACKAGE research/packed-ram-speedup outcome=partial` in 4.3 s. + +## Verify + +```text +python3 -B research/pr4541-packed-transfer-check/verify.py +``` + +This runs in about 2 s with the standard library only. + +## Limitations + +- **Not covered:** the packed IO codec (`PACKED-IO.md`, §4), the corollary's reliance on a TM multiplier with the stated envelope, and the RamStd lowering. The table here is generated lazily, for the keys actually used. #4541 generates every row and charges `r·2^b`; part A checks only that this charge fits. +- **Finite and random.** The simulator checks a finite random family. The universal statement rests on #4541's written argument, which these runs corroborate but do not replace. + +## Open next questions + +- An independent check of the packed IO codec of §4 (reservoir continuity across operands, first-blank output decoding and partial chunks). First step: a separate codec over random operand lists, compared against direct binary encoding. + +Credit: Dugongue (#4541), Hopcroft, Paul and Valiant (1975) for the classical method. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4541-packed-transfer-check/SOURCES.json b/research/pr4541-packed-transfer-check/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4541-packed-transfer-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/pr4541-packed-transfer-check/TASK.json b/research/pr4541-packed-transfer-check/TASK.json new file mode 100644 index 0000000000..a73ea3581b --- /dev/null +++ b/research/pr4541-packed-transfer-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent coverage of the RAM transfer that carries any TM κ (0.0023 selected; 0.003020165 pending) to the Word RAM model.", + "budget_minutes": 40, + "stop_rule": "Stop at §1-§3 of #4541; IO codec and corollary antecedents out of scope.", + "outcome": "completed", + "evidence": "720,240 exact parameter cases; 12,288 origin cases; independent packed simulator on 486 random machines matching direct execution (263 halting, 223 nonhalting prefixes, 46 epoch-boundary halts, 11,090 block-crossing windows); rejection control 19/20; 9 proof statements bound to vendored PROOF.md; #4541 package replays.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Independent check of #4541's packed IO codec (§4).", + "why_it_matters": "The O(n/log^κ n) corollary needs the packed ABI.", + "first_step": "Separate codec over random operand lists vs direct binary encoding.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4541-packed-transfer-check/VERIFY.json b/research/pr4541-packed-transfer-check/VERIFY.json new file mode 100644 index 0000000000..67422b5244 --- /dev/null +++ b/research/pr4541-packed-transfer-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact \u00a71 parameter inequalities (720,240 cases) and origin margin; independent packed simulator vs direct execution on 486 random TMs (halting, nonhalting prefixes, epoch-boundary halts, block crossings, dirty high bits); rejection control; binding to vendored #4541 PROOF.md (sha256)." + } + ] +} diff --git a/research/pr4541-packed-transfer-check/verify.py b/research/pr4541-packed-transfer-check/verify.py new file mode 100644 index 0000000000..6337ed6fb6 --- /dev/null +++ b/research/pr4541-packed-transfer-check/verify.py @@ -0,0 +1,304 @@ +#!/usr/bin/env python3 +"""Independent check of PR #4541 (Dugongue), packed Word RAM transfer: Section 1 parameters and Sections 2-3 macro steps. + +Written from #4541's PROOF.md text only (vendored as PR4541-PROOF.md); nothing is imported from its code. Checks: + A. Section 1 parameter arithmetic, exactly, over k<=8, c in {2,4,8}, s<=10, lambda<=3000: + 16b <= lambda above the cutoff lambda >= max(64Kc, 64s); 128Kc*r >= lambda; L <= B; codec exponent cr < b; + plus the Section 2 origin bound T+n+m+16 <= 2^(a-4)(n+2)^d => every coordinate H+z with |z| <= T+r lies in + (0, 2H), for a=8, d<=3 and all n < 2^12. + B. Sections 2-3 by an independent packed simulator: B=4r fields of c bits per word with dirty high bits above the + fields, tapes interleaved at dataBase+J*u+i, signed positions at origin H, windows of L=2r+1 cells read across at + most two words, all reads before writes, a generated (lazily memoised) local table of up to r literal steps with + invalid patterns treated as halt, and newHead = oldHead + localHead - r. Random k-tape machines are compared with + direct execution: halting runs on state, transition count, heads and every tape cell; nonhalting runs on every + macro-boundary prefix. Halts at an exact epoch boundary, block-crossing windows and negative coordinates are + counted. A rejection control (writing the window back one cell off) must be detected. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +PROOF = HERE / "PR4541-PROOF.md" # #4541 head 46ca24a8, research/packed-ram-speedup/PROOF.md, blob 43a6afbe +PROOF_SHA256 = "788535dea58df897055de81175acdea9abb149604ad9bdf7ee36b6100982d541" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def pow2_at_least(x): + p = 1 + while p < x: + p *= 2 + return p + + +def pow2_at_most(x): + p = 1 + while 2 * p <= x: + p *= 2 + return p + + +def params(k, c, s, lam): + K = pow2_at_least(k) + q = lam // (64 * K * c) + r = pow2_at_most(max(1, q)) + return K, r, 4 * r, 2 * r + 1, s + k * c * (2 * r + 1) + + +def check_parameters(): + rows = 0 + for k in range(1, 9): + for c in (2, 4, 8): + for s in range(1, 11): + for lam in range(0, 3001): + K, r, B, L, b = params(k, c, s, lam) + need(L <= B and c * r < b, "window fits two words; codec exponent below b") + if lam >= 1: + need(128 * K * c * r >= lam, "r >= lambda/(128Kc)") + if lam >= max(64 * K * c, 64 * s): + need(r >= 1 and 64 * k * c * r <= lam and 16 * b <= lam, "16b <= lambda") + rows += 1 + origins = 0 + for d in (1, 2, 3): + a = 8 + for n in range(0, 1 << 12): + ell = (n + 2).bit_length() # floor(log2(n+2)) + 1 + H = 1 << (a + d * ell) + envelope = (1 << (a - 4)) * (n + 2) ** d # T+n+m+16 <= envelope, so T and r are below it + need(H >= (1 << a) * (n + 2) ** d and 2 * envelope < H, "origin margin") + origins += 1 + return rows, origins + + +class Packed: + def __init__(self, k, c, r, H, rng): + self.k, self.c, self.r, self.H = k, c, r, H + self.B, self.L = 4 * r, 2 * r + 1 + self.lb = self.B.bit_length() - 1 + self.J = pow2_at_least(k) + self.base = 1 << 20 + self.fieldbits = c * self.B + self.mem = {} + self.junk = {} + self.rng = rng + self.crossings = 0 + + def word(self, addr): + if addr not in self.mem: + # Fields start blank (zero memory); high bits above the fields carry arbitrary dirty values. + self.junk[addr] = self.rng.getrandbits(13) << self.fieldbits + self.mem[addr] = self.junk[addr] + return self.mem[addr] + + def addr(self, tape, u): + return self.base + self.J * u + tape + + def read(self, tape, p0): + u, a0 = p0 >> self.lb, p0 & (self.B - 1) + avail = self.B - a0 + first = min(self.L, avail) + win = (self.word(self.addr(tape, u)) >> (self.c * a0)) & ((1 << (self.c * first)) - 1) + if self.L > avail: + self.crossings += 1 + rest = self.L - avail + win |= (self.word(self.addr(tape, u + 1)) & ((1 << (self.c * rest)) - 1)) << (self.c * avail) + return win + + def write(self, tape, p0, win): + u, a0 = p0 >> self.lb, p0 & (self.B - 1) + avail = self.B - a0 + first = min(self.L, avail) + m1 = ((1 << (self.c * first)) - 1) << (self.c * a0) + a = self.addr(tape, u) + self.mem[a] = (self.word(a) & ~m1) | ((win << (self.c * a0)) & m1) + if self.L > avail: + rest = self.L - avail + m2 = (1 << (self.c * rest)) - 1 + a2 = self.addr(tape, u + 1) + self.mem[a2] = (self.word(a2) & ~m2) | ((win >> (self.c * avail)) & m2) + + def cell(self, tape, p): + u, f = p >> self.lb, p & (self.B - 1) + return (self.word(self.addr(tape, u)) >> (self.c * f)) & ((1 << self.c) - 1) + + +def random_machine(rng, k, Q, sigma, p_missing): + delta = {} + + def all_syms(i): + if i == k: + yield () + return + for x in range(sigma): + for rest in all_syms(i + 1): + yield (x,) + rest + + for q in range(Q): + for syms in all_syms(0): + if rng.random() < p_missing: + continue + delta[(q, syms)] = (rng.randrange(Q), tuple(rng.randrange(sigma) for _ in range(k)), + tuple(rng.choice((-1, 0, 1)) for _ in range(k))) + return delta + + +def direct(delta, k, inputs, max_steps): + tapes = [dict(enumerate(inp)) for inp in inputs] + heads, state, steps = [0] * k, 0, 0 + while steps < max_steps: + key = (state, tuple(tapes[i].get(heads[i], 0) for i in range(k))) + if key not in delta: + return state, steps, heads, tapes, True + state, writes, moves = delta[key] + for i in range(k): + tapes[i][heads[i]] = writes[i] + heads[i] += moves[i] + steps += 1 + return state, steps, heads, tapes, False + + +def make_table(delta, k, c, r, s, Q, sigma): + L = 2 * r + 1 + table = {} + + def row(key): + if key in table: + return table[key] + state = key & ((1 << s) - 1) + wins = [[(key >> (s + i * c * L + c * j)) & ((1 << c) - 1) for j in range(L)] for i in range(k)] + local = [r] * k + elapsed, halted = 0, False + while elapsed < r: + syms = tuple(wins[i][local[i]] for i in range(k)) + if state >= Q or any(x >= sigma for x in syms) or (state, syms) not in delta: + halted = True + break + state, writes, moves = delta[(state, syms)] + for i in range(k): + wins[i][local[i]] = writes[i] + local[i] += moves[i] + need(0 <= local[i] < L, "head stays inside its window") + elapsed += 1 + packed = [sum(w[j] << (c * j) for j in range(L)) for w in wins] + table[key] = (state, halted, elapsed, packed, local) + return table[key] + + return row, table + + +def packed_run(delta, k, c, r, Q, sigma, inputs, max_macros, rng, skew=0): + s = max(1, (Q - 1).bit_length()) + H = 1 << 16 + pk = Packed(k, c, r, H, rng) + for i, inp in enumerate(inputs): + for z, x in enumerate(inp): + p = H + z + u, f = p >> pk.lb, p & (pk.B - 1) + a = pk.addr(i, u) + pk.mem[a] = pk.word(a) | (x << (c * f)) + row, table = make_table(delta, k, c, r, s, Q, sigma) + heads, state, steps = [H] * k, 0, 0 + prefixes = [] + for _ in range(max_macros): + wins = [pk.read(i, heads[i] - r) for i in range(k)] # every read before any write + key = state | sum(wins[i] << (s + i * c * pk.L) for i in range(k)) + state, halted, elapsed, out, local = row(key) + for i in range(k): + pk.write(i, heads[i] - r + skew, out[i]) + heads[i] = heads[i] + local[i] - r + steps += elapsed + prefixes.append((state, steps, [h - H for h in heads])) + if halted: + return pk, state, steps, heads, True, prefixes, len(table) + return pk, state, steps, heads, False, prefixes, len(table) + + +def compare(delta, k, c, r, Q, sigma, inputs, rng, skew=0): + max_macros = 40 + pk, state, steps, heads, halted, prefixes, rows = packed_run(delta, k, c, r, Q, sigma, inputs, max_macros, rng, skew) + ref = direct(delta, k, inputs, max_macros * r + 1) + if halted: + need(ref[4] and ref[0] == state and ref[1] == steps, "halting state and transition count") + need([h - pk.H for h in heads] == ref[2], "halting heads") + else: + need(not ref[4] or ref[1] > (max_macros - 1) * r, "nonhalting prefix") + # Prefix fidelity at every macro boundary: rerun directly to each boundary. + for j, (st, sp, hd) in enumerate(prefixes): + d = direct(delta, k, inputs, sp) + need(d[0] == st and d[1] == sp and d[2] == hd, "macro-boundary prefix") + cells = set() + for i in range(k): + cells |= {(i, z) for z in ref[3][i]} + visited_lo = min([z for _, z in cells] + [h - pk.H for h in heads] + [0]) + lo = visited_lo - 2 * r + hi = max([z for _, z in cells] + [h - pk.H for h in heads] + [0]) + 2 * r + if halted: + for i in range(k): + for z in range(lo, hi + 1): + need(pk.cell(i, pk.H + z) == ref[3][i].get(z, 0), "every tape cell") + for a, v in pk.mem.items(): + need(v >> pk.fieldbits == pk.junk[a] >> pk.fieldbits, "dirty high bits preserved") + boundary_halt = halted and steps > 0 and len(prefixes) >= 2 and prefixes[-1][1] == prefixes[-2][1] + return halted, boundary_halt, visited_lo < 0, pk.crossings, rows + + +def check_simulator(): + rng = random.Random(4541) + stats = {"runs": 0, "halting": 0, "nonhalting": 0, "epoch_boundary_halts": 0, "negative_coordinates": 0, + "block_crossing_windows": 0, "table_rows_generated": 0} + configs = [(k, Q, sigma, r) for k in (1, 2, 3) for Q in (2, 3, 5) for sigma in (2, 3, 4) for r in (1, 2, 4)] + for k, Q, sigma, r in configs: + for trial in range(6): + delta = random_machine(rng, k, Q, sigma, rng.choice((0.02, 0.08, 0.25))) + inputs = [[rng.randrange(1, sigma) for _ in range(rng.randrange(0, 9))] for _ in range(k)] + halted, boundary_halt, neg, crossings, rows = compare(delta, k, 2, r, Q, sigma, inputs, rng) + stats["runs"] += 1 + stats["halting" if halted else "nonhalting"] += 1 + stats["epoch_boundary_halts"] += int(boundary_halt and r > 1) + stats["negative_coordinates"] += int(neg) + stats["block_crossing_windows"] += crossings + stats["table_rows_generated"] += rows + need(min(stats["halting"], stats["nonhalting"], stats["epoch_boundary_halts"], stats["negative_coordinates"], + stats["block_crossing_windows"]) > 0, "every edge case occurs") + # Rejection control: writing each returned window one cell to the right must be caught. + caught = 0 + for trial in range(20): + delta = random_machine(rng, 2, 3, 3, 0.05) + inputs = [[rng.randrange(1, 3) for _ in range(6)] for _ in range(2)] + try: + compare(delta, 2, 2, 2, 3, 3, inputs, rng, skew=1) + except AssertionError: + caught += 1 + need(caught >= 15, "rejection control detected") + stats["rejection_control_caught"] = caught + return stats + + +def check_binding(): + raw = PROOF.read_bytes() + need(hashlib.sha256(raw).hexdigest() == PROOF_SHA256, "vendored #4541 PROOF.md bytes") + text = raw.decode("utf-8") + for line in ("q = floor(lambda/(64 K c));", "B = 4r; L = 2r+1.", "b = s + kc(2r+1).", "16b <= 16s + 48kcr <= lambda.", + "H = 2^(a+d*ell).", "dataBase + J*u + i.", "newHead_i = oldHead_i + savedLocalHead_i - r.", + "T+n+m+16 <= 2^(a-4) (n+2)^d.", "r >= lambda/(128Kc) when lambda>=1"): + need(line in text, f"#4541 states: {line}") + return 9 + + +def main(): + rows, origins = check_parameters() + report = {"status": "PASS_PR4541_PACKED_TRANSFER_CHECK", "parameter_cases": rows, "origin_cases": origins, + "proof_statements_bound": check_binding(), + "simulator": check_simulator(), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())