diff --git a/research/nested-xor-scratch-tapes/PROOF.md b/research/nested-xor-scratch-tapes/PROOF.md new file mode 100644 index 0000000000..7c06503323 --- /dev/null +++ b/research/nested-xor-scratch-tapes/PROOF.md @@ -0,0 +1,147 @@ +# Nested swaps for an in-place XOR correction + +The construction and proof were produced by Nick Petalas. Apache-2.0. +The two-tape record interface, R0/L0/W templates and serial comparison +formula are Dugongue / David Ganz's [PR #3879](https://github.com/CrocSwap/integer-mult-bounds/pull/3879). +Those are cited premises. This package does not audit that predecessor. + +## Contract and theorem + +Let h >= 1, N = 2^h and 0 < delta < N. Write delta = m+l, where m is a +power of two and 0 <= l < m. Let c = N/(2m). Tape zero contains + +``` +# w_0 # w_1 # ... # w_(N-1) # +``` + +with N arbitrary binary records of the same width B >= 0. Tape one +contains one arbitrary dirty record of width B, framed by two separators. +Both heads start at their opening separators, at arbitrary integer origins. +All tape cells outside these windows are arbitrary and must be preserved. +The alphabet is {0,1,#,blank}. Each transition reads both scanned symbols, +writes at most one symbol per tape and moves each head by at most one cell. + +There is a finite controller that implements w'_j = w_(j xor delta), +restores the complete scratch record and both heads, and preserves both +exteriors. Its exact number of transitions is + +``` +H_nested = N*m + 2*(c-1)*(l+1) +T_nested = (3N/2)*(2B+3) + (B+2)*H_nested. +``` + +Its control has 2*H_nested + 9N/2 + 1 states including halt, and +16*H_nested + 33N/2 defined transition entries. It uses the same B+2 +scratch cells, including separators, as the predecessor. The first tape's +visited window has N*(B+1)+1 cells. These statements hold for all h and B. +The executable evidence has explicit expansion bounds described below. +For delta = 0, the controller is already halted, with zero transitions. + +PR #3879's serial schedule has + +``` +H_serial = (N-2)*m + 2N-2. +``` + +The new schedule saves at least (N-2)*(B+2) transitions for every nonzero +mask. The saving is strict for N >= 4. This is an exact machine invoice, +not a wall-clock measurement or a recursive rank saving. No minimum over +all possible tape machines or all swap orders is asserted. + +## Schedule and arbitrary dirty scratch + +List a_0 < ... < a_(q-1), q=N/2, with a_i < b_i = a_i xor delta. +These are exactly the indices whose m bit is zero. In particular a_0=0. +Let W(v) swap the record at address v with the scratch record and rewind +both heads to their entry separators. It is the predecessor's three-state +W template, costing 2B+3 transitions for arbitrary record contents. + +Use this visit order, with literal R0/L0 seeks between visits: + +``` +a_0, a_1, ..., a_(q-1), +b_(q-1), a_(q-1), ..., b_1, a_1, b_0, a_0. +``` + +There are exactly 3q record swaps. There is no online stack or online +address arithmetic. The finite compiler unrolls every seek and swap. + +For correctness, the subword for pair i is an opening W(a_i), followed +by all later pairs, followed by W(b_i), W(a_i). Induct on the number of +enclosed pairs. The enclosed subword acts only on its own disjoint data +pairs and restores whatever scratch value it receives. Thus it returns +the scratch value left by the opening W(a_i), even though that value is +an arbitrary original data record rather than the original scratch dirt. +The remaining two swaps finish the transposition of a_i,b_i and restore +the incoming scratch value. The induction proves the desired disjoint +transpositions, including arbitrary dirt restoration. This is the usual +star-transposition identity applied to a nested schedule. + +Every data address occurs in a W, and the final visit is a_0=0. Each W +rewinds both heads. The data head therefore returns to its origin and +the scratch head never leaves its declared record. All seeks stay between +valid data-record separators. The predecessor templates write no exterior +cell. This proves the restoration, frame and visited-window statements. + +## Exact travel + +Put D_i=b_i-a_i>0 and d_i=a_(i+1)-a_i for i=1, so the positive-part term is zero. +At each of the c-1 block boundaries, the old representative is +2mt+m-1, its partner is 2mt+2m-1-l, and the next representative is +2mt+2m. The positive part is exactly l+1. Substitution gives the claimed +H_nested. No monotonicity of the partner sequence was assumed. + +For comparison, the cited serial formula gives + +``` +H_serial-H_nested = 2*(N-m-1-(c-1)*(l+1)) + >= 2*(N-m-1-(c-1)*m) + = N-2. +``` + +There are the same 3N/2 W macros in both constructions. Every seek crosses +one width-B record and costs B+2. Multiplication gives the exact transition +saving. Each seek contributes two states and sixteen transition entries; +each W contributes three states and eleven entries. Add one halt state. +The compiler also saves twice the crossing reduction in states and sixteen +times that reduction in transition entries. Control is not treated as free. + +## Evidence and limits + +The written schedule is uniform for every finite h. The supplied compiler +allows 0<=h<=9 and at most 250,000 transition entries, before allocation. +Larger controllers are not silently approximated; expansion fails. The +schedule and token-permutation checker covers every h<=9 and every mask, +including controllers too large for literal expansion. The unit-step +executor covers every mask through h=5, widths 0..3, complete one-bit +data/scratch basis fixtures through h=3, and two h=9 machines. The complete +RESULT records the enumerated counts. Its finite evidence corroborates the +proof; it does not establish the universal quantifiers by enumeration. + +No predecessor executable is imported or replayed. Its transition templates +are reimplemented here with attribution. The independent executor dispatches +only literal table entries, never an address-seek or record-swap oracle. +The executable compiler stores a bounded host-side finite table; it does +not claim an unpriced fixed-control online interpreter for arbitrary h. + +Acquiring an actual native return in this record layout, buffer placement, +representation conversions, the complete caller and its recursive invoice +remain open. No selected framework assumption, new kappa, complete rounded +multiplier, human review or formal proof-kernel acceptance is supplied. diff --git a/research/nested-xor-scratch-tapes/README.md b/research/nested-xor-scratch-tapes/README.md new file mode 100644 index 0000000000..57c8e68350 --- /dev/null +++ b/research/nested-xor-scratch-tapes/README.md @@ -0,0 +1,128 @@ +# Fewer head crossings for dirty-scratch XOR correction + +The construction, proof and verifier were produced by Nick Petalas. +Apache-2.0. Claim type: scoped construction and mathematical proof, with +exact finite machine evidence. No new kappa. + +Nesting the scratch swaps in Dugongue / David Ganz's +[PR #3879](https://github.com/CrocSwap/integer-mult-bounds/pull/3879) +reduces its in-place XOR correction cost for every nonzero mask on N>=4 +records. Both heads and the arbitrary dirty scratch record still return +exactly. The alphabet, record representation, scratch capacity and 3N/2 +record swaps are the same. + +For N=2^h, delta=m+l, m the highest power of two in delta, and 0<=l= 0, "invalid record width") + if delta: + travel = n * m + 2 * (n // (2 * m) - 1) * (low + 1) + serial = (n - 2) * m + 2 * n - 2 # PR3879, Theorem B + swaps = 3 * n // 2 + else: + travel = serial = swaps = 0 + return { + "records": n, "mask": delta, "width": width, + "record_swaps": swaps, "record_crossings": travel, + "serial_record_crossings": serial, + "saved_record_crossings": serial - travel, + "steps": swaps * (2 * width + 3) + travel * (width + 2), + "saved_steps": (serial - travel) * (width + 2), + "states_including_halt": 3 * swaps + 2 * travel + 1, + "table_entries": 11 * swaps + 16 * travel, + } + + +@dataclass(frozen=True) +class Machine: + operations: tuple + table: dict + halt: int + + +def template(table, state, op): + """Literal four-symbol templates from PR3879, not an online macro oracle.""" + need(op in ("R0", "L0", "W"), "unknown macro") + following = state + (3 if op == "W" else 2) + scan, rewind = state + 1, state + 2 + for a in range(4): + for b in range(4): + if op == "W": + if a == b == SEP: + table[state, a, b] = (scan, None, None, 1, 1) + table[scan, a, b] = (rewind, None, None, -1, -1) + table[rewind, a, b] = (following, None, None, 0, 0) + elif 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) + else: + direction = 1 if op == "R0" else -1 + if a == SEP: + table[state, a, b] = (scan, None, None, direction, 0) + table[scan, a, b] = (following, None, None, 0, 0) + elif a in (ZERO, ONE): + table[scan, a, b] = (scan, None, None, direction, 0) + return following + + +def compile_visits(h, delta, order, *, return_head=True): + """Also accepts bounded wrong orders for executable rejection controls.""" + n, _, _ = parameters(h, delta) + need(type(order) is tuple and len(order) <= 3 * n, "visit capacity") + need(all(type(a) is int and 0 <= a < n for a in order), "visit address") + position = 0 + travel = 0 + for address in order: + travel += abs(address - position) + position = address + travel += position if return_head else 0 + entries = 16 * travel + 11 * len(order) + need(entries <= MAX_TABLE_ENTRIES, "literal table capacity exceeded") + operations = [] + position = 0 + for address in order: + step = address - position + operations.extend(("R0" if step > 0 else "L0",) * abs(step)) + operations.append("W") + position = address + if return_head: + operations.extend(("L0",) * position) + table = {} + state = 0 + for op in operations: + state = template(table, state, op) + need(len(table) == entries, "transition-template inventory") + need(state == 2 * travel + 3 * len(order), "state inventory") + return Machine(tuple(operations), table, state) + + +def compile_machine(h, delta): + machine = compile_visits(h, delta, visits(h, delta)) + bill = invoice(h, delta, 0) + need(len(machine.table) == bill["table_entries"], "closed table bill") + need(machine.halt + 1 == bill["states_including_halt"], "closed state bill") + return machine diff --git a/research/nested-xor-scratch-tapes/verify.py b/research/nested-xor-scratch-tapes/verify.py new file mode 100644 index 0000000000..eccb3fb779 --- /dev/null +++ b/research/nested-xor-scratch-tapes/verify.py @@ -0,0 +1,204 @@ +"""Execute the new nested controllers; never replay a predecessor verifier. + +Produced by Nick Petalas. Apache-2.0. +""" + +import argparse +from dataclasses import replace +from hashlib import sha256 +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) + +from machine import ( + BLANK, SEP, compile_machine, compile_visits, invoice, need, visits, +) + +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "RESULT.json", "machine.py", "verify.py", +) + + +def frame(records, origin): + tape = {origin: SEP, origin - 2: 1, origin - 1: 3} + position = origin + for record in records: + for bit in record: + need(type(bit) is int and bit in (0, 1), "binary fixture") + position += 1 + tape[position] = bit + position += 1 + tape[position] = SEP + tape[position + 1] = 0 + tape[position + 2] = SEP + return tape, position + + +def execute(machine, tapes, origins, limit): + """Only symbol lookup, finite-state dispatch, writes and unit head moves.""" + need(type(limit) is int and 0 <= limit <= 1_000_000, "step capacity") + work = [dict(tapes[0]), dict(tapes[1])] + heads = list(origins) + minimum, maximum = list(origins), list(origins) + state = 0 + for steps in range(limit + 1): + if state == machine.halt: + return work, tuple(heads), steps, minimum, maximum + need(steps < limit, "transition budget exhausted") + a = work[0].get(heads[0], BLANK) + b = work[1].get(heads[1], BLANK) + action = machine.table.get((state, a, b)) + need(action is not None and len(action) == 5, "blocked finite control") + state, w0, w1, m0, m1 = action + need(type(state) is int and 0 <= state <= machine.halt, "state range") + for i, value, move in ((0, w0, m0), (1, w1, m1)): + need(type(move) is int and move in (-1, 0, 1), "nonunit head move") + if value is not None: + need(type(value) is int and 0 <= value < 4, "alphabet write") + work[i][heads[i]] = value + heads[i] += move + minimum[i] = min(minimum[i], heads[i]) + maximum[i] = max(maximum[i], heads[i]) + raise ValueError("unreachable exhausted execution") + + +def check_case(h, delta, width, *, basis=None, candidate=None): + n = 1 << h + if basis is None: + records = [tuple((i * 3 + j + (i >> (j % 3))) % 2 + for j in range(width)) for i in range(n)] + dirty = tuple((j + 1) % 2 for j in range(width)) + else: + records = [tuple(int(i == basis) for _ in range(width)) for i in range(n)] + dirty = tuple(int(basis == n) for _ in range(width)) + origins = (11, -7) + initial, end0 = frame(records, origins[0]) + scratch, end1 = frame([dirty], origins[1]) + expected, _ = frame([records[i ^ delta] for i in range(n)], origins[0]) + bill = invoice(h, delta, width) + machine = candidate if candidate is not None else compile_machine(h, delta) + result, heads, steps, minimum, maximum = execute( + machine, (initial, scratch), origins, bill["steps"] + 2000) + need(result == [expected, scratch], "permutation, dirt or exterior mismatch") + need(heads == origins, "head return mismatch") + need(steps == bill["steps"], "exact transition invoice mismatch") + need(minimum == list(origins), "crossed a left exterior") + need(maximum[0] <= end0 and maximum[1] <= end1, "crossed a right exterior") + return steps + + +def check_schedules(): + cases = strict = 0 + smallest = None + largest = 0 + for h in range(10): + n = 1 << h + for delta in range(n): + order = visits(h, delta) + tokens = list(range(n + 1)) + position = travel = 0 + for address in order: + travel += abs(address - position) + position = address + tokens[address], tokens[n] = tokens[n], tokens[address] + travel += position + need(tokens == [i ^ delta for i in range(n)] + [n], "token endpoint") + bill = invoice(h, delta, 2) + need(travel == bill["record_crossings"], "independent travel sum") + need(len(order) == bill["record_swaps"], "swap count") + if delta: + gain = bill["saved_record_crossings"] + need(gain >= n - 2, "uniform improvement inequality") + strict += int(gain > 0) + if h == 9: + smallest = gain if smallest is None else min(smallest, gain) + largest = max(largest, gain) + cases += 1 + return {"cases": cases, "strict_improvements": strict, + "n512_saved_crossings_min": smallest, + "n512_saved_crossings_max": largest} + + +def rejected(action): + try: + action() + except ValueError: + return 1 + raise ValueError("a rejection control was accepted") + + +def controls(): + order = visits(2, 2) + n = 4 + roots = order[:n // 2] + wrong_order = roots + tuple(v for a in roots for v in (a ^ 2, a)) + wrong = compile_visits(2, 2, wrong_order) + missing = compile_visits(2, 2, order[:-1]) + good = compile_machine(2, 2) + bad_move = dict(good.table) + bad_move[0, SEP, SEP] = (1, None, None, 2, 1) + bad_write = dict(good.table) + bad_write[0, SEP, SEP] = (1, 7, None, 1, 1) + fixture, _ = frame([(0,)] * 4, 0) + scratch, _ = frame([(1,)], 0) + broken = dict(fixture) + broken[0] = BLANK + checks = ( + lambda: check_case(2, 2, 1, basis=0, candidate=wrong), + lambda: check_case(2, 2, 1, basis=0, candidate=missing), + lambda: check_case(2, 2, 1, basis=0, candidate=compile_machine(2, 1)), + lambda: execute(replace(good, table=bad_move), (fixture, scratch), (0, 0), 50), + lambda: execute(replace(good, table=bad_write), (fixture, scratch), (0, 0), 50), + lambda: execute(good, (broken, scratch), (0, 0), 50), + lambda: execute(good, (fixture, scratch), (0, 0), 0), + lambda: compile_machine(9, 256), + lambda: compile_machine(10, 1), + lambda: compile_machine(3, 8), + lambda: compile_machine(True, 1), + lambda: invoice(2, 1, -1), + ) + return sum(rejected(action) for action in checks) + + +def science(): + schedules = check_schedules() + cases = transitions = basis_cases = 0 + for h in range(6): + for delta in range(1 << h): + for width in range(4): + transitions += check_case(h, delta, width) + cases += 1 + for h in range(4): + for delta in range(1 << h): + for basis in range((1 << h) + 1): + transitions += check_case(h, delta, 1, basis=basis) + basis_cases += 1 + for delta, width in ((1, 3), (16, 2)): + transitions += check_case(9, delta, width) + cases += 1 + return {"status": "PASS_NESTED_XOR_SCRATCH_TAPES", "schedules": schedules, + "payload_cases": cases, "basis_cases": basis_cases, + "executed_unit_transitions": transitions, + "rejecting_controls": controls(), + "examples": [invoice(2, 2, 1), invoice(9, 1, 3), invoice(9, 16, 2)]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-result", action="store_true") + args = parser.parse_args() + result = science() + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + need(result == expected, "complete RESULT payload differs") + hashes = {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + receipt = {"result": result, "package_sha256": hashes} + print(json.dumps(receipt if args.emit_result else result, sort_keys=True)) + + +if __name__ == "__main__": + main()