From fc09e5b783989d769e6ae6fffeb7d23b30177c86 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:03:02 +0100 Subject: [PATCH] feat(research): classify shortest binary depth-six chain schedules --- research/depth6-binary-chain/README.md | 182 ++++++++++++++++ research/depth6-binary-chain/RESULT.json | 43 ++++ research/depth6-binary-chain/SOURCES.json | 30 +++ research/depth6-binary-chain/TASK.json | 99 +++++++++ research/depth6-binary-chain/VERIFY.json | 37 ++++ research/depth6-binary-chain/verify.py | 252 ++++++++++++++++++++++ 6 files changed, 643 insertions(+) create mode 100644 research/depth6-binary-chain/README.md create mode 100644 research/depth6-binary-chain/RESULT.json create mode 100644 research/depth6-binary-chain/SOURCES.json create mode 100644 research/depth6-binary-chain/TASK.json create mode 100644 research/depth6-binary-chain/VERIFY.json create mode 100644 research/depth6-binary-chain/verify.py diff --git a/research/depth6-binary-chain/README.md b/research/depth6-binary-chain/README.md new file mode 100644 index 0000000000..33662ab27a --- /dev/null +++ b/research/depth6-binary-chain/README.md @@ -0,0 +1,182 @@ +# Exactly ten shortest binary depth-six chain schedules + +This contribution was produced by Nick Petalas. The new result is an +**exhaustive finite classification** of shortest unsigned dirty-chain +schedules at depth six in characteristic two: + +```text +There are exactly ten shortest words. +They are the ten distinct cyclic rotations of (1234565432)^2. +None has adjacent commuting calls. +``` + +The length 20 is already implied by Yifan Kang's +[CNOT-Optimal Circuit Synthesis, Proposition 3.1](https://math.mit.edu/documents/rsi/2023KangY.pdf), +which proves the directed-path minimum `4n-8` on n registers. It is credited +prior work, not the original result here. The new classification shows that +this minimal interface has only cyclic starting-position freedom. No local +swap of commuting neighbors can retime a shortest schedule. + +## Interface and algebraic reduction + +A letter l means the complete call `z_l += B_l z_(l-1)`, for l = 1,...,6. +The source `x = z_0` is immutable. The five intermediates `z_1,...,z_5` and +the target `y = z_6` hold arbitrary initial data. The maps `B_1,...,B_6` are +arbitrary compatible linear maps over a nonzero unital ring of +characteristic two. Every intermediate must be restored, and the only +output change must be + +```text +y += B_6 B_5 B_4 B_3 B_2 B_1 x. +``` + +There are no inverse, fused, scaling, copy or extra-storage calls. Length +counts complete calls with equal unit prices. This is the chain model of +[#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263) and +[#4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281), with one +additional stage. This package provides no new kappa or supplier admission. + +Use #4281's interval-count reduction. For `1 <= i <= j <= 6`, let `N[i..j]` +count scattered copies of `i(i+1)...j` in the chronological word. The +coefficient of the initial `z_(i-1)` in the final `z_j` is + +```text +N[i..j] B_j B_(j-1) ... B_i. +``` + +Induction on calls proves this formula without commuting maps. The word is +universally correct precisely when `N[1..6]` is odd and every other interval +count is even. The expansion proves sufficiency. For necessity, take all +maps to be identity and vary the initial registers independently over F2. +Any wrong interval coefficient changes a wrong register or source +coefficient. + +Equivalently, multiply the adjacent transvections `g_l = I + e_(l-1,l)` +chronologically in `UT7(F2)`. Their strict upper-triangular coordinates are +exactly the interval parities. The target is `I + e_(0,6)`. Thus universally +correct shortest schedules are exactly the labelled shortest paths to this +target in a graph of `2^21 = 2,097,152` possible states. Arbitrary-map +correctness does not require the actual maps to commute. + +## Complete shortest-path classification + +[RESULT.json](RESULT.json) lists all ten words, the exact path count, the +minimum distance and every BFS layer size through level 20. The verifier +starts only at identity and applies all six generators to every state in +each layer. It uses no symmetry or interval-based pruning. A visited array +removes only states reached at no greater distance. + +The target is absent in layers 0 through 19, which contain **1,197,817 +distinct states**, and first appears at level 20. The full layer 20 has +**338,668** states. These are states, not word counts; later group states are +not explored. + +The new counting step keeps `ways[s]`, the exact number of shortest labelled +paths to state s. Initially only identity has count one. Every edge from +level d-1 to level d contributes its source count, including edges to a +state already discovered in that same level. Edges to earlier levels do +not contribute. Induction on d proves that this counts every shortest word +once. Counts fit in uint64 because `6^20 < 2^64`. The target count is **10**. + +A separate backward traversal starts at the target and follows every edge +that decreases the BFS distance. It uses full 7-by-7 matrix multiplication, +rather than the vectorized transition formula. An explicit bounded +worklist enumerates the ten actual words, independently agreeing with the +forward count. The sorted set equals the ten distinct cyclic rotations of + +```text +12345654321234565432 +``` + +Every word has call-count vector `(2,4,4,4,4,2)`. Every adjacent pair of +letters differs by one. As universal call operations, distinct chain +generators commute exactly when their indices differ by at least two, so +no shortest word permits a local commuting-neighbor swap. There is one +cyclic-rotation class and ten classes +under commuting-neighbor swaps. + +## Verification and reproduction + +The verifier checks each of the ten words by integer chronological subword +counts and by full binary matrix products. Across all ten words, it also +checks **81,920** scalar combinations of six binary maps and seven arbitrary +dirty values, plus **8,960** two-coordinate replays. The latter use fourteen +initial basis vectors for each of 64 deterministic map tuples per word, +including noncommuting and singular maps. The universal statement rests on +the algebraic reduction, not this finite map sample. + +A full-matrix oracle checks each generator on zero and all 21 coordinate +basis states, giving **132 comparisons**. Both transition formulas are +affine over F2, so these determine every transition on the whole state space. +Six rejection controls cover a dropped final call, dropped first call, +changed final call, unrestored forward-only word, swapped noncommuting +neighbors, and unknown generator. + +From the repository root, with CPython 3.12 and NumPy 2.5.4: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth6-binary-chain/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth6-binary-chain/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth6-binary-chain +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth6-binary-chain --check-source-history +``` + +Any CPython 3.12 interpreter with the declared NumPy version can replace the +local path. Both registered commands perform the complete count and path +enumeration. No opt-in mathematical replay is needed. The verifier writes +nothing. It prints a generated JSON receipt bound to every package file and +live input SHA-256, then + +```text +PASS_DEPTH6_BINARY_CHAIN shortest_words=10 rotation_classes=1 distance=20 oracle=132 scalar=81920 matrix=8960 controls=6 +``` + +## Limits + +This classifies only shortest depth-six schedules in characteristic two +under the stated complete-call alphabet. It does not classify longer words, +other characteristics or depths, extra storage, or a different target. +No universal multiplication barrier follows from this finite rigidity. + +BFS allocates fixed main buffers at initialization: a 2 MiB visited array, +a 16 MiB path-count array and two 8 MiB state arrays. Each temporary +transition processes at most `2^18` states. BFS has at most 20 levels, six +generators and eight chunks per generator. Backward enumeration has at most +20 levels, at most 100 retained paths and six predecessors per path. The +actual target has ten paths. No recursion, subprocess, network access or +file write occurs. Bounded Python/NumPy temporary allocation is a +managed-runtime deviation from fixed-allocation operation. Warning-strict +normal/optimized replays, the matrix oracle and explicit exception +contracts supply local diagnostics; no compiled-language type checker is used. + +No physical caller, routing, dispatch, precision, tape/storage, recursive +supplier or outer multiplication proof is supplied. Independent human and +formal proof-kernel review are unclaimed. + +## Open next questions + +1. Can a structural proof classify all shortest schedules without the + finite state search? Start with Kang's minimum count vector and derive + the forced chronological constraints. This could explain the rigidity + and determine whether it persists at other depths. +2. What is the least extra call budget that permits a nontrivial commuting + retiming freedom after cancelling adjacent equal calls? Begin with + length 22, since correct words have even length. This could quantify the + cost of chronology flexibility; a redundant cancelling pair alone would + not answer the question. +3. Does a fully paid supplier consumer use this six-stage composition? + Name actual maps and routing/restoration costs before interpreting the + abstract schedules as recursive savings. + +## Credit + +Yifan Kang supplies the known directed-path minimum and bridge construction +in Proposition 3.1. The original finite contribution here is the complete +ten-schedule classification and its retiming consequence. Nick Petalas's +#4249/#4263/#4281 supply the chain model, earlier depth results and +interval-count/UT reduction used here. Ryanson Jonathan's +[#4418](https://github.com/CrocSwap/integer-mult-bounds/pull/4418) settles +the separate eleven open depth-five residues. Those results are cited, not +re-audited. Ross Richardson's #943/#934 lineage supplies the complete-call +dirty-connector interface. BFS and shortest-path counting are classical +tools. Apache-2.0. diff --git a/research/depth6-binary-chain/RESULT.json b/research/depth6-binary-chain/RESULT.json new file mode 100644 index 0000000000..f26bb732f7 --- /dev/null +++ b/research/depth6-binary-chain/RESULT.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "claim_type": "exhaustive finite classification", + "bfs": { + "distance": 20, + "layers": [ + 1, + 6, + 20, + 54, + 131, + 296, + 635, + 1294, + 2528, + 4792, + 8774, + 15400, + 26054, + 42814, + 67969, + 102588, + 146231, + 199564, + 261330, + 317336, + 338668 + ], + "shortest_word_count": 10, + "words": [ + "12345654321234565432", + "21234565432123456543", + "23456543212345654321", + "32123456543212345654", + "34565432123456543212", + "43212345654321234565", + "45654321234565432123", + "54321234565432123456", + "56543212345654321234", + "65432123456543212345" + ] + } +} diff --git a/research/depth6-binary-chain/SOURCES.json b/research/depth6-binary-chain/SOURCES.json new file mode 100644 index 0000000000..7078347f73 --- /dev/null +++ b/research/depth6-binary-chain/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/depth5-chain-connector/README.md", + "usage": "input", + "git_blob": "90f3d537de0b6f8b78efff6f4e07ceb8a7fcd90a", + "sha256": "4f65caff2edde24b48341f20d022e058debb067336807d4205366163ac61629d" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/depth6-binary-chain/TASK.json b/research/depth6-binary-chain/TASK.json new file mode 100644 index 0000000000..0f5402b123 --- /dev/null +++ b/research/depth6-binary-chain/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete classification of shortest unsigned depth-six binary dirty-chain schedules: exactly ten words, one cyclic-rotation class and no commuting-neighbor retiming.", + "scope_change_reason": "The initial depth-six minimum is covered by Yifan Kang Proposition 3.1. The original deliverable is therefore the previously uncovered complete shortest-schedule classification. This remains a chain-depth side problem, with no supplier gain.", + "bottleneck_link": "Classifies all chronology freedom at the unit-call optimum of a six-stage arbitrary-map composition. A real recursive consumer and complete physical pricing remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original exact value; do not extend the depth or characteristic census.", + "outcome": "completed", + "evidence": "Exact forward shortest-path counting gives ten. Independent full-matrix backward enumeration lists all ten and identifies precisely the rotations of (1234565432)^2. Full registered replay includes every check.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a structural argument classify shortest schedules without the finite search?", + "why_it_matters": "Explains the rigidity and could determine its all-depth scope.", + "first_step": "Combine the known minimum count vector with forced chronological constraints.", + "blocked_by": "The new classification is finite." + }, + { + "question": "What extra call budget permits nontrivial commuting retiming after adjacent equal-call cancellation?", + "why_it_matters": "Quantifies chronology flexibility beyond the rigid optimum.", + "first_step": "Examine reduced length-22 schedules.", + "blocked_by": "No longer-word enumeration is supplied." + }, + { + "question": "Does a fully paid supplier consumer use this six-stage composition?", + "why_it_matters": "Abstract schedules do not establish recursive savings.", + "first_step": "Name actual maps and price all routing, dispatch and restoration.", + "blocked_by": "No supplier caller is instantiated." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19130783", + "coordination": { + "priority_revision": 7, + "upstream_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "checked_at": "2026-10-22T19:02:26Z", + "overlap": "Live open PRs and Discussion pagination, plus merged chain packages and main README terms. Local cached notes are sparse; no novelty guarantee is inferred from no matches.", + "predecessors": [ + 4249, + 4263, + 4281, + 4418 + ], + "related_open_work": [ + 4600, + 1930 + ] + }, + "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19130859", + "external_prior_work": { + "author": "Yifan Kang", + "title": "CNOT-Optimal Circuit Synthesis", + "date": "2023-08-01", + "url": "https://math.mit.edu/documents/rsi/2023KangY.pdf", + "scope": "Proposition 3.1 proves the directed-path minimum 4n-8; no novelty is claimed for the length 20." + } +} diff --git a/research/depth6-binary-chain/VERIFY.json b/research/depth6-binary-chain/VERIFY.json new file mode 100644 index 0000000000..df06f6bd7e --- /dev/null +++ b/research/depth6-binary-chain/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [ + "research/depth5-chain-connector/README.md", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete shortest-path counting and independent full-matrix backward enumeration: exactly ten shortest words, one cyclic class, no commuting neighbors. Full UT7(F2) BFS, 132 transition-oracle cases, every word interval/matrix identity, 81920 scalar and 8960 two-coordinate dirty replays, six rejection controls and source hashes." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete shortest-path counting and independent full-matrix backward enumeration: exactly ten shortest words, one cyclic class, no commuting neighbors. Full UT7(F2) BFS, 132 transition-oracle cases, every word interval/matrix identity, 81920 scalar and 8960 two-coordinate dirty replays, six rejection controls and source hashes." + } + ] +} diff --git a/research/depth6-binary-chain/verify.py b/research/depth6-binary-chain/verify.py new file mode 100644 index 0000000000..449d9cefd0 --- /dev/null +++ b/research/depth6-binary-chain/verify.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +"""Classify all shortest unsigned binary depth-six dirty-chain schedules.""" + +import hashlib +import json +import random +from pathlib import Path + +import numpy as np + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +DEPTH = 6 +PAIRS = tuple((i, j) for i in range(7) for j in range(i + 1, 7)) +INDEX = {pair: bit for bit, pair in enumerate(PAIRS)} +STATES = 1 << len(PAIRS) +TARGET = 1 << INDEX[0, 6] +CHUNK = 1 << 18 +MAX_DISTANCE = 20 +FILES = ("README.md", "RESULT.json", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def step(states: np.ndarray, letter: int) -> np.ndarray: + """Right multiply encoded UT7 matrices by I + e_(letter,letter+1).""" + require(0 <= letter < DEPTH, "invalid generator") + answer = states ^ np.uint32(1 << INDEX[letter, letter + 1]) + for row in range(letter): + source = (states >> INDEX[row, letter]) & 1 + answer ^= source << INDEX[row, letter + 1] + return answer + + +def matrix_step(state: int, letter: int) -> int: + """Independent full 7-by-7 binary matrix multiplication oracle.""" + acc = [[int(i == j) for j in range(7)] for i in range(7)] + for bit, (i, j) in enumerate(PAIRS): + acc[i][j] = (state >> bit) & 1 + gen = [[int(i == j) for j in range(7)] for i in range(7)] + gen[letter][letter + 1] = 1 + product = [[sum(acc[i][k] * gen[k][j] for k in range(7)) % 2 + for j in range(7)] for i in range(7)] + return sum(product[i][j] << bit for bit, (i, j) in enumerate(PAIRS)) + + +def check_generators() -> int: + # Both formulas are affine over F2. Zero and every basis vector determine + # each entire map, including its constant term, on all 2^21 states. + samples = np.array([0] + [1 << bit for bit in range(21)], dtype=np.uint32) + checked = 0 + for letter in range(DEPTH): + actual = step(samples, letter) + expected = np.array([matrix_step(int(s), letter) for s in samples], + dtype=np.uint32) + require(np.array_equal(actual, expected), "generator oracle mismatch") + require(np.array_equal(step(actual, letter), samples), "not involutive") + checked += len(samples) + return checked + + +def shortest_schedules() -> dict: + """Complete BFS with exact geodesic counts, followed by path enumeration.""" + require(DEPTH ** MAX_DISTANCE < np.iinfo(np.uint64).max, "path-count overflow") + seen = np.full(STATES, 255, dtype=np.uint8) + ways = np.zeros(STATES, dtype=np.uint64) + current = np.empty(STATES, dtype=np.uint32) + following = np.empty(STATES, dtype=np.uint32) + seen[0], current[0], ways[0] = 0, 0, 1 + count, layers, distance = 1, [1], None + for level in range(1, MAX_DISTANCE + 1): + size = 0 + for letter in range(DEPTH): + for start in range(0, count, CHUNK): + part = current[start:min(start + CHUNK, count)] + candidates = step(part, letter) + eligible = (seen[candidates] == 255) | (seen[candidates] == level) + # Distinct sources have distinct images under this bijection. + # Current-layer counts are final before the next layer starts. + ways[candidates[eligible]] += ways[part[eligible]] + fresh = candidates[seen[candidates] == 255] + end = size + len(fresh) + require(end <= STATES, "frontier capacity exhausted") + # Each generator is a bijection, so this chunk has no repeats. + # Mark immediately to deduplicate subsequent generators/chunks. + seen[fresh] = level + following[size:end] = fresh + size = end + layers.append(size) + current, following, count = following, current, size + if seen[TARGET] != 255: + distance = int(seen[TARGET]) + break + require(count > 0, "target unreachable") + require(distance is not None, "target absent within declared distance bound") + total = int(ways[TARGET]) + require(0 < total <= 100, "geodesic enumeration capacity exceeded") + words = enumerate_schedules(seen, distance, total) + require(sum(layers) == int(np.count_nonzero(seen != 255)), "layer partition") + return {"distance": distance, "layers": layers, + "shortest_word_count": total, "words": words} + + +def enumerate_schedules(seen: np.ndarray, distance: int, total: int) -> list: + """Enumerate every decreasing-distance path using full matrix products.""" + paths = [(TARGET, "")] + for level in range(distance, 0, -1): + following = [] + for state, suffix in paths: + for letter in range(DEPTH): + previous = matrix_step(state, letter) + if int(seen[previous]) == level - 1: + following.append((previous, str(letter + 1) + suffix)) + require(len(following) <= total, "too many predecessor paths") + paths = following + require(len(paths) == total, "path count disagrees with forward counting") + require(all(state == 0 for state, _ in paths), "path misses identity") + words = sorted(suffix for _, suffix in paths) + require(len(set(words)) == total, "duplicate labelled path") + return words + + +def interval_signature(word: str) -> tuple: + """Integer scattered-subword counts, reduced only at the end.""" + require(len(word) <= MAX_DISTANCE, "word exceeds replay bound") + require(all(letter in "123456" for letter in word), "invalid word") + counts = {(i, j): 0 for i in range(1, 7) for j in range(i, 7)} + for event in word: + letter = int(event) + for first in range(1, letter + 1): + counts[first, letter] += 1 if first == letter else counts[first, letter - 1] + return tuple(counts[i + 1, j] % 2 for i, j in PAIRS) + + +def correct(word: str) -> bool: + return interval_signature(word) == tuple(int(pair == (0, 6)) for pair in PAIRS) + + +def matvec(matrix: tuple, vector: tuple) -> tuple: + return tuple(sum(matrix[i][j] * vector[j] for j in range(2)) % 2 + for i in range(2)) + + +def replay(word: str, maps: tuple, initial: tuple) -> bool: + registers = list(initial) + for event in word: + letter = int(event) + gain = matvec(maps[letter - 1], registers[letter - 1]) + registers[letter] = tuple(a ^ b for a, b in zip(registers[letter], gain)) + gain = initial[0] + for matrix in maps: + gain = matvec(matrix, gain) + wanted = tuple(a ^ b for a, b in zip(initial[6], gain)) + return tuple(registers[:6]) == initial[:6] and registers[6] == wanted + + +def dirty_checks(word: str) -> tuple: + scalar_cases = 0 + for map_mask in range(64): + for initial_mask in range(128): + initial = [(initial_mask >> i) & 1 for i in range(7)] + registers = initial[:] + for event in word: + letter = int(event) + registers[letter] ^= ((map_mask >> (letter - 1)) & 1) * registers[letter - 1] + wanted = initial[6] ^ (int(map_mask == 63) * initial[0]) + require(registers[:6] == initial[:6] and registers[6] == wanted, + "scalar dirty replay") + scalar_cases += 1 + rng = random.Random(1022) + swap, projection = ((0, 1), (1, 0)), ((1, 0), (0, 0)) + families = [(swap, projection) * 3, (((0, 0), (0, 0)),) * 6] + for _ in range(62): + families.append(tuple(tuple(tuple(rng.randrange(2) for _ in range(2)) + for _ in range(2)) for _ in range(6))) + matrix_cases = 0 + for maps in families: + for basis in range(14): + initial = tuple(tuple(int(2 * row + column == basis) for column in range(2)) + for row in range(7)) + require(replay(word, maps, initial), "noncommuting dirty replay") + matrix_cases += 1 + return scalar_cases, matrix_cases + + +def controls(word: str) -> int: + mutants = [word[:-1], word[1:], word[:-1] + "2", "123456", + word[:3] + word[4] + word[3] + word[5:]] + require(all(not correct(mutant) for mutant in mutants), "invalid-word control") + try: + interval_signature(word[:-1] + "7") + except ValueError as error: + require(str(error) == "invalid word", "wrong rejection reason") + else: + raise ValueError("unknown generator accepted") + return len(mutants) + 1 + + +def source_hashes() -> dict: + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + require(len(sources["files"]) == 4, "source inventory size") + hashes = {} + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "source input changed: " + row["path"]) + hashes[row["path"]] = digest + return hashes + + +def main() -> None: + hashes = source_hashes() + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(expected["schema_version"] == 1, "result schema") + oracle_cases = check_generators() + actual = shortest_schedules() + require(actual == expected["bfs"], "BFS result differs from committed certificate") + base = "1234565432" * 2 + rotations = sorted({base[i:] + base[:i] for i in range(len(base))}) + require(actual["words"] == rotations, "not precisely the ten cyclic rotations") + scalar_cases, matrix_cases = 0, 0 + for word in actual["words"]: + require(correct(word), "chronological interval identity") + require([word.count(str(i)) for i in range(1, 7)] == [2, 4, 4, 4, 4, 2], + "unexpected minimal count vector") + require(all(abs(int(a) - int(b)) == 1 for a, b in zip(word, word[1:])), + "commuting neighbors in a shortest word") + state = 0 + for event in word: + state = matrix_step(state, int(event) - 1) + require(state == TARGET, "full matrix word product") + scalar, matrix = dirty_checks(word) + scalar_cases += scalar + matrix_cases += matrix + rejected = controls("23456543212345654321") + for filename in FILES: + hashes[str((PACKAGE / filename).relative_to(ROOT))] = hashlib.sha256( + (PACKAGE / filename).read_bytes()).hexdigest() + receipt = {"result": actual, "generator_oracle_cases": oracle_cases, + "scalar_dirty_cases": scalar_cases, "matrix_dirty_cases": matrix_cases, + "rejected_controls": rejected, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_DEPTH6_BINARY_CHAIN shortest_words=10 rotation_classes=1 distance=20 " + "oracle=132 scalar=81920 matrix=8960 controls=6") + + +if __name__ == "__main__": + main()