From f7ecabe8e04738ee4fd6ac934363ca2c307d85b2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:34:29 +0000 Subject: [PATCH] feat(research): prove Walsh tape layout travel floors --- research/walsh-tape-cut-area/README.md | 264 ++++++++++++++++++++++ research/walsh-tape-cut-area/SOURCES.json | 18 ++ research/walsh-tape-cut-area/TASK.json | 96 ++++++++ research/walsh-tape-cut-area/VERIFY.json | 34 +++ research/walsh-tape-cut-area/verify.py | 240 ++++++++++++++++++++ 5 files changed, 652 insertions(+) create mode 100644 research/walsh-tape-cut-area/README.md create mode 100644 research/walsh-tape-cut-area/SOURCES.json create mode 100644 research/walsh-tape-cut-area/TASK.json create mode 100644 research/walsh-tape-cut-area/VERIFY.json create mode 100644 research/walsh-tape-cut-area/verify.py diff --git a/research/walsh-tape-cut-area/README.md b/research/walsh-tape-cut-area/README.md new file mode 100644 index 0000000000..574d233d00 --- /dev/null +++ b/research/walsh-tape-cut-area/README.md @@ -0,0 +1,264 @@ +# Exact spatial cut ranks for repeated Walsh transforms + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite corroboration.** +For a fixed linear program on one sequential tape, repeated Walsh transforms +have different unavoidable head-travel bills under two common data layouts. +For N Walsh addresses, m independent columns and one carried field register, +the proved lower bounds, in unit cell moves, are + +```text +address-major: (Nm)^2 / 2 +column-major: m N^2 / 2 + 2(m-1). +``` + +These are lower bounds, not attained minima. For N=8 and m=4 they are 512 +and 134. The underlying sums of directional communication ranks are 512 +and 128; the extra six column-major moves account for crossing the three +boundaries between whole columns and returning. A zero communication rank +at such a boundary does not make physical travel free. + +The new result is the exact pair of layout profiles and their complete +one-head travel conversion, including arbitrary positive register capacity. +The communication-rank argument is classical. This is a side result for the +`precision_tape` obligation, not a new supplier, κ or complete multiplication +theorem. The selected construction permits multiple tapes and is not excluded. + +## Machine and endpoint + +Let F be any field of characteristic other than two, N=2^h with h>=1, +m>=1, and s>=1. Let + +```text +H_N[a,b] = (-1)^(popcount(a & b)), 0 <= a,b < N. +``` + +The Nm independent input scalars occupy consecutive cells 0,...,Nm-1. +The endpoint replaces each column x[:,c] by H_N x[:,c] in those same cells. +Two physical encodings are compared: + +```text +address-major position(a,c) = a m + c, matrix H_N tensor I_m; +column-major position(a,c) = c N + a, matrix I_m tensor H_N. +``` + +There is one movable head and s carried field registers. At its current +cell it may apply any fixed F-linear operation to that cell and the +registers. It may move one cell at a time. Control, coefficients and the +entire address schedule are independent of input values. No other head, +remote-cell operation or source-dependent channel is available. Scratch +cells outside the data interval and the carried registers may start with +arbitrary independent dirt; any used scratch must be restored. The head +starts and finishes at cell zero. There is no requirement to preserve the +original data separately. + +This permits destructive local linear updates and arbitrary coefficients, +not merely a chosen butterfly gate list. It excludes nonlinear encodings +of several field values into one register, input-dependent control or head +positions, changed output placement and additional data tapes. The lower +bound does not charge local arithmetic, which can only add work. + +## General directional cut bound + +For any prescribed linear endpoint matrix M, cut the tape between q-1 and q. +Let L and R denote the data indices on its two sides. Write + +```text +r_left(q) = rank M[L,R], +r_right(q) = rank M[R,L]. +``` + +If the head crosses right to left c_left times and left to right c_right +times, then + +```text +s c_left >= r_left(q), s c_right >= r_right(q). +``` + +To prove the first inequality, keep only dependence on the initial right +input variables. All initial left cells and independent scratch then have +zero dependence. Every right-to-left crossing imports at most s linear +forms. Between such crossings, every left-side operation only takes linear +combinations of forms already available there. Outgoing messages cannot +enlarge this space. Consequently all final left outputs lie in the span of +at most s c_left imported forms. Their coefficient matrix is M[L,R]. The +other direction is identical after exchanging the roles of left and right. +Interaction, reuse, destructive updates and dirty scratch do not change +this span argument. The starting registers contain independent dirt, not +input-dependent information. + +Every cell must receive a nonidentity output for this Walsh endpoint. In +particular the head must reach the last cell. Since it returns to zero, +each internal data boundary is crossed at least once in each direction. +Thus the total number of unit moves obeys + +```text +moves >= sum(q=1..Nm-1) [max(1,ceil(r_left(q)/s)) + + max(1,ceil(r_right(q)/s))]. +``` + +A unit move crosses exactly one boundary. Extra visits outside the data +interval only increase the move count. The proof does not assume that all +cut demands are simultaneously attainable. + +## Exact Walsh cut profiles + +First consider a single H_N, cut after k coordinates. Both directional +ranks are min(k,N-k). For k<=N/2, the first k rows and the last N/2 columns +form the first k rows of H_(N/2), by the block recursion + +```text +H_N = [ H_(N/2) H_(N/2) ; H_(N/2) -H_(N/2) ]. +``` + +Those rows are independent because H_(N/2) is invertible. For k>=N/2, +take the first N/2 rows and the last N-k columns instead; these columns +of H_(N/2) are independent. The opposite block is the transpose, so it has +the same rank. The endpoint cases k=0,N have rank zero. Invertibility uses +H_N H_N^T = N I and the characteristic hypothesis. + +For address-major storage write q=km+r with 0<=r=N/2 it is Nm-km-r. +For column-major storage only the partly cut column can communicate across +the boundary. Whole columns have no endpoint dependence on other columns. +The rank in either direction is therefore + +```text +min(q mod N, N-(q mod N)). +``` + +These equalities give exact cut ranks for every h,m and every cut, not just +the finite fixtures below. + +## Register-dependent closed form + +For an even positive L define + +```text +F(a,s) = sum(j=1..a) ceil(j/s) + = s u(u+1)/2 + (u+1)v, a=us+v, 0<=v= B(Nm,s); +column-major moves >= m B(N,s) + 2(m-1). +``` + +For s=1, B(L,1)=L^2/2, giving the displayed bounds. Even without the +ceiling corrections, address-major storage forces at least (Nm)^2/(2s) +moves. With fixed N and s this excludes a travel bill linear in m for that +one-head layout. The column-major cut bound grows linearly in m. This does +not by itself construct a linear-in-m program or compare optimal runtimes. + +## Reproduce and finite evidence + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/walsh-tape-cut-area/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/walsh-tape-cut-area/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/walsh-tape-cut-area +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/walsh-tape-cut-area --check-source-history +``` + +Substitute another CPython 3.12 executable on another machine. Both registered +commands print `PASS_WALSH_TAPE_CUT_AREA`, counts and a generated SHA256-bound +receipt on stdout. Redirect logs outside the checkout; replay writes no files. + +The verifier constructs 32 literal integer endpoint matrices for N in +{2,4,8,16}, m in {1,2,3,4} and both layouts. Fraction elimination computes +both directional ranks at all 568 internal cuts. It independently sums those +ranks and the ceiling demands for seven register capacities, checking 224 +closed-form travel bounds. + +A separate local-gate interpreter executes 18 programs for N in {2,4,8}, +m in {1,2,3} and both layouts. Each butterfly borrows one arbitrary dirty +register: swap it with the first data cell, apply a two-variable Hadamard +at the second cell, then swap it back at the first. Independent initial +symbols verify every endpoint column and register restoration. The inverse +uses the reversed gate list and a half-Hadamard, and its full product is +checked. The programs execute 612 local gates and 2,358 enumerated unit +moves; 150 spatial cuts satisfy both directional demands. These programs +are feasibility controls, not optimal upper bounds. + +Eleven controls cover invalid dimensions, a wrong layout, a zero-rank +inter-column boundary, omitted inter-column travel, omitted dirty restoration, +a changed gate, register-capacity sensitivity and an unpaid remote shortcut. +The last control checks that a nonzero communication demand cannot have a +zero-move local realization; it does not execute a remote-operation machine. +Explicit exceptions keep the checks active under optimized Python. + +## Limits and engineering choices + +The all-size theorem is the written argument. Finite replay is corroboration, +not a formal proof. No production tape layout, complete native caller, +precision ledger, bit encoding or selected supplier is instantiated. Several +heads, extra data tapes, reordering or source-dependent side information can +change the obstruction. Field-operation and bit-operation models are distinct. +Independent human and formal proof-kernel review are unclaimed. + +The checker accepts no external data and caps matrices at 64 cells, its +local word at 4,096 gates, and the main census at fixed finite ranges. There +is no recursion or subprocess. Functions are below 60 lines. Python/Fraction +allocation is a managed-runtime deviation from fixed memory allocation, bounded +by these finite matrices and words. Warning-strict normal and optimized +execution provide the interpreter diagnostics. No global linter or repository +build setting is changed. + +## Sources, overlap and credit + +Base main is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The scope changes the `uniform-transfer-audit` card to an original restricted +backend obstruction; it does not purport to discharge the selected +`precision_tape` assumption. The selected source-binding positive control +passed before the investigation. No predecessor executable is imported or +replayed as the deliverable. [The advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226107) +states this question. + +Credit zxv's [PR #5441](https://github.com/CrocSwap/integer-mult-bounds/pull/5441) +for the distinction between fixed transfer representations and unpriced +physical movement, and ToikY's [PR #4192](https://github.com/CrocSwap/integer-mult-bounds/pull/4192) +for the distinct explicit sequential scan compiler. Their results are context, +not mathematical premises. Nick Petalas's #5148 studies stable lane passes; +its indivisible-record/tape-lane model and reversal question differ from the +one-head local linear machine and independent-column transforms here. This +is not a continuation of that result. + +Communication-based one-tape lower bounds are classical; see, for example, +[Dietzfelbinger's 1996 linear-array paper](https://eccc.weizmann.ac.il/eccc-reports/1996/TR96-063/index.html). +The linear-span proof above is self-contained. The Walsh matrix, Kronecker +products and rank subadditivity are background, not new general methods. +No global literature-priority claim is made. + +Entry overlap checking covered all 361 open PRs and 5,562 Discussion records +in the helper's reported complete remote pagination. The sparse local note +scan covered 205 of 8,136 tracked note paths; separate all-main README +searches covered the named layouts, Walsh/tape and cut-rank/head-travel terms, +and live merged searches were inspected. Recent account PRs and the local +claims were checked. This bounded, non-atomic search is not a novelty proof +and does not cover unpublished work or arbitrary diffs. + +## Open next questions + +1. Construct matching-order head-travel upper bounds in these exact layouts, + with scratch restoration and a literal schedule. This would determine + whether the layout-specific lower bounds describe the true order of + growth. Start by processing complete column programs consecutively; + finite butterfly feasibility alone does not establish the best schedule. +2. Bind one actual native caller's data layout and moving register budget to + this model, or identify the extra tape/head channel that escapes it. + This would decide applicability to production. Its data placement, + head motion and side information are not supplied here. diff --git a/research/walsh-tape-cut-area/SOURCES.json b/research/walsh-tape-cut-area/SOURCES.json new file mode 100644 index 0000000000..d596e2e530 --- /dev/null +++ b/research/walsh-tape-cut-area/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/walsh-tape-cut-area/TASK.json b/research/walsh-tape-cut-area/TASK.json new file mode 100644 index 0000000000..7736bbc18a --- /dev/null +++ b/research/walsh-tape-cut-area/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Original exact spatial cut-rank profiles and register-dependent one-head travel floors for independent Walsh columns in two physical layouts.", + "scope_change_reason": "Replaces a source-specific selected-assumption audit with a scoped obstruction for an explicitly restricted backend. No selected assumption is discharged.", + "bottleneck_link": "Side result for precision_tape: all-width algebraic correctness alone does not price layout-dependent sequential movement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved exact cut profiles and verified travel conversion; package without optimizing schedules or extending the machine model.", + "outcome": "completed", + "evidence": "README.md supplies the all-size linear-span and Walsh proofs; verify.py checks exact rational ranks and literal local dirty-register programs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What matching-order one-head schedules attain these layout-dependent travel floors?", + "why_it_matters": "Distinguishes an optimal growth obstruction from a cut lower bound.", + "first_step": "Process complete restored column programs consecutively and count every stage and inter-column move.", + "blocked_by": "No optimal schedule or upper-bound theorem is supplied." + }, + { + "question": "Which actual native caller satisfies or escapes the restricted machine contract?", + "why_it_matters": "Decides whether the obstruction affects a proposed physical lowering.", + "first_step": "Pin one caller layout, register budget and every extra head or tape channel.", + "blocked_by": "No production layout and movement binding is included." + } + ], + "validation_environment": { + "implementation": "CPython", + "version": "3.12.15", + "platform": "darwin", + "machine": "arm64", + "dependencies": "Python standard library only" + } +} diff --git a/research/walsh-tape-cut-area/VERIFY.json b/research/walsh-tape-cut-area/VERIFY.json new file mode 100644 index 0000000000..170a0d44b6 --- /dev/null +++ b/research/walsh-tape-cut-area/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All finite cut ranks, complete ceiling sums, literal local endpoints/inverses, dirty restoration, one-cell movement and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical evidence with optimization enabled; every check uses explicit exceptions." + } + ] +} diff --git a/research/walsh-tape-cut-area/verify.py b/research/walsh-tape-cut-area/verify.py new file mode 100644 index 0000000000..f78dcb5a46 --- /dev/null +++ b/research/walsh-tape-cut-area/verify.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the written one-head Walsh layout theorem.""" +from __future__ import annotations + +import hashlib +import json +from fractions import Fraction +from pathlib import Path + + +MAX_CELLS = 64 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def dimensions(n: int, columns: int) -> int: + require(type(n) is int and 2 <= n <= 32 and n & (n - 1) == 0, + 'n must be a power of two in [2,32]') + require(type(columns) is int and 1 <= columns <= 8, + 'columns must be in [1,8]') + require(n * columns <= MAX_CELLS, 'finite checker cell cap exceeded') + return n * columns + + +def index(address: int, column: int, n: int, columns: int, layout: str) -> int: + require(layout in ('address', 'column'), 'unknown layout') + return address * columns + column if layout == 'address' else column * n + address + + +def endpoint(n: int, columns: int, layout: str) -> list[list[int]]: + size = dimensions(n, columns) + matrix = [[0] * size for _ in range(size)] + for a in range(n): + for b in range(n): + sign = -1 if (a & b).bit_count() % 2 else 1 + for c in range(columns): + matrix[index(a, c, n, columns, layout)][index(b, c, n, columns, layout)] = sign + return matrix + + +def rank(matrix: list[list[int]]) -> int: + require(len(matrix) <= MAX_CELLS, 'rank row cap exceeded') + width = len(matrix[0]) if matrix else 0 + require(width <= MAX_CELLS and all(len(row) == width for row in matrix), + 'invalid rank matrix') + work = [[Fraction(value) for value in row] for row in matrix] + pivot = 0 + for column in range(width): + selected = next((i for i in range(pivot, len(work)) if work[i][column]), None) + if selected is None: + continue + work[pivot], work[selected] = work[selected], work[pivot] + divisor = work[pivot][column] + work[pivot] = [value / divisor for value in work[pivot]] + for row in range(pivot + 1, len(work)): + coefficient = work[row][column] + if coefficient: + work[row] = [a - coefficient * b for a, b in zip(work[row], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return pivot + + +def cut_ranks(matrix: list[list[int]], cut: int) -> tuple[int, int]: + size = len(matrix) + require(1 <= cut < size <= MAX_CELLS, 'cut outside finite matrix') + left_from_right = rank([row[cut:] for row in matrix[:cut]]) + right_from_left = rank([row[:cut] for row in matrix[cut:]]) + return left_from_right, right_from_left + + +def predicted_rank(n: int, columns: int, cut: int, layout: str) -> int: + size = dimensions(n, columns) + require(1 <= cut < size, 'cut outside finite matrix') + require(layout in ('address', 'column'), 'unknown layout') + if layout == 'address': + return min(cut, size - cut) + residual = cut % n + return min(residual, n - residual) + + +def ceil_sum(length: int, registers: int) -> int: + quotient, remainder = divmod(length, registers) + return registers * quotient * (quotient + 1) // 2 + (quotient + 1) * remainder + + +def single_block_bound(size: int, registers: int) -> int: + require(type(size) is int and size >= 2 and size % 2 == 0, 'even size required') + require(type(registers) is int and registers >= 1, 'positive registers required') + half = size // 2 + return 4 * ceil_sum(half - 1, registers) + 2 * ((half + registers - 1) // registers) + + +def travel_bound(n: int, columns: int, registers: int, layout: str) -> int: + size = dimensions(n, columns) + require(layout in ('address', 'column'), 'unknown layout') + if layout == 'address': + return single_block_bound(size, registers) + return columns * single_block_bound(n, registers) + 2 * (columns - 1) + + +def rank_census() -> dict[str, int]: + fixtures = cuts = bounds = 0 + for n in (2, 4, 8, 16): + for columns in (1, 2, 3, 4): + for layout in ('address', 'column'): + matrix = endpoint(n, columns, layout) + ranks = [] + for cut in range(1, len(matrix)): + expected = predicted_rank(n, columns, cut, layout) + require(cut_ranks(matrix, cut) == (expected, expected), 'cut rank formula') + ranks.append(expected) + cuts += 1 + for registers in (1, 2, 3, 5, 8, 16, 64): + enumerated = 2 * sum(max(1, (r + registers - 1) // registers) for r in ranks) + require(enumerated == travel_bound(n, columns, registers, layout), 'ceiling sum') + bounds += 1 + if layout == 'address': + require(2 * sum(ranks) == (n * columns) ** 2 // 2, 'address rank area') + else: + require(2 * sum(ranks) == columns * n * n // 2, 'column rank area') + fixtures += 1 + return dict(matrix_fixtures=fixtures, spatial_cuts=cuts, register_bounds=bounds) + + +def butterfly_word(n: int, columns: int, layout: str) -> list[tuple[int, str]]: + dimensions(n, columns) + word = [] + for stage in range(n.bit_length() - 1): + stride = 1 << stage + for base in range(0, n, 2 * stride): + for offset in range(stride): + for column in range(columns): + a = index(base + offset, column, n, columns, layout) + b = index(base + offset + stride, column, n, columns, layout) + word.extend(((a, 'swap'), (b, 'butterfly'), (a, 'swap'))) + require(len(word) == 3 * columns * (n // 2) * (n.bit_length() - 1), 'gate count') + return word + + +def execute(size: int, word: list[tuple[int, str]], inverse: bool = False) -> tuple[list[list[Fraction]], list[int], list[int]]: + require(2 <= size <= MAX_CELLS and len(word) <= 4096, 'execution cap exceeded') + rows = [[Fraction(i == j) for j in range(size + 1)] for i in range(size + 1)] + right = [0] * (size - 1) + left = [0] * (size - 1) + position = 0 + instructions = list(reversed(word)) if inverse else word + for location, gate in instructions: + require(0 <= location < size and gate in ('swap', 'butterfly'), 'invalid local gate') + step = 1 if location > position else -1 + for previous in range(position, location, step): + boundary = previous if step == 1 else previous - 1 + (right if step == 1 else left)[boundary] += 1 + position = location + cell, carried = rows[location], rows[size] + if gate == 'swap': + rows[location], rows[size] = carried, cell + else: + scale = Fraction(1, 2) if inverse else Fraction(1) + rows[size] = [scale * (a + b) for a, b in zip(carried, cell)] + rows[location] = [scale * (a - b) for a, b in zip(carried, cell)] + for previous in range(position, 0, -1): + left[previous - 1] += 1 + require(left == right, 'head return') + return rows, left, right + + +def literal_census() -> dict[str, int]: + programs = moves = gates = checks = 0 + for n in (2, 4, 8): + for columns in (1, 2, 3): + for layout in ('address', 'column'): + word = butterfly_word(n, columns, layout) + size = n * columns + result, left, right = execute(size, word) + expected = endpoint(n, columns, layout) + require(result[:size] == [row + [0] for row in expected], 'literal endpoint') + require(result[size] == [0] * size + [1], 'dirty register restoration') + backward, _, _ = execute(size, word, inverse=True) + for i in range(size + 1): + for j in range(size + 1): + require(sum(backward[i][k] * result[k][j] for k in range(size + 1)) == (i == j), 'literal inverse') + for cut in range(1, size): + demand = max(1, predicted_rank(n, columns, cut, layout)) + require(left[cut - 1] >= demand and right[cut - 1] >= demand, 'directional communication') + checks += 1 + require(sum(left) + sum(right) >= travel_bound(n, columns, 1, layout), 'total travel') + positions = [0] + [location for location, _ in word] + [0] + distance = sum(abs(a - b) for a, b in zip(positions, positions[1:])) + require(distance == sum(left) + sum(right), 'literal unit-move accounting') + programs += 1 + moves += distance + gates += len(word) + return dict(literal_programs=programs, local_gates=gates, unit_moves=moves, + directional_cut_checks=checks) + + +def controls() -> int: + requests = ((1, 1), (3, 1), (2, 0), (32, 8)) + for n, columns in requests: + rejected = False + try: + dimensions(n, columns) + except ValueError: + rejected = True + require(rejected, 'invalid dimension accepted') + matrix = endpoint(4, 3, 'column') + require(cut_ranks(matrix, 4) == (0, 0), 'whole-column boundary must have zero rank') + require(predicted_rank(4, 3, 4, 'address') != 0, 'layout mutation invisible') + require(travel_bound(4, 3, 1, 'column') == 28, 'inter-column travel cannot be free') + word = butterfly_word(2, 1, 'address') + altered, _, _ = execute(2, word[:-1]) + require(altered[2] != [0, 0, 1], 'omitted dirty restore undetected') + altered, _, _ = execute(2, [(p, 'swap') for p, _ in word]) + require(altered[:2] != [row + [0] for row in endpoint(2, 1, 'address')], 'wrong local gate') + require(single_block_bound(16, 2) < single_block_bound(16, 1), 'register budget ignored') + require(cut_ranks(endpoint(2, 1, 'address'), 1) == (1, 1), 'remote zero-travel shortcut') + return len(requests) + 7 + + +def main() -> None: + evidence = rank_census() + evidence.update(literal_census()) + evidence['controls'] = controls() + evidence['example_n8_m4_s1'] = dict(address=travel_bound(8, 4, 1, 'address'), + column=travel_bound(8, 4, 1, 'column')) + package = Path(__file__).resolve().parent + files = sorted(path for path in package.iterdir() if path.is_file()) + require(len(files) <= 16, 'package file cap exceeded') + evidence['sha256'] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() for path in files} + print('PASS_WALSH_TAPE_CUT_AREA') + print(json.dumps(evidence, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()