From eaea286b055724895adb4ca949b5ac0495be5ff8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:42:34 +0100 Subject: [PATCH] feat(research): prove optimal square-zero reflection compilation --- .../square-zero-idempotent-compiler/PROOF.md | 164 +++++++++ .../square-zero-idempotent-compiler/README.md | 117 +++++++ .../SOURCES.json | 24 ++ .../square-zero-idempotent-compiler/TASK.json | 69 ++++ .../VERIFY.json | 36 ++ .../square-zero-idempotent-compiler/verify.py | 324 ++++++++++++++++++ 6 files changed, 734 insertions(+) create mode 100644 research/square-zero-idempotent-compiler/PROOF.md create mode 100644 research/square-zero-idempotent-compiler/README.md create mode 100644 research/square-zero-idempotent-compiler/SOURCES.json create mode 100644 research/square-zero-idempotent-compiler/TASK.json create mode 100644 research/square-zero-idempotent-compiler/VERIFY.json create mode 100644 research/square-zero-idempotent-compiler/verify.py diff --git a/research/square-zero-idempotent-compiler/PROOF.md b/research/square-zero-idempotent-compiler/PROOF.md new file mode 100644 index 0000000000..7b14aa9c1f --- /dev/null +++ b/research/square-zero-idempotent-compiler/PROOF.md @@ -0,0 +1,164 @@ +# Exact projector-call cost of a square-zero coupling + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and boundary + +Let `N` be an `R x R` binary matrix with `N^2=0`, and put `q=rank(N)`. +Let `g` be a fixed nonidentity involution. Work in the full formal group +algebra `F2[C2]`, with `C2={1,g}`, and write `Q=1+[g]`. Thus `Q!=0` +and `Q^2=0`. The required full endpoint is + +``` +D_N = I + Q N. +``` + +All `R` input roles are arbitrary. A paid call is `I+Q P`, where `P=uv^T` +is a binary rank-one idempotent, equivalently `v^T u=1`. Arbitrary constant +binary invertible scalar maps may occur freely anywhere. Any finite number +of additional arbitrary dirty roles may be used, but they must be restored +with no residual couplings. On those enlarged roles the required endpoint +is `I+Q (N direct-sum 0)`. + +The exact minimum number of paid calls is zero when `q=0`. For `q>0` it is + +``` +L(q) = q+1, if q is odd; + q+2, if q is even. +``` + +Equivalently, it is the smallest even integer strictly greater than q. +No bound is placed on the original word length, finite workspace dimension +or placement of free scalar maps. Other address labels and clean or discarded +workspace are outside the theorem. + +The identity `product_j (I+Q A_j)=I+Q sum_j A_j` is inherited from +ywz65's [PR2716](https://github.com/CrocSwap/integer-mult-bounds/pull/2716). +That package implements each nilpotent rank-one term with two address calls. +The new result determines the exact cost of jointly compiling a square-zero +matrix of arbitrary rank into the original idempotent-call alphabet. + +## Remove free scalar maps + +For a constant invertible scalar matrix S, + +``` +S (I+Q P) = (I+Q S P S^-1) S. +``` + +Conjugation preserves binary rank-one idempotence. Move every free scalar +factor to the right. The complete word becomes a product of paid calls +followed by one scalar matrix S. Apply augmentation `[g] -> 1`: every paid +call and the required endpoint augment to I, so S=I. Consequently every legal +word gives + +``` +N direct-sum 0 = sum_(j=1)^L P_j. (1) +``` + +To read off this equality, compare the coefficient of the formal basis +element `[g]`. This uses `g!=1`. Conversely any such sum gives the entire +formal endpoint, since Q is central and Q^2=0. No nonfaithful representation +is used to certify endpoint equality. The normalization is the standard +register-model argument, not a new result claimed here. + +## Lower bound + +Equation (1) implies `L>=q` by rank subadditivity. Each binary rank-one +idempotent has trace one. A square-zero matrix has trace zero: for example, +`trace(N^2)=sum_i N_ii^2=trace(N)` over F2, since off-diagonal terms cancel +in pairs. Thus (1) also implies L is even. + +It remains to rule out L=q, even after arbitrary dirty padding. Suppose +`N direct-sum 0=UV`, where U has the q image columns u_j, V has the q +functional rows v_j, and every diagonal entry of VU is one. Since UV has +rank q, U has full column rank and V has full row rank. Choose a left +inverse A of U and a right inverse B of V. Square-zero gives + +``` +0 = A (UV)^2 B = VU, +``` + +contradicting those diagonal entries. Therefore L>q. Together with even +parity this proves `L>=L(q)`. Padding changes neither rank nor square-zero, +so this proof includes every finite restored dirty workspace. + +## Construction for odd rank + +First take the canonical square-zero matrix on 2q coordinates, + +``` +N = sum_(i=1)^q e_i f_i^T, +``` + +where the distinct coordinates e_i span its image and the coordinates f_i +are their chain preimages. Let `h=sum_i e_i^T`, a row functional supported +on the image coordinates, and let `u=sum_i e_i`. For odd q use the q+1 +rank-one matrices + +``` +P_i = e_i (h+f_i^T), for 1<=i<=q; +P_* = u h. +``` + +Every P_i is idempotent because `(h+f_i^T)e_i=1`. Also `h u=q=1` in F2, +so P_* is a nonzero rank-one idempotent. Their sum is N, since +`sum_i e_i h=u h` cancels P_*. Consequently the q+1 legal paid factors +have full product `I+Q N`. + +At q=3 this replaces six factorwise calls by four. In coordinate order +`e_1,e_2,e_3,f_1,f_2,f_3`, the factors are specified by + +``` +u_1=100000, v_1=111100; +u_2=010000, v_2=111010; +u_3=001000, v_3=111001; +u_*=111000, v_*=111000. +``` + +Here strings list coordinates left to right, rather than integer bit +significance. The two target blocks are arbitrary dirty inputs; the map is +`e_i <- e_i + (1+[g]) f_i`, with every f_i unchanged. + +## Even rank and arbitrary matrices + +For positive even q, split the q chains into blocks of sizes q-1 and one. +Both sizes are odd. Apply the preceding construction separately on the two +blocks. This uses `(q-1)+1 + 1+1=q+2` legal calls and gives their direct-sum +endpoint. Unused coordinates remain untouched. + +For any square-zero N, choose an image basis e_1,...,e_q and choose preimages +f_i with `N f_i=e_i`. Their 2q vectors are independent: applying N to a +linear dependence first kills all preimage coefficients, then independence +of the e_i kills the rest. Extend them to a basis by vectors in ker N. +This is possible because the image is contained in ker N. Thus N is +binary-similar to the canonical chains plus zeros. Conjugate every constructed +projector by that same binary basis. Rank-one idempotence and the complete +projector sum survive, and the number of paid calls stays L(q). + +These basis maps specify legal projector factors. They do not require clean +initial values or erase any initial role. If an implementation admits only a +coordinate reflection, each projector can be implemented by a scalar basis +change, one reflection, and the inverse scalar change, as in PR2716. Those +scalar operations must be separately charged in a physical comparison. + +## Scope of the improvement + +PR2716's factorwise construction uses 2q address calls for a rank-q +square-zero coupling. The new optimum saves `2q-L(q)` calls in the same +optimistic formal idempotent-call model. It first saves two at q=3. The +lower bound concerns one fixed involution label; extra address operations +may change it. It does not identify formal calls with recursive child rank. + +The result supplies neither a native reflection supplier nor a complete +scalar, frame, routing, precision, hosting, stock or tape invoice. No new +multiplication bound follows. The universal quantifiers rest on this written +proof. The finite shortest-path and full-operator checks are corroboration; +independent human and formal proof-kernel review are unclaimed. + +Credit ywz65/PR2716 for the arbitrary-coupling product and implementation +motivation; Adam Gall/PR1911 for the dihedral register context; eumemic/PR288, +Ali Romman/PR468, woklerx/PR1443, Gareth Davidson/PR1333 and the retained +register-model lineage. PR2716 also credits Arham Tahir/PR1589 and Cinna +Davis/PR2290 for enlarged-coupling precedents. No literature-priority claim +is made for matrix rank, trace, square-zero normal form or idempotent sums. diff --git a/research/square-zero-idempotent-compiler/README.md b/research/square-zero-idempotent-compiler/README.md new file mode 100644 index 0000000000..1fa5319015 --- /dev/null +++ b/research/square-zero-idempotent-compiler/README.md @@ -0,0 +1,117 @@ +# Exact square-zero coupling compilation + +This contribution was produced by Nick Petalas. + +A rank-q square-zero binary coupling can be implemented by exactly the +smallest even number of rank-one idempotent reflection calls greater than q. +The minimum is q+1 for odd q and q+2 for positive even q; the zero matrix +costs zero. This is a scoped algebraic proof with exact finite corroboration. + +For rank three the new joint construction uses four calls, improving the six +calls of the factorwise compiler in ywz65's merged +[PR2716](https://github.com/CrocSwap/integer-mult-bounds/pull/2716). +The first improvement is shipped here without extending the operation alphabet. + +The full endpoint is `I+(1+[g])N` over formal `F2[C2]`, with `N^2=0` and +one fixed nonidentity involution g. Each paid call has a binary rank-one +idempotent coupling. Free binary scalar mixing and any finite number of +restored arbitrary dirty roles are allowed. The matching lower bound applies +uniformly to all these dimensions. [PROOF.md](PROOF.md) gives the explicit +projectors, free-mixing normalization, parity obstruction and rank-saturation +obstruction. It proves the full formal identity, not only selected columns. + +## Evidence and reproduction + +From the repository root, use CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/square-zero-idempotent-compiler/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/square-zero-idempotent-compiler/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/square-zero-idempotent-compiler +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/square-zero-idempotent-compiler --check-source-history +``` + +Substitute another CPython 3.12 path outside this environment. Expected output +includes `PASS_SQUARE_ZERO_IDEMPOTENT_COMPILER rank3=4 previous=6 no_new_kappa`. +The verifier writes no files and emits a receipt bound to package and live +source hashes. No receipt is hand-written or inferred from a previous run. + +The exact checks enumerate all 66,066 binary matrices through four roles. +An independent additive shortest-path search computes their minimum number +of rank-one idempotent summands, without using the proposed compiler. All +343 square-zero matrices match the formula, including all 210 rank-two +matrices, each requiring four summands. The compiler then checks every one +of those 343 complete formal endpoints and 2,678 faithful regular-action +basis columns. Eight further conjugated fixtures cover ranks one through +eight with two restored dirty spectators, 176 regular columns and 48 +single-call omission controls. Four boundary controls reject non-square-zero +inputs, a noninvolutory-label substitution and dirty-input-only leakage. + +These bounded checks corroborate the all-rank proof; they do not derive an +unbounded theorem from finite enumeration. CPython 3.12.15 is the recorded +local interpreter. No predecessor executable or census was replayed. + +## Scope, overlap and limitations + +This changes the `bit-new-register-model` card to a compiler side question. +It does not meet the card's native-supplier gate. The historical first command +`scripts/research_baseline.py` fails with `KeyError: 'bit_lower'` under the +selected schema; the current `scripts/research_selected_baseline.py` passes +its metadata orientation. Neither is a scientific premise of this proof. + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [SOURCES.json](SOURCES.json) pins the inherited compiler README +and historical catalogue/selected context. [TASK.json](TASK.json) records the +changed scope and structured next question. The source README is cited and +authenticated, not offered as a verification deliverable. + +Initial overlap-helper coverage was 428 open PRs at 23:37 UTC and 3,964 +Discussion records at 23:38 UTC on October 22, 2026, with complete remote +pagination. Sparse local coverage was incomplete, so separate `git grep` +searches over main's full README tree and merged-PR searches covered +`square-zero`, `nilpotent`, `idempotent`, compilation and decomposition terms. +The finite-dihedral extension was discarded because David Arias's merged +PR2738 already covers arbitrary couplings. No-match searches do not establish +novelty, and unpublished work remains outside coverage. + +Scalar basis conversion costs, native reflection implementation, recursive +child pricing, physical routing/hosting/precision/tape/stock and a complete +multiplication theorem remain unestablished. The four-call result alone does +not assert a better total physical bill or new kappa. The lower bound excludes +other address labels, clean/discarded workspace and nonconstant free maps. +Independent human and formal proof-kernel review are unclaimed. Lean, Docker +and the selected full cold replay were not run. + +The verifier uses Python-managed allocations, a Power of Ten rule-3 deviation. +Its enforced maximum width is 20; the largest shortest-path state space is +65,536 binary matrices with 120 possible moves per state. Every loop has a +finite bound, functions are below 60 physical lines, and explicit exceptions +keep checks active under optimization. It uses no recursion, dynamic code, +external solver or subprocess. Both registered checks treat warnings as errors. + +## Related open work + +The title/body searches before publication found no open PR claiming this +square-zero-to-idempotent compilation minimum. Open PR4849 studies the +UT3(F4) central-target floor after admitting nilpotent calls. Its group, +endpoint and paid alphabet differ; it does not determine this fixed-involution +compiler cost. No numerical comparison or predecessor replay is asserted. + +## Open next questions + +Can this joint compiler improve a fully charged native boundary? Fix one +literal caller with a rank-three square-zero coupling and compare the four-call +construction with the six-call factorwise implementation, including every +scalar basis conversion, frame and movement cost. A native reflection contract +and complete physical invoice are the blockers. The structured question is in +[TASK.json](TASK.json). + +## Credit + +Credit ywz65/PR2716 for the arbitrary-coupling identity and factorwise dirty +compiler, and Adam Gall/PR1911 for the register context. The retained lineage +includes eumemic/PR288, Ali Romman/PR468, woklerx/PR1443, Gareth Davidson/PR1333, +Arham Tahir/PR1589 and Cinna Davis/PR2290. The new repository contribution is +the sharp joint compilation count and matching construction. No priority claim +is made for elementary idempotent-sum or square-zero matrix facts. New work is +Apache-2.0. diff --git a/research/square-zero-idempotent-compiler/SOURCES.json b/research/square-zero-idempotent-compiler/SOURCES.json new file mode 100644 index 0000000000..62df6a8998 --- /dev/null +++ b/research/square-zero-idempotent-compiler/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/dihedral-arbitrary-couplings/README.md", + "usage": "input", + "git_blob": "66027d2a8856d931e7b1c8fa9811a65196d01637", + "sha256": "17bc49fd6215c155aacb0e4a8ce4a8e33e83226b8a1b937a638256a39b99f8ee" + } + ] +} diff --git a/research/square-zero-idempotent-compiler/TASK.json b/research/square-zero-idempotent-compiler/TASK.json new file mode 100644 index 0000000000..6b35fd433d --- /dev/null +++ b/research/square-zero-idempotent-compiler/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum rank-one idempotent reflection calls for a square-zero binary coupling of any rank, with free scalar mixing and arbitrary restored dirty workspace.", + "scope_change_reason": "Replace a new nonabelian supplier search by the missing joint implementation cost of the enlarged coupling alphabet in ywz65 PR2716. This is a scoped algebraic compiler result.", + "bottleneck_link": "Joint compilation removes reflection invocations relative to per-factor compilation. Scalar basis costs and native recursive admission remain separate; no exponent saving follows.", + "budget_minutes": 60, + "stop_rule": "Stop after proving and exactly corroborating the first strict call-count improvement at rank three.", + "outcome": "completed", + "evidence": "PROOF.md gives a uniform matching lower bound and construction. verify.py checks new complete binary-matrix domains and full arbitrary-input formal endpoints.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this joint compiler reduce a fully charged native supplier boundary?", + "why_it_matters": "Fewer reflection invocations alone do not price scalar encoding and routing.", + "first_step": "Fix a literal caller with a rank-three square-zero coupling and compare its four-call compiler with the six-call factorwise implementation, charging every scalar basis conversion.", + "blocked_by": "No native reflection supplier contract, physical caller or complete invoice is supplied." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit" + } +} diff --git a/research/square-zero-idempotent-compiler/VERIFY.json b/research/square-zero-idempotent-compiler/VERIFY.json new file mode 100644 index 0000000000..926309d0bf --- /dev/null +++ b/research/square-zero-idempotent-compiler/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dihedral-arbitrary-couplings/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Uniform-construction corroboration, exact additive shortest paths, full formal endpoints, dirty-input regular action and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks with assertions disabled." + } + ] +} diff --git a/research/square-zero-idempotent-compiler/verify.py b/research/square-zero-idempotent-compiler/verify.py new file mode 100644 index 0000000000..28273e45bf --- /dev/null +++ b/research/square-zero-idempotent-compiler/verify.py @@ -0,0 +1,324 @@ +"""Exact square-zero compiler checks; standard library, no generated files. + +Produced by Nick Petalas. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path + + +MAX_WIDTH = 20 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def rank(rows): + pivots = {} + for original in rows: + value = original + for bit in range(MAX_WIDTH * 2 - 1, -1, -1): + if value & (1 << bit): + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def multiply(a, b): + n = len(a) + require(len(b) == n <= MAX_WIDTH * 2, 'matrix width') + return tuple(xor_selected(row, b) for row in a) + + +def xor_selected(mask, vectors): + value = 0 + for i, vector in enumerate(vectors): + if mask & (1 << i): + value ^= vector + return value + + +def columns(rows): + n = len(rows) + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(rows)) + for j in range(n)) + + +def inverse(rows): + n = len(rows) + work = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for j in range(n): + pivot = next((i for i in range(j, n) if work[i] & (1 << j)), None) + require(pivot is not None, 'singular basis') + work[j], work[pivot] = work[pivot], work[j] + for i in range(n): + if i != j and work[i] & (1 << j): + work[i] ^= work[j] + require(tuple(row & ((1 << n) - 1) for row in work) == identity(n), + 'inverse elimination') + return tuple(row >> n for row in work) + + +def coordinates(vector, basis): + work = [(value, 1 << i) for i, value in enumerate(basis)] + pivots = {} + for value, label in work: + for bit in range(MAX_WIDTH - 1, -1, -1): + if value & (1 << bit): + if bit in pivots: + other, coefficient = pivots[bit] + value ^= other + label ^= coefficient + else: + pivots[bit] = (value, label) + break + result = 0 + for bit in range(MAX_WIDTH - 1, -1, -1): + if vector & (1 << bit): + require(bit in pivots, 'outside image span') + value, label = pivots[bit] + vector ^= value + result ^= label + require(vector == 0, 'coordinate residual') + return result + + +def jordan_basis(matrix): + n = len(matrix) + image, preimages = [], [] + cols = columns(matrix) + for j, vector in enumerate(cols): + if rank(image + [vector]) > len(image): + image.append(vector) + preimages.append(1 << j) + q = len(image) + basis = image + preimages + require(rank(basis) == 2 * q, 'Jordan chain independence') + for j, vector in enumerate(cols): + kernel = (1 << j) ^ xor_selected(coordinates(vector, image), preimages) + if rank(basis + [kernel]) > len(basis): + basis.append(kernel) + require(len(basis) == n, 'Jordan basis completeness') + change = columns(tuple(basis)) + undo = inverse(change) + canonical = tuple((1 << (q + i)) if i < q else 0 for i in range(n)) + require(multiply(multiply(undo, matrix), change) == canonical, + 'Jordan conjugation') + return q, change, undo + + +def outer(u, v, n): + return tuple(v if u & (1 << i) else 0 for i in range(n)) + + +def canonical_projectors(q, n): + groups = [tuple(range(q))] if q % 2 else [tuple(range(q - 1)), (q - 1,)] + result = [] + for group in groups: + functional = sum(1 << i for i in group) + for i in group: + result.append(outer(1 << i, functional ^ (1 << (q + i)), n)) + result.append(outer(functional, functional, n)) + return result + + +def compile_matrix(matrix): + n = len(matrix) + require(1 <= n <= MAX_WIDTH and all(0 <= row < (1 << n) for row in matrix), + 'binary matrix boundary') + require(not any(multiply(matrix, matrix)), 'coupling must be square-zero') + if not any(matrix): + return [] + q, change, undo = jordan_basis(matrix) + result = [multiply(multiply(change, p), undo) + for p in canonical_projectors(q, n)] + require(len(result) == q + 1 + (q % 2 == 0), 'optimal length') + total = (0,) * n + for projector in result: + require(rank(projector) == 1 and multiply(projector, projector) == projector, + 'legal rank-one projector') + total = add(total, projector) + require(total == matrix, 'projector sum') + return result + + +def formal_product(projectors, n): + zero = (0,) * n + a, b = identity(n), zero + for p in projectors: + c = add(identity(n), p) + a, b = add(multiply(c, a), multiply(p, b)), add(multiply(p, a), multiply(c, b)) + return a, b + + +def regular_action(projectors, n, period=2): + """Literal address rotation, using neither formal convolution nor its output.""" + result = [] + mask = (1 << period) - 1 + for column in range(n * period): + state = [0] * n + state[column // period] = 1 << (column % period) + for p in projectors: + read = [xor_selected(row, state) for row in p] + for i in range(n): + rotated = ((read[i] << 1) & mask) | (read[i] >> (period - 1)) + state[i] ^= read[i] ^ rotated + result.append(tuple(state)) + return tuple(result) + + +def desired_action(matrix, period=2): + n = len(matrix) + result = [] + for column in range(n * period): + role, address = divmod(column, period) + state = [0] * n + state[role] = 1 << address + for i, row in enumerate(matrix): + if row & (1 << role): + state[i] ^= (1 << address) ^ (1 << ((address + 1) % period)) + result.append(tuple(state)) + return tuple(result) + + +def unpack(value, n): + return tuple((value >> (n * i)) & ((1 << n) - 1) for i in range(n)) + + +def pack(rows): + n = len(rows) + return sum(row << (n * i) for i, row in enumerate(rows)) + + +def shortest_sums(n): + size = 1 << (n * n) + projectors = sorted({pack(outer(u, v, n)) for u in range(1, 1 << n) + for v in range(1, 1 << n) if (u & v).bit_count() % 2}) + distances = [-1] * size + distances[0] = 0 + queue = [0] + for index in range(size): + require(index < len(queue), 'projectors do not span matrix space') + value = queue[index] + for p in projectors: + target = value ^ p + if distances[target] < 0: + distances[target] = distances[value] + 1 + queue.append(target) + require(len(queue) == size, 'shortest-path coverage') + return distances + + +def exhaustive_checks(): + counts = {'binary_matrices': 0, 'square_zero': 0, 'rank_two_minimum_four': 0, + 'formal_endpoints': 0, 'regular_columns': 0} + for n in range(1, 5): + distances = shortest_sums(n) + for value, distance in enumerate(distances): + counts['binary_matrices'] += 1 + matrix = unpack(value, n) + if any(multiply(matrix, matrix)): + continue + q = rank(matrix) + expected = q + 1 + (q % 2 == 0) if q else 0 + require(distance == expected, 'independent shortest-sum minimum') + counts['square_zero'] += 1 + counts['rank_two_minimum_four'] += q == 2 and distance == 4 + projectors = compile_matrix(matrix) + require(formal_product(projectors, n) == (add(identity(n), matrix), matrix), + 'full formal endpoint') + require(regular_action(projectors, n) == desired_action(matrix), + 'regular arbitrary-input columns') + counts['formal_endpoints'] += 1 + counts['regular_columns'] += 2 * n + return counts + + +def larger_checks(): + counts = {'larger_endpoints': 0, 'larger_regular_columns': 0, 'omission_controls': 0} + for q in range(1, 9): + n = 2 * q + 2 + canonical = tuple((1 << (q + i)) if i < q else 0 for i in range(n)) + change = list(identity(n)) + for i in range(n): + change[i] ^= change[(i + 1) % n] + undo = inverse(tuple(change)) + matrix = multiply(multiply(tuple(change), canonical), undo) + projectors = compile_matrix(matrix) + require(formal_product(projectors, n) == (add(identity(n), matrix), matrix), + 'conjugated full formal endpoint') + require(regular_action(projectors, n) == desired_action(matrix), + 'conjugated full dirty action') + counts['larger_endpoints'] += 1 + counts['larger_regular_columns'] += 2 * n + for i in range(len(projectors)): + omitted = projectors[:i] + projectors[i + 1:] + require(formal_product(omitted, n) != (add(identity(n), matrix), matrix), + 'omitted reflection must fail') + counts['omission_controls'] += 1 + return counts + + +def boundary_controls(): + for bad in [(1,), (2, 1)]: + try: + compile_matrix(bad) + except ValueError: + pass + else: + raise ValueError('non-square-zero input accepted') + n, q = 8, 3 + matrix = tuple((1 << (q + i)) if i < q else 0 for i in range(n)) + projectors = compile_matrix(matrix) + require(len(projectors) == 4 < 2 * q, 'first strict improvement') + require(regular_action(projectors, n, 3) != desired_action(matrix, 3), + 'noninvolutory-label control') + mutant = list(matrix) + mutant[0] ^= 1 << (n - 1) + require(desired_action(tuple(mutant)) != desired_action(matrix), + 'dirty-input-only leakage') + return {'boundary_controls': 4, 'rank_three_calls': len(projectors), + 'rank_three_factorwise_calls': 2 * q} + + +def source_hashes(): + package = Path(__file__).resolve().parent + root = package.parent.parent + manifest = json.loads((package / 'SOURCES.json').read_text()) + hashes = {} + for item in manifest['files']: + if item['usage'] == 'input': + data = (root / item['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == item['sha256'], 'source SHA256') + blob = b'blob ' + str(len(data)).encode() + b'\0' + data + require(hashlib.sha1(blob).hexdigest() == item['git_blob'], 'source Git blob') + hashes[item['path']] = item['sha256'] + for path in sorted(package.iterdir()): + if path.is_file(): + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + hashes = source_hashes() + result = exhaustive_checks() | larger_checks() | boundary_controls() + result['file_sha256'] = hashes + print(json.dumps(result, sort_keys=True)) + print('PASS_SQUARE_ZERO_IDEMPOTENT_COMPILER rank3=4 previous=6 no_new_kappa') + + +if __name__ == '__main__': + main()