From 4be95e7135920931a58ab09a8b5b5487c9d6f3ca Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:48:17 +0100 Subject: [PATCH] perf(research): fuse packed tape reads and writes --- research/packed-tape-fusion/README.md | 219 +++++++++++++++++++++++ research/packed-tape-fusion/RESULT.json | 22 +++ research/packed-tape-fusion/SOURCES.json | 42 +++++ research/packed-tape-fusion/TASK.json | 80 +++++++++ research/packed-tape-fusion/VERIFY.json | 32 ++++ research/packed-tape-fusion/fusion.py | 146 +++++++++++++++ research/packed-tape-fusion/verify.py | 173 ++++++++++++++++++ 7 files changed, 714 insertions(+) create mode 100644 research/packed-tape-fusion/README.md create mode 100644 research/packed-tape-fusion/RESULT.json create mode 100644 research/packed-tape-fusion/SOURCES.json create mode 100644 research/packed-tape-fusion/TASK.json create mode 100644 research/packed-tape-fusion/VERIFY.json create mode 100644 research/packed-tape-fusion/fusion.py create mode 100644 research/packed-tape-fusion/verify.py diff --git a/research/packed-tape-fusion/README.md b/research/packed-tape-fusion/README.md new file mode 100644 index 0000000000..8d0bed75c9 --- /dev/null +++ b/research/packed-tape-fusion/README.md @@ -0,0 +1,219 @@ +# Packed tape reads and writes in 17 instructions per tape + +This contribution is produced by Nick Petalas. + +A selected packed tape cell can be read and overwritten in 17 successful RAM +instructions, including address computation. Read each of k tapes before any +write, retain four observations per tape, and the access bill is exactly 17k. +The separately emitted GET and SET macros in Dugongue's +[PR #4538](https://github.com/CrocSwap/integer-mult-bounds/pull/4538) cost 13k+17k=30k. +The new local schedule eliminates 13k instructions. This is a scoped construction +proof with finite executable corroboration. It is neither an optimality theorem +nor a new multiplication bound. + +The contribution isolates a small part of the predecessor's complete-packed-backend +next question. Its representation and machine semantics are cited premises; +rechecking those results is not the deliverable. The XOR bit-field identity is +standard. The new repository result is the retained-read contract, explicit +instruction schedule and cost reduction at a simultaneous-read boundary. + +## Contract + +Fix k>=1 tapes, c=2^ell bits per field, B=2^b fields per word, H=2^h>=2k, +and a data base R above every control/cache register. For tape i with signed +head z, set u=z if z>=0, otherwise u=-z-1, and tag=2i+[z<0]. Its word address +and field offset are + +``` +a = R + H floor(u/B) + tag +offset = c (u mod B) +``` + +Assume cB<=w, u<2^w, a<2^w, and every register, literal constant and effective +address fits the w-bit machine. The packed data can contain arbitrary dirty +words, including arbitrary unused high bits and arbitrary unselected fields. +The symbol selected for writing satisfies 0<=new<2^c. + +The read phase keeps a, offset, the loaded word W, and the old selected field +s=(W>>offset) AND (2^c-1) in separate registers for each tape. The intervening +finite dispatcher may read the old symbols and compute new symbols. It must +preserve these four caches, shared B metadata and all packed data words. Its +registers must be disjoint from the cache registers. Its actual instructions +are paid separately. These assumptions permit a usual finite TM dispatcher +that reads all tapes before writing any tape. + +After the dispatch, commit each tape exactly once. Heads can then advance. +The result has exactly the chosen new symbol at each selected position and +preserves every other data bit. Cache/scratch registers are clobbered; this is +not a reversible dirty-workspace restoration claim. + +## Four-instruction commit and proof + +The emitted commit uses register operands throughout: + +``` +xor delta, old, new +shiftl delta, delta, offset +xor word, word, delta +store address, word +``` + +Let M=2^c-1. Write W=L+2^offset s+2^(offset+c) U, where +0<=L<2^offset and 0<=s<=M. The three summands occupy disjoint bit ranges. +Since both s and new are c-bit values, delta=(s XOR new)< None: + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Layout: + """Bounded executable domain; the written identity has no 64-tape limit.""" + + tapes: int + field_log: int + block_log: int + width: int + + def __post_init__(self) -> None: + for value in (self.tapes, self.field_log, self.block_log, self.width): + require(type(value) is int, "integer layout parameters required") + require(1 <= self.tapes <= 64, "tape count outside 1..64") + require(0 <= self.field_log <= 4, "field log outside 0..4") + require(0 <= self.block_log <= 8, "block log outside 0..8") + require(10 <= self.width <= 256, "word width outside 10..256") + require(self.field_bits * self.block_size <= self.width, "fields overflow") + require(self.base + self.stride <= self.word_mask, "address region overflow") + + @property + def field_bits(self) -> int: + return 1 << self.field_log + + @property + def block_size(self) -> int: + return 1 << self.block_log + + @property + def stride_log(self) -> int: + return (2 * self.tapes - 1).bit_length() + + @property + def stride(self) -> int: + return 1 << self.stride_log + + @property + def base(self) -> int: + return 1 << max(7, (8 + 16 * self.tapes - 1).bit_length()) + + @property + def word_mask(self) -> int: + return (1 << self.width) - 1 + + +def register(tape: int) -> int: + require(type(tape) is int and 0 <= tape < 64, "invalid tape register") + return 8 + 16 * tape + + +def read_code(layout: Layout, tape: int) -> list[tuple]: + """Retain address, offset, loaded word and observed field in this slab.""" + require(0 <= tape < layout.tapes, "tape not in layout") + r = register(tape) + return [ + ("shiftr", r + 3, r, 0), + ("and", r + 4, r, 1), + ("set", r + 5, layout.field_log), + ("shiftl", r + 6, r + 4, r + 5), + ("set", r + 7, layout.stride_log), + ("shiftl", r + 8, r + 3, r + 7), + ("add", r + 8, r + 8, r + 1), + ("set", r + 9, layout.base), + ("add", r + 8, r + 8, r + 9), + ("load", r + 10, r + 8), + ("shiftr", r + 11, r + 10, r + 6), + ("set", r + 12, (1 << layout.field_bits) - 1), + ("and", r + 13, r + 11, r + 12), + ] + + +def commit_code(layout: Layout, tape: int) -> list[tuple]: + require(0 <= tape < layout.tapes, "tape not in layout") + r = register(tape) + return [ + ("xor", r + 14, r + 13, r + 2), + ("shiftl", r + 14, r + 14, r + 6), + ("xor", r + 10, r + 10, r + 14), + ("store", r + 8, r + 10), + ] + + +def execute(code: list[tuple], memory: dict[int, int], width: int) -> int: + """Execute the bounded straight-line RamStd subset; return successful steps.""" + require(type(width) is int and 10 <= width <= 256, "invalid VM width") + require(len(code) <= 2048, "program exceeds straight-line replay bound") + require(len(memory) <= 4096, "memory exceeds replay capacity") + mask = (1 << width) - 1 + for address, value in memory.items(): + require(type(address) is int and 0 <= address <= mask, "invalid address") + require(type(value) is int and 0 <= value <= mask, "invalid word") + for record in code: + require(len(record) in (3, 4), "malformed instruction") + op, destination, *args = record + require(type(destination) is int and 0 <= destination <= mask, "bad register") + require(all(type(x) is int and 0 <= x <= mask for x in args), "bad argument") + if op == "set" and len(args) == 1: + memory[destination] = args[0] + elif op == "load" and len(args) == 1: + memory[destination] = memory.get(memory.get(args[0], 0), 0) + elif op == "store" and len(args) == 1: + memory[memory.get(destination, 0)] = memory.get(args[0], 0) + else: + require(len(args) == 2, "binary instruction needs two arguments") + x, y = (memory.get(a, 0) for a in args) + if op == "add": + result = x + y + elif op == "and": + result = x & y + elif op == "xor": + result = x ^ y + elif op == "shiftl": + result = x << y if y < width else 0 + elif op == "shiftr": + result = x >> y + else: + raise ValueError("unsupported instruction") + memory[destination] = result & mask + require(len(memory) <= 4096, "memory exceeds replay capacity") + return len(code) + + +def prepare(layout: Layout, heads: list[int], words: list[int]) -> dict[int, int]: + require(len(heads) == len(words) == layout.tapes, "one head and word per tape") + memory = {0: layout.block_log, 1: layout.block_size - 1} + for tape, (head, word) in enumerate(zip(heads, words, strict=True)): + require(type(head) is int, "signed integer head required") + require(type(word) is int and 0 <= word <= layout.word_mask, "word overflow") + index = head if head >= 0 else -head - 1 + require(index <= layout.word_mask, "head index overflows word") + tag = 2 * tape + (head < 0) + address = layout.base + layout.stride * (index // layout.block_size) + tag + require(address <= layout.word_mask, "head address wraps") + r = register(tape) + memory[r], memory[r + 1] = index, tag + memory[address] = word + return memory diff --git a/research/packed-tape-fusion/verify.py b/research/packed-tape-fusion/verify.py new file mode 100644 index 0000000000..8e765363b3 --- /dev/null +++ b/research/packed-tape-fusion/verify.py @@ -0,0 +1,173 @@ +"""Exact semantic checks and generated source-bound receipt. Apache-2.0.""" + +import argparse +import hashlib +import json +from pathlib import Path +from random import Random + +from fusion import Layout, commit_code, execute, prepare, read_code, register, require + + +def scalar_identity() -> int: + cases = 0 + for width in range(1, 11): + for bits in (1, 2, 4, 8): + for offset in range(0, width - bits + 1, bits): + mask = (1 << bits) - 1 + for word in range(1 << width): + old = (word >> offset) & mask + for new in range(1 << bits): + actual = word ^ ((old ^ new) << offset) + expected = (word & ~(mask << offset)) | (new << offset) + require(actual == expected, "field identity failed") + cases += 1 + return cases + + +def transition(layout: Layout, heads: list[int], words: list[int], new: list[int]) -> int: + memory = prepare(layout, heads, words) + # Fill every register with arbitrary dirt, leaving the ABI parameters intact. + for address in range(2, layout.base): + memory.setdefault(address, (address * 37 + 11) & layout.word_mask) + spectator = layout.word_mask + require(spectator not in memory, "fixture spectator aliases data") + memory[spectator] = layout.word_mask // 3 + initial = dict(memory) + reads = [op for tape in range(layout.tapes) for op in read_code(layout, tape)] + require(execute(reads, memory, layout.width) == 13 * layout.tapes, "read bill") + for tape, head in enumerate(heads): + index = head if head >= 0 else -head - 1 + offset = layout.field_bits * (index % layout.block_size) + old = (words[tape] >> offset) & ((1 << layout.field_bits) - 1) + require(memory[register(tape) + 13] == old, "simultaneous observation") + require(0 <= new[tape] < 1 << layout.field_bits, "new field overflow") + memory[register(tape) + 2] = new[tape] + commits = [op for tape in range(layout.tapes) for op in commit_code(layout, tape)] + require(execute(commits, memory, layout.width) == 4 * layout.tapes, "commit bill") + expected = {a: v for a, v in initial.items() if a >= layout.base} + for tape, head in enumerate(heads): + index = head if head >= 0 else -head - 1 + block, field = divmod(index, layout.block_size) + address = layout.base + layout.stride * block + 2 * tape + (head < 0) + offset = layout.field_bits * field + mask = ((1 << layout.field_bits) - 1) << offset + expected[address] = (words[tape] & ~mask) | (new[tape] << offset) + require({a: v for a, v in memory.items() if a >= layout.base} == expected, + "write, spectator, padding or bank preservation") + return 17 * layout.tapes + + +def program_cases() -> dict: + rng = Random(20261022) + cases, instructions = 0, 0 + for tapes in (1, 2, 3, 8, 16, 64): + for width in (16, 32, 64, 128, 256): + for field_log in range(5): + for block_log in range(9): + if (1 << (field_log + block_log)) > width: + continue + layout = Layout(tapes, field_log, block_log, width) + for trial in range(8): + heads = [rng.randrange(-3 * layout.block_size, + 3 * layout.block_size) for _ in range(tapes)] + if trial < 4: + heads = [(0, -1, layout.block_size - 1, + -layout.block_size - 1)[trial]] * tapes + words = [rng.getrandbits(width) for _ in range(tapes)] + new = [rng.getrandbits(layout.field_bits) for _ in range(tapes)] + instructions += transition(layout, heads, words, new) + cases += 1 + return {"transition_cases": cases, "executed_access_instructions": instructions} + + +def dispatcher_fixture() -> int: + layout = Layout(2, 1, 2, 16) + memory = prepare(layout, [0, 0], [0xABCD, 0x5678]) + reads = read_code(layout, 0) + read_code(layout, 1) + r0, r1 = register(0), register(1) + # Register 2 is initially zero. These are two actual successful instructions. + dispatch = [("xor", r0 + 2, r1 + 13, 2), ("xor", r1 + 2, r0 + 13, 2)] + code = reads + dispatch + commit_code(layout, 0) + commit_code(layout, 1) + count = execute(code, memory, layout.width) + require(count == 36, "dispatcher-inclusive instruction bill") + require(memory[layout.base] == 0xABCC and memory[layout.base + 2] == 0x5679, + "literal simultaneous swap dispatcher") + return count + + +def controls() -> dict: + invalid_layouts = [(True, 0, 0, 16), (0, 0, 0, 16), (65, 0, 0, 32), + (1, 5, 0, 64), (1, 0, 9, 256), (1, 0, 0, 9), + (1, 4, 1, 16), (64, 0, 0, 10)] + rejected = 0 + for parameters in invalid_layouts: + try: + Layout(*parameters) + except ValueError: + rejected += 1 + invalid_words = [(Layout(1, 0, 0, 10), [1000], [0]), + (Layout(1, 0, 0, 10), [0], [1024]), + (Layout(1, 0, 6, 64), [1 << 64], [0])] + for parameters in invalid_words: + try: + prepare(*parameters) + except ValueError: + rejected += 1 + try: + execute([("bad", 0, 0, 0)], {}, 16) + except ValueError: + rejected += 1 + require(rejected == 12, "invalid boundary accepted") + layout = Layout(1, 1, 1, 16) + mutations = 0 + for mutation in ("omit_delta", "shift_wrong", "clobber_cache", "stale_word"): + memory = prepare(layout, [1], [0xFFFF]) + execute(read_code(layout, 0), memory, 16) + r = register(0) + memory[r + 2] = 0 + code = commit_code(layout, 0) + if mutation == "omit_delta": + code = code[1:] + elif mutation == "shift_wrong": + code[1] = ("shiftl", r + 14, r + 14, 0) + elif mutation == "clobber_cache": + memory[r + 13] = 0 + else: + memory[layout.base] ^= 1 + before = memory[layout.base] + execute(code, memory, 16) + expected = before & ~(3 << 2) + require(memory[layout.base] != expected, "mutation escaped observation") + mutations += 1 + return {"invalid_inputs_rejected": rejected, "semantic_controls_rejected": mutations} + + +def receipt() -> dict: + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("fusion.py", "verify.py", "README.md", "TASK.json", + "SOURCES.json", "VERIFY.json")} + return {"status": "PASS_PACKED_TAPE_FUSION", "source_sha256": hashes, + "scalar_identity_cases": scalar_identity(), **program_cases(), + "dispatcher_fixture_instructions": dispatcher_fixture(), **controls(), + "read_instructions_per_tape": 13, "commit_instructions_per_tape": 4, + "access_instructions_per_tape": 17, + "predecessor_separate_access_instructions_per_tape": 30, + "claim_type": "scoped construction proof with finite corroboration"} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate source-bound receipt") + args = parser.parse_args() + result = receipt() + target = Path(__file__).resolve().with_name("RESULT.json") + if args.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + require(json.loads(target.read_text()) == result, "receipt differs from computed result") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()