From e8832b7fd18458ff82a96e2c9a061e9df66943cc Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 09:11:38 +0000 Subject: [PATCH] feat(research): share paired samplers in 21 canonical tables --- research/signed-swap-residue-bank/PROOF.md | 128 ++++++++++++ research/signed-swap-residue-bank/README.md | 107 ++++++++++ .../signed-swap-residue-bank/SOURCES.json | 30 +++ research/signed-swap-residue-bank/TASK.json | 103 ++++++++++ research/signed-swap-residue-bank/VERIFY.json | 37 ++++ research/signed-swap-residue-bank/bank.py | 89 ++++++++ research/signed-swap-residue-bank/verify.py | 193 ++++++++++++++++++ 7 files changed, 687 insertions(+) create mode 100644 research/signed-swap-residue-bank/PROOF.md create mode 100644 research/signed-swap-residue-bank/README.md create mode 100644 research/signed-swap-residue-bank/SOURCES.json create mode 100644 research/signed-swap-residue-bank/TASK.json create mode 100644 research/signed-swap-residue-bank/VERIFY.json create mode 100644 research/signed-swap-residue-bank/bank.py create mode 100644 research/signed-swap-residue-bank/verify.py diff --git a/research/signed-swap-residue-bank/PROOF.md b/research/signed-swap-residue-bank/PROOF.md new file mode 100644 index 0000000000..e79b627806 --- /dev/null +++ b/research/signed-swap-residue-bank/PROOF.md @@ -0,0 +1,128 @@ +# A smaller forward bank by signed exchange + +## Contract and cited input + +Let `1 <= a,b <= 12`. The caller supplies both residues before drawing coins. +It requests two independent Bernoulli outputs with parameters `a/13,b/13`. +Coins are independent fair bits, with no free initial random state. + +zxv's [#6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072) +supplies the following input theorem. Its fixed-parameter dyadic decision graph +returns labels `00,01,10,11` with weights + +``` +w(a,b) = ((13-a)(13-b), (13-a)b, a(13-b), ab), denominator 169. +``` + +At every depth `k`, the number of completed label-`i` binary prefixes is +`floor(2^k w_i/169)`. This saturates the fair-prefix lower bound and attains the +optimal expected draw count. Its periodic representation has 312 pending states +and four terminal labels, hence 624 nine-bit targets, or 702 bytes. These are +cited predecessor results. The present verification does not rerun its law, +mean catalogue or optimality verifier. + +The new contract permits changing which output a particular coin tape returns. +It retains the requested joint law and, as shown below, the original stopping +time on every coin tape. It is a forward logical contract only. + +## Theorem + +All 144 requested pairs can be served from 21 unchanged canonical source tables, +a 144-byte selector and fixed output logic. Their transition and selector payload +is exactly 14,886 bytes. The resulting sampler has the requested independent +product law, the cited optimal expected draw count, and the original first +stopping depth on every finite or infinite coin tape. + +This is a constructive upper bound. No global minimum ROM size, physical tariff +or reversible implementation is asserted. + +## Canonicalization and the output map + +Put `c=min(a,13-a)`, `d=min(b,13-b)`, and let `u=min(c,d)`, `v=max(c,d)`. +The representatives are exactly `(u,v)` with `1 <= u <= v <= 6`. There are +`6+5+4+3+2+1=21`. Independent complements give four pairs on each diagonal +representative; complement and exchange give eight on each off-diagonal one. +Thus the orbit sizes are six fours and fifteen eights, totaling 144 pairs. +These are precisely the orbits under these specified operations, not a minimum +number of tables under arbitrary sampler redesigns. + +Draw `(U,V)` from the canonical `(u,v)` source table. Exchange its coordinates +when `c>d`, then complement its first coordinate when `a>6` and its second when +`b>6`. Call this bijection `F`. Independent complements and exchange preserve +independence and give the two required parameters. More explicitly, + +``` +w(a,b)[F(i)] = w(u,v)[i] for i=0,1,2,3. +``` + +For each depth `k`, relabelled completed prefix counts therefore equal +`floor(2^k w(a,b)[j]/169)` for every requested label `j`. This proves the full +joint law and transfers the cited depth-optimal expected-bit bound. It uses no +floating point, finite draw cap or assumption about an actual inverse caller. + +## Pointwise stopping times + +Permuting the four weights preserves their residue sum at every binary phase. +It therefore preserves the pending-node counts `n_k` and the total number `D_k` +of terminal children at the next level. The literal source rule orders all +terminal children before the pending children. At node `j` with coin `t`, put +`l=2j+t`. If `l None: + if not condition: + raise ValueError(message) + + +def pair_index(a: int, b: int) -> int: + require(type(a) is int and type(b) is int, "integer residue pair") + require(1 <= a <= 12 and 1 <= b <= 12, "nonzero residue pair") + return (a - 1) * 12 + b - 1 + + +def selector(a: int, b: int) -> int: + _ = pair_index(a, b) # Validate the pair; its input index is not needed here. + left, right = min(a, 13 - a), min(b, 13 - b) + flags = 2 * int(a > 6) + int(b > 6) + if left > right: + left, right = right, left + flags += 4 + return 8 * REPRESENTATIVES.index((left, right)) + flags + + +def output_map(flags: int, output: int) -> int: + require(type(flags) is int and 0 <= flags < 8, "output flags") + require(type(output) is int and 0 <= output < 4, "output label") + left, right = output >> 1, output & 1 + if flags & 4: + left, right = right, left + return 2 * (left ^ ((flags >> 1) & 1)) + (right ^ (flags & 1)) + + +def pack(tables: tuple) -> bytes: + require(len(tables) == 21, "canonical table count") + payload = bytearray(BANK_BYTES) + for a in range(1, 13): + for b in range(1, 13): + payload[pair_index(a, b)] = selector(a, b) + for table_id, table in enumerate(tables): + require(len(table) == STATES, "source state count") + base = SELECTORS + table_id * TABLE_BYTES + for state, row in enumerate(table): + require(len(row) == 2, "binary transition row") + for coin, target in enumerate(row): + require(type(target) is int and 0 <= target < 316, "table target") + position = 9 * (2 * state + coin) + byte, shift = divmod(position, 8) + word = target << shift + payload[base + byte] |= word & 255 + payload[base + byte + 1] |= word >> 8 + return bytes(payload) + + +def transition(payload: bytes, code: int, state: int, coin: int) -> int: + require(type(payload) is bytes and len(payload) == BANK_BYTES, "bank length") + require(type(code) is int and 0 <= code < 168, "selector code") + require(type(state) is int and 0 <= state < STATES, "pending state") + require(type(coin) is int and coin in (0, 1), "binary coin") + table_id, flags = divmod(code, 8) + byte, shift = divmod(9 * (2 * state + coin), 8) + offset = SELECTORS + table_id * TABLE_BYTES + byte + target = ((payload[offset] | (payload[offset + 1] << 8)) >> shift) & 511 + require(target < 316, "packed target") + if target >= STATES: + return STATES + output_map(flags, target - STATES) + return target + + +def run(payload: bytes, a: int, b: int, coins: tuple) -> tuple: + index = pair_index(a, b) + require(type(payload) is bytes and len(payload) == BANK_BYTES, "bank length") + require(type(coins) is tuple and len(coins) <= 4096, "finite tape limit") + require(all(type(coin) is int and coin in (0, 1) for coin in coins), "binary tape") + state, code = 0, payload[index] + for used, coin in enumerate(coins, 1): + state = transition(payload, code, state, coin) + if state >= STATES: + return state - STATES, used + return None, len(coins) diff --git a/research/signed-swap-residue-bank/verify.py b/research/signed-swap-residue-bank/verify.py new file mode 100644 index 0000000000..25484c96b3 --- /dev/null +++ b/research/signed-swap-residue-bank/verify.py @@ -0,0 +1,193 @@ +"""Verify the new selector, packed bank and relabelled paths. Apache-2.0.""" + +import argparse +from collections import Counter, deque +import hashlib +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from bank import (BANK_BYTES, REPRESENTATIVES, SELECTORS, STATES, TABLE_BYTES, + output_map, pack, pair_index, require, run, selector, transition) + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MAPS = ((0, 1, 2, 3), (1, 0, 3, 2), (2, 3, 0, 1), (3, 2, 1, 0), + (0, 2, 1, 3), (1, 3, 0, 2), (2, 0, 3, 1), (3, 1, 2, 0)) + + +def source_tables() -> tuple: + """Load authenticated source bytes, bypassing any bytecode cache. + + This fixed, hash-bound module load is the only dynamic-code exception. + Only make() is called; the predecessor's main verifier is never called. + """ + manifest = json.loads((HERE / "SOURCES.json").read_text()) + source = ROOT / "research/paired-residue-sampler/verify.py" + authenticated = {} + for row in manifest["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "source hash") + authenticated[row["path"]] = raw + namespace = {"__file__": str(source), "__name__": "paired_source"} + raw = authenticated["research/paired-residue-sampler/verify.py"] + exec(compile(raw, str(source), "exec"), namespace) + # The inherited weights, depth counts and exact means are not audit targets. + return tuple(namespace["make"](a, b)[2] for a, b in REPRESENTATIVES) + + +def weights(a: int, b: int) -> tuple: + return ((13 - a) * (13 - b), (13 - a) * b, a * (13 - b), a * b) + + +def validate(payload: bytes, tables: tuple) -> dict: + require(type(payload) is bytes and len(payload) == BANK_BYTES, "bank length") + orbits = Counter() + edges = 0 + for a in range(1, 13): + for b in range(1, 13): + code = payload[pair_index(a, b)] + require(code < 168, "selector code") + table_id, flags = divmod(code, 8) + representative = REPRESENTATIVES[table_id] + mapped = [0] * 4 + for label, weight in enumerate(weights(*representative)): + mapped[MAPS[flags][label]] = weight + require(output_map(flags, label) == MAPS[flags][label], "output map") + require(tuple(mapped) == weights(a, b), "selector product law") + orbits[representative] += 1 + for state, row in enumerate(tables[table_id]): + for coin, target in enumerate(row): + expected = target if target < STATES else STATES + MAPS[flags][target - STATES] + require(transition(payload, code, state, coin) == expected, "packed edge") + edges += 1 + require(len(orbits) == 21, "all canonical tables used") + require(Counter(orbits.values()) == {4: 6, 8: 15}, "signed-exchange orbits") + return {"selectors": SELECTORS, "canonical_tables": 21, "checked_edges": edges, + "orbit_size_histogram": {str(k): v for k, v in sorted(Counter(orbits.values()).items())}} + + +def leaf_paths(table: tuple) -> tuple: + """Shortest terminating fixtures. The queue visits at most 312 states.""" + paths = {0: ()} + queue = deque([0]) + leaves = {} + for _ in range(STATES): + if not queue: + break + state = queue.popleft() + for coin, target in enumerate(table[state]): + path = paths[state] + (coin,) + if target >= STATES: + leaves.setdefault(target - STATES, path) + elif target not in paths: + paths[target] = path + queue.append(target) + require(not queue and len(leaves) == 4, "complete fixture traversal") + return tuple(leaves[label] for label in range(4)) + + +def path_checks(payload: bytes, tables: tuple) -> dict: + fixtures = tuple(leaf_paths(table) for table in tables) + cases = 0 + for a in range(1, 13): + for b in range(1, 13): + code = payload[pair_index(a, b)] + table_id, flags = divmod(code, 8) + for label, path in enumerate(fixtures[table_id]): + expected = (MAPS[flags][label], len(path)) + require(run(payload, a, b, path + (0, 1, 0)) == expected, "first stop and label") + require(run(payload, a, b, path[:-1]) == (None, len(path) - 1), "unfinished prefix") + cases += 1 + require(run(payload, a, b, (1,) * 312) == (None, 312), "phase-wrap continuation") + # A seven-step literal source rule illustrates the changed coin-to-label contract. + tape = (1, 1, 1, 1, 1, 0, 0) + residues, node, original = weights(12, 2), 0, None + for used, coin in enumerate(tape, 1): + node = 2 * node + coin + for label, residue in enumerate(residues): + node -= 2 * residue // 169 + if node < 0: + original = label, used + break + if original is not None: + break + residues = tuple(2 * residue % 169 for residue in residues) + require(original == (1, 7), "original label witness") + require(run(payload, 12, 2, tape) == (2, 7), "changed label witness") + return {"terminating_paths": cases, "unfinished_prefixes": cases, + "two_period_continuations": 144, + "changed_function_witness": {"pair": [12, 2], "tape": "1111100", + "original_label": 1, "bank_label": 2, "stopping_depth": 7}} + + +def rejected(operation, reason: str) -> None: + try: + operation() + except ValueError as error: + require(str(error) == reason, "wrong rejection reason") + return + raise ValueError("negative control accepted") + + +def negative_checks(payload: bytes, tables: tuple) -> int: + for a, b in ((0, 1), (13, 1), (True, 1), (1.0, 2)): + reason = "integer residue pair" if type(a) is not int else "nonzero residue pair" + rejected(lambda: selector(a, b), reason) + for flag in (1, 2, 4): + altered = bytearray(payload) + altered[pair_index(1, 2)] ^= flag + rejected(lambda: validate(bytes(altered), tables), "selector product law") + altered = bytearray(payload) + altered[0] = 255 + rejected(lambda: validate(bytes(altered), tables), "selector code") + altered = bytearray(payload) + altered[SELECTORS] ^= 1 + rejected(lambda: validate(bytes(altered), tables), "packed edge") + rejected(lambda: validate(payload[:-1], tables), "bank length") + rejected(lambda: transition(payload, 0, STATES, 0), "pending state") + rejected(lambda: transition(payload, 0, 0, True), "binary coin") + rejected(lambda: run(payload, 1, 1, (0, 2)), "binary tape") + rejected(lambda: run(payload, 1, 1, (1,) * 4097), "finite tape limit") + altered = bytearray(payload) + altered[SELECTORS] = 255 + altered[SELECTORS + 1] |= 1 + rejected(lambda: transition(bytes(altered), 0, 0, 0), "packed target") + return 15 + + +def outside_output(path: str, data: bytes) -> None: + target = Path(path).expanduser().resolve() + require(not target.is_relative_to(ROOT), "output must be outside checkout") + require(target.parent.is_dir(), "output parent exists") + require(target.write_bytes(data) == len(data), "complete output write") + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-bank") + parser.add_argument("--receipt") + args = parser.parse_args() + tables = source_tables() + payload = pack(tables) + result = {"status": "PASS_SIGNED_SWAP_RESIDUE_BANK", **validate(payload, tables), + **path_checks(payload, tables), "rejection_controls": negative_checks(payload, tables), + "bank_bytes": len(payload), "transition_bytes": 21 * TABLE_BYTES, + "bank_sha256": hashlib.sha256(payload).hexdigest(), + "scope": "new forward logical bank; inherited DDG law and optimum; no physical tariff or kappa"} + result["package_sha256"] = { + path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.iterdir()) if path.is_file() + } + if args.emit_bank: + outside_output(args.emit_bank, payload) + encoded = (json.dumps(result, indent=2, sort_keys=True) + "\n").encode() + if args.receipt: + outside_output(args.receipt, encoded) + print(encoded.decode(), end="") + + +if __name__ == "__main__": + main()