From 5c5b01e419c6737811cf94391a202586fe16c4b3 Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Mon, 19 Oct 2026 01:43:16 +0000 Subject: [PATCH] Implement framed XOR endpoint corrections on two tapes --- research/xor-endpoint-tapes/INPUTS.json | 8 + .../xor-endpoint-tapes/LIBRARY-BRIDGES.json | 54 +++ .../xor-endpoint-tapes/LIBRARY-BRIDGES.md | 29 ++ research/xor-endpoint-tapes/NOTICE.md | 51 +++ research/xor-endpoint-tapes/PROOF.md | 281 +++++++++++++++ research/xor-endpoint-tapes/README.md | 112 ++++++ research/xor-endpoint-tapes/RESULT.json | 319 ++++++++++++++++++ research/xor-endpoint-tapes/SOURCES.json | 63 ++++ research/xor-endpoint-tapes/TASK.json | 80 +++++ research/xor-endpoint-tapes/VERIFY.json | 37 ++ .../xor-endpoint-tapes/inputs/PR2297-PROOF.md | 41 +++ .../inputs/PR3480-README.md | 43 +++ .../inputs/PR3480-verify.py | 149 ++++++++ research/xor-endpoint-tapes/machine.py | 212 ++++++++++++ research/xor-endpoint-tapes/test_machine.py | 119 +++++++ research/xor-endpoint-tapes/verify.py | 173 ++++++++++ 16 files changed, 1771 insertions(+) create mode 100644 research/xor-endpoint-tapes/INPUTS.json create mode 100644 research/xor-endpoint-tapes/LIBRARY-BRIDGES.json create mode 100644 research/xor-endpoint-tapes/LIBRARY-BRIDGES.md create mode 100644 research/xor-endpoint-tapes/NOTICE.md create mode 100644 research/xor-endpoint-tapes/PROOF.md create mode 100644 research/xor-endpoint-tapes/README.md create mode 100644 research/xor-endpoint-tapes/RESULT.json create mode 100644 research/xor-endpoint-tapes/SOURCES.json create mode 100644 research/xor-endpoint-tapes/TASK.json create mode 100644 research/xor-endpoint-tapes/VERIFY.json create mode 100644 research/xor-endpoint-tapes/inputs/PR2297-PROOF.md create mode 100644 research/xor-endpoint-tapes/inputs/PR3480-README.md create mode 100644 research/xor-endpoint-tapes/inputs/PR3480-verify.py create mode 100644 research/xor-endpoint-tapes/machine.py create mode 100644 research/xor-endpoint-tapes/test_machine.py create mode 100644 research/xor-endpoint-tapes/verify.py diff --git a/research/xor-endpoint-tapes/INPUTS.json b/research/xor-endpoint-tapes/INPUTS.json new file mode 100644 index 0000000000..5f5540effb --- /dev/null +++ b/research/xor-endpoint-tapes/INPUTS.json @@ -0,0 +1,8 @@ +{ + "schema_version": 1, + "sha256": { + "inputs/PR3480-verify.py": "4ce24c8e835b1defae20fa8a2630c44536523ba08bce6226ab39c1045754de6b", + "inputs/PR3480-README.md": "d537f1342e8de682826e98e7a1ec9bb30f9d4152d3d7ba270443eb91877f2c9f", + "inputs/PR2297-PROOF.md": "9020e4b7ea5c5bd6e49148f940a81c5c95e8f91ce870389a2f73cac4ff276696" + } +} diff --git a/research/xor-endpoint-tapes/LIBRARY-BRIDGES.json b/research/xor-endpoint-tapes/LIBRARY-BRIDGES.json new file mode 100644 index 0000000000..e57716f7f7 --- /dev/null +++ b/research/xor-endpoint-tapes/LIBRARY-BRIDGES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "sources": [ + { + "module_path": "Mathproof/External/IntegerMultBounds20261008/Matrix/CommutingPhases.lean", + "sha256": "95d64270a9973e00b75d2b1f8a29ed95d15f0c3013e604f2ef14249a2a7c9d48", + "declarations": [ + "translate", + "xor_translation_commutes", + "raw_phase_translation_commutes", + "gauge_phase_noncommuting_witness" + ], + "evidence": "Inspected canonical source and direct mathematical adaptation; no new Lean compile, typed-port composition or kernel audit." + }, + { + "module_path": "Mathproof/Computability/MultitapeLocality20261014.lean", + "sha256": "4e5df1bdd9764d335424acb2a3aad8364f647892e632d8b09aec85e45cfb5b31", + "declarations": [ + "act_preserves_unscanned", + "step_locality", + "moveOffset_unit" + ], + "evidence": "Inspected canonical source and direct mathematical adaptation; no new Lean compile, typed-port composition or kernel audit." + }, + { + "module_path": "Mathproof/Computability/MultitapeFrameRule20261014.lean", + "sha256": "e5aa9ec056340c67bc6e382eee0a859e6903d9944d3a0e021f2a24a12459cb66", + "declarations": [ + "FootprintedRuns.frame", + "FootprintedRuns.compose" + ], + "evidence": "Inspected canonical source and direct mathematical adaptation; no new Lean compile, typed-port composition or kernel audit." + } + ], + "search_coverage": "Four source-catalog queries capped at 12 hits each; two DAG name lookups capped at 3 hits each. Not exhaustive.", + "dag_results": [ + { + "query": "xor_translation_commutes", + "results": [] + }, + { + "query": "FootprintedRuns.frame", + "results": [ + { + "id": "source:7977930", + "snapshot": "source-catalog", + "name": "Mathproof.Multitape.Absolute.FrameRule.FootprintedRuns.frame", + "type_node": null, + "axioms": null + } + ] + } + ] +} diff --git a/research/xor-endpoint-tapes/LIBRARY-BRIDGES.md b/research/xor-endpoint-tapes/LIBRARY-BRIDGES.md new file mode 100644 index 0000000000..9f5e63cd88 --- /dev/null +++ b/research/xor-endpoint-tapes/LIBRARY-BRIDGES.md @@ -0,0 +1,29 @@ +# Linked-library and predecessor bridges + +The shared source catalogue and authoritative DAG were queried with bounded +packets. Retrieval is not a fresh kernel check or an exhaustive novelty +search. Exact inspected source hashes and declaration names are stored in +LIBRARY-BRIDGES.json; no absolute local user path is needed by the package. + +| Inspected source | Reused concept and exact limit | +|---|---| +| `Mathproof.External.IntegerMultBounds20261008.Matrix.CommutingPhases` | `translate`, `xor_translation_commutes` and `raw_phase_translation_commutes` supply the exact XOR operator/commutation precedent. The new proof specializes to bounded h-bit records and implements the resulting permutation on tapes. | +| Same module, `gauge_phase_noncommuting_witness` | Prevents assuming a deferred translation passes every native gauge. The new correction is applied at an explicit endpoint and does not use free global relabeling. | +| `Mathproof.Computability.MultitapeLocality20261014` | `act_preserves_unscanned`, `step_locality` and `moveOffset_unit` guide the literal observation/write/unit-move semantics. The new tables are proved directly; they are not represented as Lean-compiled runs. | +| `Mathproof.Computability.MultitapeFrameRule20261014` | `FootprintedRuns.frame` and `FootprintedRuns.compose` guide exact window preservation and additive subroutine composition. The explicit template scans give the new footprint and restored head endpoints. No existing Lean footprint is silently reused for a new machine. | +| PR2297, Cinna Davis | Defines `C_q=((1+i)I+(1-i)X_q)/2` and the five-plane local correction. The generic C_E² identity is written out in PROOF.md and checked on small exact complex streams. No full cover search or 16-term decoder is rerun. | +| PR3480, Gonzalo Mier | Supplies the conditional shared-register cancellation handoff and the source-pinned 23 masks. Here each is corrected separately; summing isolated tape bills does not establish native owner placement. | +| `research/high-route-permutation-frames/` | Tekalign's existing paid permutation-frame scheduling prevents a first-use claim for carrying permutations. The new standalone XOR record machines use an explicit different ABI and full bit-tape invoice. | +| Coordinate-CNOT spectator and integer-address signed-SWAP packages | Their native-alphabet prices are not prices for the present literal tape scans. This comparison prevents treating an address map as free or conflating binary payload operations with address operations. | + +The bounded source packet used 4 queries with at most 12 hits per query. +The directly relevant translation hit was inspected in the canonical source. +Queries with no hits do not exclude related declarations under other names. +Historical/source-catalog DAG entries remain labelled as such; no new typed +port, compatible combined import environment or kernel/transitive-axiom +certificate is claimed for the informal machine proof. + +The concrete sufficient result consists of the finite transition construction, +exact travel formulas, dirty-scratch restoration, norm-preserving endpoint +composition and source-bound bills. XOR permutation, three-swap restoration +and sequential tape compilation themselves are established techniques. diff --git a/research/xor-endpoint-tapes/NOTICE.md b/research/xor-endpoint-tapes/NOTICE.md new file mode 100644 index 0000000000..28cb9b6554 --- /dev/null +++ b/research/xor-endpoint-tapes/NOTICE.md @@ -0,0 +1,51 @@ +# Attribution + +New finite transition compiler, exact movement formulas, dirty-record +correction primitive, proof/application and checks: Dugongue, with substantial +OpenAI Codex assistance. Apache-2.0. No independent human or new kernel +verification is claimed. + +The three documents in inputs/ are unmodified public sources. Gonzalo Mier's +PR3480 at `8e6fcaa557d2bff56c914f167e19929b0b656e1f` supplies the immediate +shared-register correction question and the explicit 23-mask list. Its +README and verifier retain the existing OpenAI Codex disclosure. The +verifier is treated as source data and never imported or executed here. +Cinna Davis (1337isnot1337)'s PR2297 proof at +`49f9c1a08bf1fe67a62bd6d2825aa0d03e1b1518` supplies the five-plane endpoint +definition and local algebra. Its OpenAI disclosure and nested credit remain. + +The five-plane lineage credits Philippe Van Velzen/Discussion1587, paired +planes PR1825, Discussion2024/PR2041 and tetrad-local PR1909. Sagar Thakrar's +PR3876 at `d359cf4d3e2fc46e989979dcb2be351cbab97451` closes a separate scalar +decoder contract, building on Arham Tahir/PR2879, Philippe Van Velzen, +Sagar Thakrar/PR2532, Cinna Davis, Adam Gall/PR1889, Tekalign/PR2782, +the C5 principal-rank work and other retained contributors. We use that +scope distinction, not its certificate as a computational input or a +claimed impossibility of this operator-valued tape primitive. + +The merged `research/high-route-permutation-frames/` package, by Tekalign +(tekuuu) with OpenAI Codex assistance, already carries field permutations +through later BIT route factors with a paid restoration guard. It credits +Jose Manuel/PR2915/2899, David Arias/PR2753, Nick Petalas, commdata2338/PR3233, +Sagar Thakrar/PR3265, Krzysztof Wójt/PR3301, Arham Tahir, ywz65, PR2157/589/555 +and the native geometry/compiler lineage. That work is a different actual +route compiler and its savings are not attributed to this package. + +Gareth Davidson's coordinate-CNOT spectator certificate and ywz65's +integer-address signed-SWAP theorem use explicit paid native alphabets; +their address operations are not free operations in our tape bill. +Their inherited PR1414/1333, PR2544, Aaron Wang/PR2444 and Ross Richardson +PR1989/2415 credit remains with those packages. They are compared for scope, +not imported as implementation dependencies. + +The linked MathProof `CommutingPhases`, `MultitapeFrameRule` and +`MultitapeLocality` sources provide translation/phase and exact-frame +precedents. Their source hashes and declaration references are recorded in +LIBRARY-BRIDGES.json. No source-only/historical index hit is represented as +a new kernel check, and no assertion of first use of XOR permutations, +three-swap scratch restoration or finite tape compilation is made. + +The retained Harvey–van der Hoeven, OpenAI manuscript, Douglas Colkitt, +RaD/hipotures and other upstream/community notices are not replaced. +No frozen supplier, selected certificate, upstream source or other +contributor's file is changed. diff --git a/research/xor-endpoint-tapes/PROOF.md b/research/xor-endpoint-tapes/PROOF.md new file mode 100644 index 0000000000..e46aefdb54 --- /dev/null +++ b/research/xor-endpoint-tapes/PROOF.md @@ -0,0 +1,281 @@ +# Exact framed XOR endpoint corrections on two tapes + +Prepared by Dugongue with substantial OpenAI Codex assistance. Apache-2.0. +This is an informal proof of explicit finite-alphabet machine families. +The new construction has not received a Lean kernel audit or independent +human review. Exact finite transition replays corroborate it. + +## 1. Statement, representation and cost convention + +Let h ≥ 0, N = 2^h, and 0 ≤ δ < N. For a record vector w define + + (X_δ w)_j = w_(j xor δ), 0 ≤ j < N. + +Use two tapes, each with alphabet {0, 1, #, blank}. A framed record vector is + + # w_0 # w_1 # ... # w_(N−1) #, + +where every w_j is a finite binary word. Both heads begin at the first #. +Origins may be any integers on their respective tapes. Tape locations outside +the declared windows contain arbitrary symbols. No blank infinite exterior +or clean full output buffer is assumed. + +One transition observes both scanned symbols, writes at most one symbol on +each tape and moves each head by −1, 0 or +1. A designated halt state has no +outgoing transition. This is the ordinary synchronous multitape-step +convention. It is not the repository's separate read/write/move event count: +at most six such elementary events occur per transition (two reads, two +writes, two moves). Thus 6T is a conservative event-count conversion. + +**Theorem A (borrowed-input copy).** For every h and δ the supplied compiler +produces a finite two-tape machine that, for every framed vector of N equal +width-B words, returns X_δ w in natural record order on the second tape, +preserves the complete input tape, restores both heads, and changes no output +cell outside its declared window. Interior output dirt may be overwritten. +Its exact transition count is + + T_copy = 2NB + 4N + (B+2)Q_h(δ), + Q_h(δ) = V_h(δ) + 1 + 2 rev_h(δ), + V_h(δ) = ∑_(j=0)^(N−2) |((j+1) xor δ) − (j xor δ)|, + +where rev_h reverses the h mask bits. In particular, + + Q_h(δ) ≤ (h+1)N, + T_copy ≤ N((h+3)B + 2h + 6). + +The online machine uses no counters, address arithmetic or recursive Fourier +oracle. Its generated control has exactly 2(2N+Q_h)+1 states, including halt, +and 16(2N+Q_h) defined transitions. Compilation and stored control are finite +and charged, not free uniformity assumptions. The same machine also permutes +variable-length records, with the exact weighted invoice in section 3. + +**Theorem B (in-place correction with restored dirty scratch).** For δ ≠ 0, +the second compiler produces a two-tape machine that transforms the first +framed, equal-width vector in place to X_δ w. It restores an arbitrary dirty +B-bit scratch record on the second tape, restores both heads, and preserves +both exteriors. If k is the highest set-bit index of δ, put + + H_h(δ) = (N−2)2^k + 2N − 2. + +Its exact transition count is + + T_inplace = (3N/2)(2B+3) + (B+2)H_h(δ). + +For δ = 0 the compiler returns a genuinely halted identity machine with zero +transitions. The in-place construction needs only B+2 scratch cells, including +two separators, but its time may be quadratic in N. The copy construction uses +N(B+1)+1 output cells and has the smaller O(NB(h+1)+N(h+1)) bound. These are +different time/space contracts; neither cost is silently substituted for the +other. B = 0 is admitted by both constructions. + +The machine is fixed once h and δ are fixed and works for every B and every +payload. There is a uniform explicit finite compiler for all h, δ. We do not +claim a single fixed-control online machine accepting unbounded h as data at +the displayed cost. In the P112 application h = 9 is fixed. + +## 2. Explicit transition templates + +The control program is a finite sequence of the following macros. Each macro +has its own entry/scan states and a fixed successor state. Every template is +expanded over the four-symbol alphabet in `machine.py`; there is no hidden +random-access operation in `run`. + +R0 starts with tape 0 at a separator. It moves that head right once, scans +binary payload symbols right until the next #, and takes one stationary +transition to its fixed successor. Tape 1 does not move or change. For a +crossed word of length b it costs b+2 transitions. L0 is the left version. +L1 moves left through one record on tape 1 while leaving tape 0 alone, with +the same b+2 count. These macros may read a symbol on the other tape but their +actions are independent of it. They write no tape cells. + +C starts with tape 0 at the separator before the desired input word and tape +1 at the separator position for the next output word. It writes # on tape 1 +and moves both heads right. For each input bit it writes that same bit to +tape 1 and moves both heads right. On the closing input # it writes # on +tape 1, stays put and enters its fixed successor. Its count is b+2; the input +head now lies at the following separator, not at the copied word's start. + +These two-state macros each have 16 defined transitions across entry and +scan states. All input writes are absent. Invalid symbols or missing +separators can block; the theorem's precondition is a well-formed framed +input. Verification uses explicit transition limits for malformed controls. + +For in-place work, W swaps one equal-width record on each tape. It moves +both heads right from #, swaps the two scanned bits in each transition and +moves right, then moves both heads left on the closing pair of #. A rewind +state scans the two binary words left to their opening separators and takes +one stationary transition to the successor. The count is 2B+3. Both heads +return to their entry separators. W has three states and 11 defined +transitions. Equal word width is required: mismatched closing separators +block. W never changes a separator or any exterior cell. + +The interpreter makes exactly one finite table lookup, bounded-symbol write +and unit move per transition. Its host dictionaries represent tape storage; +they do not supply address jumps to the simulated machine. All arithmetic +that selects the visit order occurs in the finite program generator. + +## 3. Borrowed-input permutation and exact travel + +Let f(j) = j xor δ. Before output record j, issue enough R0 or L0 macros to +move the input head from its current record separator to separator f(j), +then issue C. The input head is now at separator f(j)+1. After all N copies, +return it to separator 0 with L0 macros and return the output head with N +L1 macros. Every source and output separator lies in the declared finite +windows; the C macro may visit the final closing separator but never passes it. + +XOR with δ is a permutation of {0,...,N−1}. Thus every input word is copied +exactly once and the concatenated output is exactly X_δ w. The source is +never written. Every output cell from the initial to final separator is +written, and no other output cell is written. The explicit return scans +restore both heads. This proves the functional and frame statements. + +The number of input record crossings outside C is + + Q = f(0) + ∑_(j=0)^(N−2) |f(j+1)−f(j)−1| + f(N−1)+1 + = N + ∑ |Δ_j−1|, + +since f(0)=δ and f(N−1)=N−1−δ. Every Δ_j is a nonzero integer, so +|Δ_j−1| = |Δ_j| − sign(Δ_j). If incrementing j flips bits 0 through r, +the sign of Δ_j is positive exactly when mask bit δ_r is zero. This carry +case occurs N/2^(r+1) times. Hence + + ∑ sign(Δ_j) = ∑_(r=0)^(h−1) (1−2δ_r)2^(h−1−r) + = N−1 − 2 rev_h(δ), + +and Q = V_h + 1 + 2 rev_h(δ). This also holds for h=0: Q=1, because the +single C leaves the input head at its closing separator before return. + +There is an independent recurrence for V. Let d be the low h−1 bits of δ. +Then V_0(0)=0 and + + V_h(δ) = 2V_(h−1)(d) + J, + J = 1+2d if the top mask bit is zero, + J = 2^h−1−2d if the top mask bit is one. + +The two halves have identical variation and J is their boundary jump. +Since J ≤ N−1, induction gives V_h ≤ (h−1)N+1, including h=0. Therefore +Q ≤ (h+1)N. Copy and output-return scans cost NB+2N each; input seeks cost +(B+2)Q. This proves the exact and upper-bound times in Theorem A. + +For variable lengths b_i, let c_i be the number of input-seek crossings of +the edge between separators i and i+1, including the final return. Then + + T_copy = 2∑ b_i + 4N + ∑ c_i(b_i+2), ∑ c_i = Q. + +`exact_cost` computes these edge counts independently of the transition +table. Equal-width cost is consequently independent of payload values. + +## 4. In-place swaps and dirty-scratch restoration + +For δ ≠ 0, f is an involution without fixed points. Enumerate the N/2 pairs +(a,b) in increasing a, where b=a xor δ and a None: + if not ok: + raise ValueError(message) + + +def load_predecessor_core(): + spec = importlib.util.spec_from_file_location("five_plane_core", PREDECESSOR / "core.py") + need(spec is not None and spec.loader is not None, "cannot load predecessor core") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def apply_c(state: dict[int, tuple[int, int]], q: int) -> dict[int, tuple[int, int]]: + """Apply the unnormalised Gaussian-dyadic lift C_q used by the predecessor.""" + out: dict[int, tuple[int, int]] = {} + + def add(index: int, real: int, imag: int) -> None: + old_real, old_imag = out.get(index, (0, 0)) + out[index] = (old_real + real, old_imag + imag) + + for index, (real, imag) in state.items(): + add(index, real - imag, real + imag) + add(index ^ q, real + imag, imag - real) + return {index: value for index, value in out.items() if value != (0, 0)} + + +def xor_group(labels: list[int], group: list[int]) -> int: + shift = 0 + for port in group: + shift ^= labels[port] + return shift + + +def verify_partition(candidate: dict) -> list[list[int]]: + groups = candidate["groups"] + residual = candidate["residual"] + blocks = candidate["blocks"] + need(blocks == groups + [residual], "block order differs from the cover") + need(len(groups) == 22 and all(len(g) == 5 for g in groups), "expected 22 five-frames") + need(len(residual) == 2, "expected one residual pair") + flat = [port for group in blocks for port in group] + need(sorted(flat) == list(range(112)), "blocks do not partition P112") + return blocks + + +def main() -> None: + # Direct runs enforce the package's live source pins too. + source_manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in source_manifest["files"]: + if row["usage"] == "input": + path = ROOT / row["path"] + need(path.is_file(), "missing input: " + row["path"]) + need(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], + "input hash mismatch: " + row["path"]) + + core = load_predecessor_core() + labels, _ = core.load_sources() + record = json.loads((PREDECESSOR / "CANDIDATE.json").read_text()) + candidate = record["candidate"] + blocks = verify_partition(candidate) + need(len(labels) == 112, "wrong selected label count") + + block_deltas = [xor_group(labels, group) for group in blocks] + all_labels_xor = 0 + for label in labels: + all_labels_xor ^= label + all_deltas_xor = 0 + for delta in block_deltas: + all_deltas_xor ^= delta + need(all_labels_xor == 0, "selected P112 labels no longer have zero xor") + need(all_deltas_xor == all_labels_xor, "partitioned correction xor differs from label xor") + need(core.rank_rows(block_deltas, core.DIM) == 9, "expected full-rank block correction set") + expected_deltas = [98, 70, 100, 274, 50, 506, 247, 352, 304, 56, 19, 274, + 22, 445, 152, 388, 268, 254, 463, 508, 322, 475, 235] + need(block_deltas == expected_deltas, "per-block endpoint translations changed") + + # Each local C_E^2 translation is checked on every basis address (512 states). + local_cases = 0 + for group, delta in zip(blocks, block_deltas): + for start in range(1 << core.DIM): + state = {start: (1, 0)} + for port in group + group: + state = apply_c(state, labels[port]) + expected = {start ^ delta: (1 << (2 * len(group)), 0)} + need(state == expected, "local C_E^2 endpoint identity failed") + local_cases += 1 + need(local_cases == 23 * (1 << core.DIM), "wrong local endpoint case count") + + # If these corrections share one address register, their product is one + # translation by xor(block_deltas), hence identity on every address state. + for start in range(1 << core.DIM): + destination = start + for delta in block_deltas: + destination ^= delta + need(destination == start, "deferred global endpoint correction is nonidentity") + + hist = {int(rank): int(count) for rank, count in candidate["copy_rank_histogram"].items()} + profile, centre = core.profile_for(hist) + fused_screen = core.moment_screen(profile, centre) + need(fused_screen == candidate["moment_screen_u5"], "predecessor local screen changed") + separate_profile = profile.copy() + separate_profile[1] = separate_profile.get(1, 0) + len(blocks) + separate_screen = core.moment_screen(separate_profile, centre + len(blocks)) + need(separate_screen == candidate["one_unit_per_aggregate_translation_screen"], + "separate-correction screen changed") + need(Q(fused_screen["ceiling_upper"]) > Q(separate_screen["ceiling_upper"]), + "deferring corrections did not recover local ceiling") + overhead = candidate["all_in_rank1_overhead_threshold"] + max_overhead = overhead["largest_passing"]["extra_rank1_equivalent_charge"] + need(max_overhead == 157 and max_overhead - len(blocks) == 134, + "rank-one overhead arithmetic changed") + + # Negative controls: one missing block leaves its nonzero translation behind; + # a duplicated port violates the exact cover before any algebra is applied. + missing_xor = 0 + for delta in block_deltas[:-1]: + missing_xor ^= delta + need(missing_xor != 0, "missing-block control did not expose endpoint debt") + bad_blocks = [group[:] for group in blocks] + bad_blocks[-1][0] = bad_blocks[0][0] + bad_flat = [port for group in bad_blocks for port in group] + need(sorted(bad_flat) != list(range(112)), "duplicate-port control was accepted") + + print("PASS_GLOBAL_P112_ENDPOINT_CANCELLATION", + f"blocks={len(blocks)}", f"local_basis_cases={local_cases}", + f"label_xor={all_labels_xor}", f"delta_rank=9", + f"separate_a_ceiling={separate_screen['ceiling_upper_decimal']:.12f}", + f"deferred_a_ceiling={fused_screen['ceiling_upper_decimal']:.12f}", + f"rank1_overhead={max_overhead}", + "physical_shared_register=OPEN") + + +if __name__ == "__main__": + main() diff --git a/research/xor-endpoint-tapes/machine.py b/research/xor-endpoint-tapes/machine.py new file mode 100644 index 0000000000..1710effc98 --- /dev/null +++ b/research/xor-endpoint-tapes/machine.py @@ -0,0 +1,212 @@ +"""Literal two-tape, four-symbol machines for XOR record permutations. +Dugongue, with substantial OpenAI Codex assistance. Apache-2.0. +Compile-time integers generate a finite transition table. The online runner +uses only the table, scanned symbols, unit moves, writes and finite state. +""" +from dataclasses import dataclass + +ZERO,ONE,SEP,BLANK=range(4) +ALPHABET=range(4) + + +def need(ok,message): + if not ok: + raise ValueError(message) + + +def integer(n,minimum,name): + need(type(n) is int and n>=minimum,name) + + +def reverse_bits(delta,h): + value=0 + for _ in range(h): + value=2*value+(delta&1) + delta >>= 1 + return value + + +def variation(h,delta): + integer(h,0,'dimension') + integer(delta,0,'mask') + need(delta < 1 << h,'mask range') + value=0 + for k in range(1,h+1): + low=delta&((1 << (k-1))-1) + jump=1+2*low if not ((delta>>(k-1))&1) else (1 << k)-1-2*low + value=2*value+jump + return value + + +@dataclass +class Machine: + h:int + delta:int + operations:tuple[str,...] + table:dict + halt:int + mode:str='copy' + + @property + def input_travel(self): + return sum(op in ('R0','L0') for op in self.operations) + + +def compile_machine(h,delta): + integer(h,0,'dimension') + integer(delta,0,'mask') + n=1 << h + need(delta0 else 'L0']*abs(step)) + operations.append('C') + position=source+1 # copying ends at the following separator + operations.extend(['L0']*position) + operations.extend(['L1']*n) + table={} + for i,op in enumerate(operations): + entry,scan,next_state=2*i,2*i+1,2*i+2 + for a in ALPHABET: + for b in ALPHABET: + if op=='C': + if a==SEP:table[(entry,a,b)]=(scan,None,SEP,1,1) + if a in (ZERO,ONE):table[(scan,a,b)]=(scan,None,a,1,1) + elif a==SEP:table[(scan,a,b)]=(next_state,None,SEP,0,0) + elif op in ('R0','L0'): + direction=1 if op=='R0' else -1 + if a==SEP:table[(entry,a,b)]=(scan,None,None,direction,0) + if a in (ZERO,ONE):table[(scan,a,b)]=(scan,None,None,direction,0) + elif a==SEP:table[(scan,a,b)]=(next_state,None,None,0,0) + elif op=='L1': + if b==SEP:table[(entry,a,b)]=(scan,None,None,0,-1) + if b in (ZERO,ONE):table[(scan,a,b)]=(scan,None,None,0,-1) + elif b==SEP:table[(scan,a,b)]=(next_state,None,None,0,0) + else:raise ValueError('unknown macro') + machine=Machine(h,delta,tuple(operations),table,2*len(operations)) + expected=variation(h,delta)+1+2*reverse_bits(delta,h) + need(machine.input_travel==expected,'closed travel formula') + need(expected <= (h+1)*n,'travel upper bound') + need(len(table)==16*len(operations),'complete finite transition inventory') + return machine + + +def inplace_travel(h,delta): + integer(h,0,'dimension');integer(delta,0,'mask') + n=1 << h;need(delta=b:continue + for address in (a,b,a): + step=address-position + operations.extend(['R0' if step>0 else 'L0']*abs(step)) + operations.append('W') + position=address # swap rewinds both heads to their record starts + operations.extend(['L0']*position) + table={};state=0 + for op in operations: + count=3 if op=='W' else 2 + entry,scan,next_state=state,state+1,state+count + for a in ALPHABET: + for b in ALPHABET: + if op=='W': + rewind=state+2 + if a==b==SEP:table[(entry,a,b)]=(scan,None,None,1,1) + if a in (ZERO,ONE) and b in (ZERO,ONE): + table[(scan,a,b)]=(scan,b,a,1,1) + table[(rewind,a,b)]=(rewind,None,None,-1,-1) + elif a==b==SEP: + table[(scan,a,b)]=(rewind,None,None,-1,-1) + table[(rewind,a,b)]=(next_state,None,None,0,0) + else: + direction=1 if op=='R0' else -1 + if a==SEP:table[(entry,a,b)]=(scan,None,None,direction,0) + if a in (ZERO,ONE):table[(scan,a,b)]=(scan,None,None,direction,0) + elif a==SEP:table[(scan,a,b)]=(next_state,None,None,0,0) + state=next_state + machine=Machine(h,delta,tuple(operations),table,state,'inplace') + need(machine.input_travel==inplace_travel(h,delta),'in-place closed travel') + return machine + + +def encode(records,origin=0): + tape={origin:SEP};position=origin + for word in records: + need(all(type(x) is int and x in (0,1) for x in word),'binary record') + for bit in word: + position+=1;tape[position]=bit + position+=1;tape[position]=SEP + return tape,position + + +def decode(tape,n,origin=0): + position=origin + need(tape.get(position,BLANK)==SEP,'initial separator') + result=[] + for _ in range(n): + position+=1;word=[] + while tape.get(position,BLANK) in (ZERO,ONE): + word.append(tape[position]);position+=1 + need(tape.get(position,BLANK)==SEP,'terminated record') + result.append(tuple(word)) + return result,position + + +def run(machine,input_tape,output_tape,input_origin=0,output_origin=0,limit=10000000): + """Execute one literal transition at a time. No address arithmetic here.""" + tapes=[dict(input_tape),dict(output_tape)] + heads=[input_origin,output_origin] + minimum=heads.copy();maximum=heads.copy() + writes=[set(),set()] + state=steps=0 + while state != machine.halt: + need(steps>k)&1 + for component in pair for k in reversed(range(width))) + + +class Controls(unittest.TestCase): + def test_domains(self): + for args in [(-1,0),(3,8),(3,-1),(True,0),(2,True)]: + with self.assertRaises(ValueError):compile_machine(*args) + with self.assertRaises(ValueError):encode([(0,2)]) + + def test_unit_moves_and_borrowed_source(self): + machine=compile_machine(2,1) + key=next(iter(machine.table));action=machine.table[key] + machine.table[key]=(action[0],0,*action[2:]) + with self.assertRaisesRegex(ValueError,'borrowed input'):check_table(machine) + machine.table[key]=(*action[:3],2,action[4]) + with self.assertRaisesRegex(ValueError,'unit physical'):check_table(machine) + + def test_wrong_mask_and_missing_restoration(self): + records=[tuple((j>>k)&1 for k in range(3)) for j in range(8)] + machine=compile_machine(3,2);source,end=encode(records) + answer=run(machine,source,{}) + got,_=decode(answer['tapes'][1],8) + with self.assertRaises(ValueError):need(got==[records[j^1] for j in range(8)],'wrong mask') + # Halt at the first output-return macro, before restoring its head. + machine.halt=2*machine.operations.index('L1') + answer=run(machine,source,{}) + with self.assertRaises(ValueError):need(answer['heads']==(0,0),'head restoration') + + def test_missing_delimiter_and_budget(self): + records=[(0,1),(1,0)] + machine=compile_machine(1,1);source,end=encode(records) + count,_=exact_cost(machine,records) + with self.assertRaisesRegex(ValueError,'budget'):run(machine,source,{},limit=count-1) + del source[end] + with self.assertRaisesRegex(ValueError,'blocked'):run(machine,source,{},limit=count+10) + + def test_separate_complex_block_endpoints(self): + # Three independent streams have shifts 3, 6, 5 with xor zero. + # Their uncorrected product is not identity on the separate streams. + before=[];uncorrected=[];after=[] + for block,labels in enumerate([(1,2),(2,4),(1,4)]): + values=[(j-4+block,2-j) for j in range(8)] + numerators=values + for q in labels+labels:numerators=raw_phase(numerators,q) + denom=1 << (2*len(labels)) + need(all(a%denom==b%denom==0 for a,b in numerators),'exact block denominator') + returned=[(a//denom,b//denom) for a,b in numerators] + delta=labels[0]^labels[1] + need(returned==[values[j^delta] for j in range(8)],'universal C_E squared identity') + words=[bits(z) for z in returned] + _,result,_=execute(3,delta,words) + corrected,_=decode(result['tapes'][1],8,21) + self.assertEqual(corrected,[bits(z) for z in values]) + before.append(values);uncorrected.append(returned);after.append(corrected) + self.assertNotEqual(before,uncorrected) + + def test_involution_and_dirty_windows(self): + records=[tuple((j+2*k)%2 for k in range(j%4)) for j in range(16)] + _,first,_=execute(4,11,records,-20,40) + intermediate,_=decode(first['tapes'][1],16,40) + _,second,_=execute(4,11,intermediate,7,-100) + final,_=decode(second['tapes'][1],16,-100) + self.assertEqual(final,records) + + def test_dirty_scratch_swap_requires_third_pass(self): + machine=compile_inplace(1,1) + swaps=[i for i,op in enumerate(machine.operations) if op=='W'] + third=swaps[2] + machine.halt=sum(3 if op=='W' else 2 for op in machine.operations[:third]) + data,_=encode([(1,0),(0,0)]) + scratch,_=encode([(1,1)]) + result=run(machine,data,scratch) + with self.assertRaises(ValueError):need(result['tapes'][1]==scratch,'dirty scratch not restored') + + def test_export_cli_and_source_receipt_mutants(self): + with TemporaryDirectory(prefix='xor-endpoint-') as temp: + copy=Path(temp)/'package' + shutil.copytree(ROOT,copy,ignore=shutil.ignore_patterns('__pycache__')) + command=[sys.executable,'-B',str(copy/'verify.py')] + good=subprocess.run(command,cwd=temp,capture_output=True,text=True,timeout=60) + self.assertEqual(good.returncode,0,good.stderr);self.assertIn('RECEIPT_MATCH',good.stdout) + receipt=copy/'RESULT.json';original=receipt.read_bytes() + receipt.write_text('{}',encoding='utf-8') + bad=subprocess.run(command,cwd=temp,capture_output=True,text=True,timeout=60) + self.assertNotEqual(bad.returncode,0);self.assertIn('receipt changed',bad.stderr) + receipt.write_bytes(original) + predecessor=copy/'inputs/PR3480-verify.py' + predecessor.write_bytes(predecessor.read_bytes()+b'\n# mutation\n') + bad=subprocess.run(command,cwd=temp,capture_output=True,text=True,timeout=60) + self.assertNotEqual(bad.returncode,0);self.assertIn('source hash',bad.stderr) + + +if __name__=='__main__':unittest.main() diff --git a/research/xor-endpoint-tapes/verify.py b/research/xor-endpoint-tapes/verify.py new file mode 100644 index 0000000000..4a3f5754ea --- /dev/null +++ b/research/xor-endpoint-tapes/verify.py @@ -0,0 +1,173 @@ +"""Exact transition-table replay and P112 predecessor-mask application. +Dugongue, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +from itertools import product +import argparse +import ast +import hashlib +import json + +from machine import (BLANK,SEP,compile_machine,compile_inplace,decode,encode, + exact_cost,inplace_travel,need,reverse_bits,run,variation) + +ROOT=Path(__file__).resolve().parent + + +def authenticate(): + data=json.loads((ROOT/'INPUTS.json').read_text(encoding='utf-8')) + for name,digest in data['sha256'].items(): + p=(ROOT/name).resolve() + need(p.is_relative_to(ROOT) and p.is_file(),'source path') + need(hashlib.sha256(p.read_bytes()).hexdigest()==digest,'source hash '+name) + + +def predecessor_masks(): + authenticate() + tree=ast.parse((ROOT/'inputs/PR3480-verify.py').read_text(encoding='utf-8')) + literals=[] + for node in ast.walk(tree): + if isinstance(node,ast.Assign) and any(isinstance(t,ast.Name) and t.id=='expected_deltas' for t in node.targets): + literals.append(ast.literal_eval(node.value)) + need(len(literals)==1,'unique predecessor mask literal') + values=literals[0] + need(len(values)==23 and all(type(d) is int and 0<=d<512 for d in values),'P112 mask shape') + return values + + +def check_table(machine): + need(machine.halt==sum(3 if op=='W' else 2 for op in machine.operations),'finite state count') + need(all(0<=s>(width-1-k))&1 for k in range(width)) for j in range(n)] + data,end=encode(words,-17) + scratch,send=encode([tuple((3*k+1)%2 for k in range(width))],31) + data[-24]=SEP;data[end+7]=1;scratch[22]=0;scratch[send+11]=SEP + original_data=data.copy();original_scratch=scratch.copy() + travel=inplace_travel(h,delta) + invoice=0 if delta==0 else (3*n//2)*(2*width+3)+(width+2)*travel + result=run(machine,data,scratch,-17,31,limit=invoice+1) + got,_=decode(result['tapes'][0],n,-17) + need(got==[words[j^delta] for j in range(n)],'in-place XOR permutation') + need(result['tapes'][1]==original_scratch,'arbitrary dirty scratch restored') + need(result['heads']==(-17,31),'in-place heads restored') + need(result['steps']==invoice,'in-place exact time invoice') + need(result['minimum'][0]>=-17 and result['maximum'][0]<=end,'in-place data scan window') + need(result['minimum'][1]>=31 and result['maximum'][1]<=send,'in-place scratch scan window') + need(all(result['tapes'][0][k]==v for k,v in original_data.items() + if k < -17 or k > end),'in-place dirty exterior frame') + need(all(-17<=k<=end for k in result['writes'][0]),'in-place write window') + need(all(31<=k<=send for k in result['writes'][1]),'scratch write window') + need(data==original_data and scratch==original_scratch,'caller storage preserved') + return result['steps'] + + +def run_checks(): + cases=steps=0 + for h in range(6): + n=1 << h + for delta in range(n): + f=[j^delta for j in range(n)] + direct=sum(abs(b-a) for a,b in zip(f,f[1:])) + need(variation(h,delta)==direct,'independent variation recurrence') + direct_q=f[0]+sum(abs(b-a-1) for a,b in zip(f,f[1:]))+f[-1]+1 + need(direct_q==direct+1+2*reverse_bits(delta,h),'bit-reversal travel identity') + for width in (0,1,3): + words=[tuple((j+3*k+(j>>1))%2 for k in range(width)) for j in range(n)] + machine,result,cross=execute(h,delta,words) + need(sum(cross)==machine.input_travel,'edge scan count') + need(result['steps']==n*(2*width+4)+(width+2)*direct_q,'fixed-width exact time') + need(result['steps']<=n*((h+3)*width+2*h+6),'universal time bound') + cases+=1;steps+=result['steps'] + variable=[tuple((j+k)%2 for k in range(j%5)) for j in range(n)] + _,result,_=execute(h,delta,variable) + cases+=1;steps+=result['steps'] + # Full basis corroboration in every small address space. + basis=0 + for h in range(4): + n=1 << h + for delta in range(n): + for pos in range(n): + words=[(int(j==pos),) for j in range(n)] + _,result,_=execute(h,delta,words) + steps+=result['steps'];basis+=1 + # Literal 23-mask P112 application: these are separate tape instances. + # This authenticates source masks, not the complete original cover proof. + literal=[] + words=[tuple((j>>(8-k))&1 for k in range(9)) for j in range(512)] + for block,delta in enumerate(predecessor_masks()): + machine,result,_=execute(9,delta,words) + literal.append({'block':block,'delta':delta,'input_record_travel':machine.input_travel, + 'states':machine.halt+1,'transitions':len(machine.table), + 'time_width_9':result['steps'], + 'time_coefficient_B':1024+machine.input_travel, + 'time_constant':2048+2*machine.input_travel, + 'inplace_record_travel':inplace_travel(9,delta), + 'inplace_time_coefficient_B':1536+inplace_travel(9,delta), + 'inplace_time_constant':2304+2*inplace_travel(9,delta)}) + steps+=result['steps'] + inplace_cases=0 + for h in range(5): + for delta in range(1 << h): + for width in (0,1,4): + steps+=execute_inplace(h,delta,width);inplace_cases+=1 + # One literal nine-bit mask, block 10's delta=19, is also fully executed + # in place. Other nine-bit in-place bills are universal formulas, not runs. + steps+=execute_inplace(9,19,9);inplace_cases+=1 + return {'schema_version':1,'status':'PASS_XOR_ENDPOINT_TAPES', + 'parameter_cases':cases,'full_small_basis_cases':basis,'literal_masks':23, + 'inplace_parameter_cases':inplace_cases, + 'executed_unit_transitions':steps,'p112':literal, + 'alphabet':['0','1','#','blank'],'tapes':2, + 'uniform_time_bound':'2^h*((h+3)*B+2*h+6)', + 'coverage':'Every transition is a literal finite-control, unit-move two-tape step. Universal proof is in PROOF.md; source/consumer identification and complete recursive invoice remain outside this result.'} + + +def main(): + ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('--emit',action='store_true');args=ap.parse_args() + result=run_checks() + if args.emit:print(json.dumps(result,indent=2,sort_keys=True)) + else: + need(result==json.loads((ROOT/'RESULT.json').read_text(encoding='utf-8')),'result receipt changed') + print(f"PASS_XOR_ENDPOINT_TAPES parameter_cases={result['parameter_cases']} basis_cases={result['full_small_basis_cases']} literal_masks=23 steps={result['executed_unit_transitions']} RECEIPT_MATCH") + + +if __name__=='__main__':main()