diff --git a/research/fixed-line-crossing-floor/PROOF.md b/research/fixed-line-crossing-floor/PROOF.md new file mode 100644 index 0000000000..db828c07b0 --- /dev/null +++ b/research/fixed-line-crossing-floor/PROOF.md @@ -0,0 +1,104 @@ +# The fixed-line permutation theorem + +## Contract + +Let `V` be a finite-dimensional binary vector space and let `L_1,...,L_n` +be distinct one-dimensional subspaces. The scalar payload space is over an +arbitrary field `K`; the frame field and payload field need not agree. +Register `X_i` has frame `L_i` and arbitrary independent initial payload `x_i`. +All public register frames stay fixed. Other public registers have arbitrary +independent initial payloads. There are no preloaded copies of any `x_i`. + +The circuit is finite, fixed and linear. A local operation can combine or +scale registers only when their current frames agree. Owned registers can be +initialized to zero at any frame and cleared at any time. Every owned MOVE +changes a register's frame between strictly nested subspaces; its rank is the +positive dimension difference. MOVEs carry the payload unchanged in the +common-chart convention. Arbitrarily many carriers, feedback, intermediate +frames, repeated visits and interleaved reads and writes are permitted. +No control flow or scalar side channel communicates payload between frames. + +For a permutation `pi` and nonzero scalars `a_i`, require the checkpoint +endpoint `X_{pi(i)} = a_i x_i`. All other public registers are restored and +all owned registers are cleared. Let `s` be the number of indices with +`pi(i) != i`. The checkpoint is before releasing the fixed public frames. + +## Theorem + +Every such circuit has at least `2s` owned MOVEs. A circuit with exactly `2s` +rank-one MOVEs exists. Consequently its minimum owned MOVE tariff is `2s` +for every tariff `c(r)` with `c(1)=1` and `c(r)>=1` for positive integer `r`. + +### Lower bound + +For a designated line `L_i`, call the set of registers whose current frame +equals `L_i` its region. An INIT contributes zero, a CLEAR discards data, +and local operations cannot communicate across its boundary. The only ways +data enter or leave this region are MOVEs whose arrival or departure frame +equals `L_i`. This statement includes every owned carrier currently there. + +If no MOVE ever leaves `L_i`, the coefficient of the independent input `x_i` +remains zero in every register outside the region. This follows by induction +on events. Local operations outside see zero coefficients; INIT is zero; +CLEAR cannot introduce one; and every MOVE not leaving the region carries +a zero coefficient from an outside register or remains within it. But for +`pi(i) != i`, the endpoint outside the region contains `a_i x_i` with +`a_i != 0`. Therefore a departure from `L_i` is required. + +Likewise, if no MOVE ever enters `L_i`, every register there stays independent +of all initial `x_j` with `j != i`. The same event induction proves this, +even if outside registers have previously received `x_i`. For a moved line, +its final register requires `x_{pi^{-1}(i)}` from a different line, with a +nonzero coefficient. Therefore an arrival at `L_i` is required. + +There are `s` departure requirements and `s` arrival requirements. A single +MOVE can serve at most one of them. Its departure frame and arrival frame +cannot be two different designated lines, since distinct lines are +incomparable and every MOVE is strictly nested. Nor can both endpoints be +the same designated line, since the inclusion is strict. Each MOVE thus +contributes at most one item to these `2s` requirements. This proves the +lower bound without a read-once, two-phase or independent-carrier premise. + +### Attainment + +For each moved index `i`, initialize a zero owned register `C_i` at `L_i`, +copy `X_i` into it, and set `X_i := X_i - C_i`. These are local operations; +now `C_i=x_i` and all moved public registers are zero. Scale any fixed-point +register `X_i` by `a_i` locally. + +For each moved source `i`, put `j=pi(i)` and `H=L_i+L_j`. The two distinct +binary lines span a plane. MOVE `C_i` from `L_i` UP to `H` and DOWN to `L_j`, +then perform `X_j := X_j + a_i C_i` and CLEAR `C_i`. Both MOVEs have rank one. +Every moved destination receives exactly one source. Therefore the endpoint +is the required scaled permutation and all owned registers are cleared. +Other public registers are untouched. There are exactly `2s` MOVEs. + +All scalar copying, subtraction, scaling and owned erasure are part of this +local circuit, but only its MOVEs are counted in the stated tariff. The +construction uses `s` owned registers; it does not claim minimum peak storage. + +## Application and limits + +PR #6939 section 1.3 specifies a perfect-matching exchange on the 104 distinct +P104 lines before its Y bounce. Each of its X registers exchanges its x payload +with its partner while both public frames stay fixed. Taking `s=104` proves +an owned-MOVE floor of `208` for that preprocessing contract. The predecessor's +two rank-one transfers per port attain it. This is an application of the new +all-circuit lower bound, not a new construction of the predecessor's native. + +In particular, sharing runs, allowing more intermediate frames or tolerating +temporary junk cannot save an owned MOVE while preserving this contract. +Merely checking the endpoint's shadow matrix would not establish this floor; +the separation of line regions is the additional invariant. + +The application does not assert that every proposed shared-landing native +contains this checkpoint. Allowing a public register to leave its line, using +a different endpoint, or interleaving with the later changing Y frames removes +a hypothesis. The full common-chart versus physical phase interface, the +complete signed invoice and every all-size framework assumption remain open. +The checker's changed-frame control permits public descent as well as ascent. +It demonstrates the necessity of the fixed-frame premise in this abstract +model; it does not supply a native under monotone public-frame rules. +For `0 <= C <= 1`, `r^(1-C)>=1` at every positive integer rank, so the tariff +corollary applies on its stated range. Nothing is asserted for cheaper +positive-rank tariffs. diff --git a/research/fixed-line-crossing-floor/README.md b/research/fixed-line-crossing-floor/README.md new file mode 100644 index 0000000000..ac6ca7498c --- /dev/null +++ b/research/fixed-line-crossing-floor/README.md @@ -0,0 +1,97 @@ +# Exact transport cost for a fixed-line permutation + +For a permutation moving `s` public registers on distinct fixed lines, the +minimum number of owned MOVEs is **`2s`**. Every MOVE can have rank one in an +attaining schedule. Thus the minimum owned tariff is also `2s` whenever a +rank-one MOVE costs one and every positive-rank MOVE costs at least one, +including `r^(1-C)` for `0 <= C <= 1`. + +This is a **scoped written proof with exact finite corroboration**. It permits +arbitrarily many shared owned carriers, feedback, interleaved reads and writes, +intermediate subspaces and owned erasure. The public registers stay on their +distinct lines throughout the exchange, and scalar gates only join registers +on equal frames. [PROOF.md](PROOF.md) states the complete contract and proof. +The universal result rests on that proof, not on a finite census. + +## Connection to the Whitehead question + +DreamingOfClouds's [PR #6939](https://github.com/CrocSwap/integer-mult-bounds/pull/6939) +asks whether shared owned runs can carry the beta crossings of its window +native more cheaply. Its existing matching exchange moves all 104 public X +registers while they remain on distinct lines. The theorem gives an exact +**208-MOVE floor for that exchange**, even with arbitrary carrier sharing and +interleaving. Its rank-one exchange attains the floor. We cite that construction +and the port count; we do not replay or claim credit for them. + +This closes sharing as a way to improve that fixed-line preprocessing contract. +It does not exclude changing public frames during the exchange, mixing the +exchange with the later Y bounce, Gamma coupling, or a different native. +No kappa improvement, supplier admission, full physical native replay or +complete multiplication theorem is claimed. The tariff counts owned MOVEs +only. Scalar operations, allocation, storage and physical delivery remain +separate costs. + +## Reproduce + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/fixed-line-crossing-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B research/fixed-line-crossing-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-line-crossing-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-line-crossing-floor --check-source-history +``` + +The marker is `PASS_FIXED_LINE_CROSSING_FLOOR`. The checker enumerates every +permutation through six registers over Q and three prime fields, checks a +104-register exchange, enumerates all nested MOVE edges in the binary subspace +lattices through dimension four, and exercises rejected circuits and a changed +public-frame control. Its stdout receipt binds the package bytes by SHA256. +It writes no generated files. Exact counts appear in the generated output. +An export can run the direct verifier without Git or predecessor executables. +The changed-frame control permits public ascent and descent; it is a boundary +test, not a proposed legal native. + +[SOURCES.json](SOURCES.json) pins the predecessor text, catalogue and selected +record as historical provenance. There are no external runtime inputs or +dependencies. The selected metadata orientation passed; the selected cold +replay, predecessor scientific suites, Lean and Docker were not run. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can a public-frame change or an exchange interleaved with the Y bounce + reduce the complete Whitehead bill? This escapes a specific hypothesis of + the floor. Start with one literal shared-carrier schedule and record its + complete endpoint, frame changes and both public and owned charges. A legal + schedule with restored outputs and a favorable complete bill is missing. +- What is the smallest peak owned storage among schedules attaining `2s` + MOVEs? The construction here uses one carrier per moved source. Start with + a single permutation cycle and permit interleaving; a matching storage + lower bound is not supplied here. + +## Credit + +The new fixed-line theorem, general attaining schedule and checker were +produced by Nick Petalas. DreamingOfClouds supplies the Whitehead window +construction, matching exchange and shared-landing question in #6939. +Retain its credit to Ali Romman #5599, CubeJerry #6912/#6914/#6916, +unpaidmoon #6930, icekylinx #104 and their native/caller predecessors. +New work is Apache-2.0; predecessor files remain unchanged. + +## Checker bounds + +The finite checker caps inputs at 104 ports and 832 events, with at most 211 +symbolic rows of 107 integer coefficients. It enumerates at most 720 +permutations at a given size and four payload fields. The lattice check uses +at most 67 subspaces with 16 elements each. Every loop has an explicit finite +corpus or enforced input bound; no recursion, subprocess or network call is +used. Each function is under 60 lines. Explicit checks remain enabled under +optimized Python. + +Python's managed runtime allocates rows, sets and integers during replay, +which is a deviation from fixed allocation under Power of Ten rule 3. The +stated finite capacities bound live collections; fixture coefficients have +absolute value at most 104. This is a bounded offline verifier, not a real-time +implementation. Revisit allocation and coefficient bounds before expanding +its input domain. Warnings are errors in both registered commands. diff --git a/research/fixed-line-crossing-floor/SOURCES.json b/research/fixed-line-crossing-floor/SOURCES.json new file mode 100644 index 0000000000..6a41951121 --- /dev/null +++ b/research/fixed-line-crossing-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-whitehead-native-objects/PROOF.md", + "usage": "provenance", + "git_blob": "4956b7e63f50870b3fd0a1ed3162224e876ead6c", + "sha256": "d01547cfeeec205af989999b00f4e7a59c827aaff6a5a86c182fd151f0bd0d73" + }, + { + "path": "research/p104-whitehead-native-objects/README.md", + "usage": "provenance", + "git_blob": "9fcc0292a7c6ec24c447d45791e010797e75ab58", + "sha256": "42c8b1f7a5b6561e206fdd06a4b942a7bebce10f0cb082f34b55268371893c4f" + } + ] +} diff --git a/research/fixed-line-crossing-floor/TASK.json b/research/fixed-line-crossing-floor/TASK.json new file mode 100644 index 0000000000..d52a55ad15 --- /dev/null +++ b/research/fixed-line-crossing-floor/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the 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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "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": "Sharp 2s owned-MOVE lower bound and rank-one attainment for scaled permutations moving s public registers on distinct fixed binary lines, with arbitrary shared carriers and local linear feedback. Application to the 104-port matching preprocessing contract of PR6939 gives 208 owned MOVEs.", + "scope_change_reason": "Replace helper-inventory construction with one exact transport obstruction for the shared-landing question in DreamingOfClouds PR6939. The fixed-line preprocessing contract is essential; no full native exclusion follows.", + "bottleneck_link": "Eliminates carrier sharing alone as a way to lower the Whitehead beta-crossing preprocessing bill while public X frames stay fixed. A promising continuation must change that boundary or combine it with the Y bounce and pay the full bill.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp local theorem after exact attainers, frame-edge checks and rejection controls; do not extend to a changed native.", + "outcome": "negative-result", + "evidence": "PROOF.md; verify.py: 3492 small exact matrix cases, 1008 nested frame edges, one generic 104-port exchange, 18 rejection controls, and one changed-public-frame escape control.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a public-frame change or an exchange interleaved with the Y bounce reduce the complete Whitehead bill?", + "why_it_matters": "These changes escape the fixed-frame checkpoint and can change the native construction decision.", + "first_step": "Write one literal shared-carrier schedule, then record its complete endpoint, all public and owned frame changes, and full charges.", + "blocked_by": "No legal schedule with restored outputs and a favorable complete bill is supplied." + }, + { + "question": "What is the smallest peak owned storage at the minimum 2s MOVE count?", + "why_it_matters": "The general attainer uses one carrier per moved source; storage is separate from its MOVE optimum.", + "first_step": "Analyze one permutation cycle with interleaved carrier transport and overwrite.", + "blocked_by": "A matching storage lower bound and complete physical storage price are not supplied." + } + ], + "environment": { + "python": "3.12.15", + "dependencies": "standard library only" + }, + "predecessor": { + "pr": 6939, + "author": "DreamingOfClouds", + "question": "README Open next question 2; PROOF section 6 item 2", + "input_status": "Cited predecessor text and matching construction; no scientific executable replayed." + } +} diff --git a/research/fixed-line-crossing-floor/VERIFY.json b/research/fixed-line-crossing-floor/VERIFY.json new file mode 100644 index 0000000000..e86a39f3be --- /dev/null +++ b/research/fixed-line-crossing-floor/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact scaled-permutation endpoints and scratch clearing over integers and F2/F3/F5; all nested frame edges through dimension four; sharp move/rank/peak counts; 18 rejection controls; changed-public-frame escape; generated package hash receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all exact checks with Python assertions disabled; explicit contracts must remain active." + } + ] +} diff --git a/research/fixed-line-crossing-floor/verify.py b/research/fixed-line-crossing-floor/verify.py new file mode 100644 index 0000000000..893bcb33b8 --- /dev/null +++ b/research/fixed-line-crossing-floor/verify.py @@ -0,0 +1,309 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of PROOF.md; no predecessor code is executed.""" +from __future__ import annotations + +from dataclasses import dataclass, replace +from hashlib import sha256 +from itertools import permutations +import json +from pathlib import Path +import sys + +MAX_PORTS = 104 +MAX_EVENTS = 8 * MAX_PORTS +PACKAGE_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") +Frame = frozenset[int] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def span(vectors: tuple[int, ...]) -> Frame: + require(len(vectors) <= 128, "too many frame generators") + result = {0} + for vector in vectors: + require(0 <= vector < 128, "frame vector out of bounds") + result |= {entry ^ vector for entry in result} + return frozenset(result) + + +@dataclass(frozen=True) +class Event: + op: str + target: int + source: int = -1 + scalar: int = 1 + frame: Frame | None = None + + +@dataclass(frozen=True) +class Program: + lines: tuple[Frame, ...] + permutation: tuple[int, ...] # source i goes to permutation[i] + scales: tuple[int, ...] + events: tuple[Event, ...] + modulus: int = 0 + + +def validate(program: Program) -> int: + n = len(program.lines) + require(1 <= n <= MAX_PORTS, "port count outside finite checker domain") + require(len(set(program.lines)) == n, "lines must be distinct") + for frame in program.lines: + require(len(frame) == 2 and 0 in frame, "not a binary line") + require(all(0 <= v < 128 for v in frame), "line outside ambient space") + require(sorted(program.permutation) == list(range(n)), "not a permutation") + require(len(program.scales) == n, "wrong scale count") + require(program.modulus in (0, 2, 3, 5), "unsupported finite check field") + for scale in program.scales: + require(isinstance(scale, int), "scale must be integral in checker") + require(scale != 0 if program.modulus == 0 + else scale % program.modulus != 0, "zero scale") + require(len(program.events) <= MAX_EVENTS, "event capacity exceeded") + return n + + +def build(permutation: tuple[int, ...], modulus: int = 0) -> Program: + n = len(permutation) + lines = tuple(frozenset((0, i + 1)) for i in range(n)) + scales = tuple((-1) ** i * (i + 1) if modulus == 0 + else 1 + i % (modulus - 1) for i in range(n)) + draft = Program(lines, permutation, scales, (), modulus) + validate(draft) + events = [] + for i, j in enumerate(permutation): + if i == j: + events.append(Event("SCALE", i, scalar=scales[i])) + else: + carrier = n + 3 + i + events.extend((Event("INIT", carrier, frame=lines[i]), + Event("ADD", carrier, i), + Event("ADD", i, carrier, -1))) + for i, j in enumerate(permutation): + if i != j: + carrier = n + 3 + i + plane = span(tuple(lines[i] | lines[j])) + events.extend((Event("MOVE", carrier, frame=plane), + Event("MOVE", carrier, frame=lines[j]), + Event("ADD", j, carrier, scales[i]), + Event("CLEAR", carrier))) + result = replace(draft, events=tuple(events)) + validate(result) + return result + + +def frame_move(old: Frame, new: Frame) -> int: + require(bool(new) and len(new) <= 128 and 0 in new, "invalid frame size") + require(span(tuple(new)) == new, "frame is not a binary subspace") + require(old < new or new < old, "MOVE frames are not strictly nested") + return abs(len(old).bit_length() - len(new).bit_length()) + + +def row_operation(event: Event, rows: list[list[int]], + frames: list[Frame | None], modulus: int) -> None: + target = event.target + if event.op == "ADD": + require(0 <= event.source < len(rows), "source role out of bounds") + require(frames[event.source] is not None, "read of dead carrier") + require(frames[target] == frames[event.source], "nonlocal scalar ADD") + source = rows[event.source].copy() + rows[target] = [a + event.scalar * b + for a, b in zip(rows[target], source, strict=True)] + elif event.op == "SCALE": + require(event.scalar != 0 if modulus == 0 + else event.scalar % modulus != 0, "singular scalar SCALE") + rows[target] = [event.scalar * entry for entry in rows[target]] + else: + raise ValueError("unknown scalar operation") + if modulus: + rows[target] = [entry % modulus for entry in rows[target]] + + +def endpoints(program: Program, rows: list[list[int]], + frames: list[Frame | None], initial: list[Frame | None]) -> None: + n = len(program.lines) + columns = n + 3 + expected = [[0] * columns for _ in range(columns)] + for i, j in enumerate(program.permutation): + expected[j][i] = program.scales[i] + for i in range(n, columns): + expected[i][i] = 1 + if program.modulus: + expected = [[entry % program.modulus for entry in row] + for row in expected] + require(rows[:columns] == expected, "wrong complete public endpoint") + require(frames == initial, "wrong final frames or live owned carrier") + require(all(not any(row) for row in rows[columns:]), "uncleared payload") + + +def replay(program: Program, frozen: bool = True) -> dict: + n = validate(program) + columns = n + 3 + full = span(tuple(range(1, n + 1))) + initial = list(program.lines) + [frozenset((0,)), full, program.lines[0]] + initial += [None] * n + frames = initial.copy() + rows = [[int(i == j) for j in range(columns)] for i in range(columns)] + rows += [[0] * columns for _ in range(n)] + moves = [] + live = peak = 0 + for event in program.events: + target = event.target + require(0 <= target < len(rows), "target role out of bounds") + owned = target >= columns + if event.op == "INIT": + require(owned and frames[target] is None, "invalid owned INIT") + require(event.frame is not None, "missing INIT frame") + require(span(tuple(event.frame)) == event.frame, "invalid INIT frame") + frames[target] = event.frame + rows[target] = [0] * columns + live += 1 + peak = max(peak, live) + else: + require(frames[target] is not None, "operation on dead carrier") + if event.op == "CLEAR": + require(owned, "public CLEAR is forbidden") + frames[target] = None + rows[target] = [0] * columns + live -= 1 + elif event.op == "MOVE": + require(owned or not frozen, "public MOVE violates fixed frames") + require(event.frame is not None, "missing MOVE frame") + old = frames[target] + require(old is not None, "missing departure frame") + rank = frame_move(old, event.frame) + moves.append((old, event.frame, rank, owned)) + frames[target] = event.frame + else: + row_operation(event, rows, frames, program.modulus) + endpoints(program, rows, frames, initial) + require(live == 0, "owned lifetime imbalance") + moved = [i for i, j in enumerate(program.permutation) if i != j] + for i in moved: + require(any(old == program.lines[i] for old, _, _, _ in moves), "no exit") + require(any(new == program.lines[i] for _, new, _, _ in moves), "no entry") + owned_ranks = [rank for _, _, rank, owned in moves if owned] + return {"moves": len(owned_ranks), "rank_mass": sum(owned_ranks), "peak": peak} + + +def all_subspaces(dimension: int) -> tuple[Frame, ...]: + require(1 <= dimension <= 4, "lattice enumeration domain") + spaces = {frozenset((0,))} + for _ in range(dimension): + require(len(spaces) <= 67, "subspace capacity exceeded") + spaces |= {span(tuple(frame) + (vector,)) + for frame in tuple(spaces) for vector in range(1 << dimension)} + return tuple(sorted(spaces, key=lambda frame: (len(frame), tuple(sorted(frame))))) + + +def check_lattice_edges() -> dict: + counts, edges = [], 0 + for dimension in range(1, 5): + spaces = all_subspaces(dimension) + require(len(spaces) == (2, 5, 16, 67)[dimension - 1], "wrong lattice") + counts.append(len(spaces)) + for old in spaces: + for new in spaces: + if old < new or new < old: + rank = frame_move(old, new) + require(rank >= 1, "nonpositive rank") + # An edge cannot satisfy both a designated-line exit and entry. + require(int(len(old) == 2) + int(len(new) == 2) <= 1, + "nested MOVE joins two line boundaries") + edges += 1 + return {"subspace_counts": counts, "nested_edges": edges} + + +def check_permutations() -> dict: + cases = 0 + maximum_moves = 0 + for n in range(1, 7): + for permutation in permutations(range(n)): + moved = sum(i != j for i, j in enumerate(permutation)) + for modulus in (0, 2, 3, 5): + answer = replay(build(permutation, modulus)) + require(answer["moves"] == answer["rank_mass"] == 2 * moved, + "attainer misses sharp tariff") + require(answer["peak"] == moved, "unexpected carrier peak") + maximum_moves = max(maximum_moves, answer["moves"]) + cases += 1 + permutation = tuple(i ^ 1 for i in range(MAX_PORTS)) + large = replay(build(permutation)) + require(large == {"moves": 208, "rank_mass": 208, "peak": 104}, + "104-port size fixture failed") + return {"small_matrix_cases": cases, "small_maximum_moves": maximum_moves, + "large_generic_fixture": large} + + +def reject(program: Program) -> None: + try: + replay(program) + except ValueError: + return + raise ValueError("invalid circuit unexpectedly accepted") + + +def check_controls() -> int: + base = build((1, 0)) + events = base.events + first_move = next(i for i, event in enumerate(events) if event.op == "MOVE") + controls = [replace(base, permutation=(0, 0)), + replace(base, lines=(base.lines[0], base.lines[0])), + replace(base, scales=(0, 1)), + replace(base, events=events[1:]), + replace(base, events=events[:first_move] + events[first_move + 1:]), + replace(base, events=events[:-1]), + replace(base, events=(Event("CLEAR", 0),) + events), + replace(base, events=(Event("ADD", 0, 1),) + events), + replace(base, events=(Event("ADD", 0, 5),) + events), + replace(base, events=(Event("MOVE", 0, frame=frozenset((0, 1, 2, 3))),) + events)] + for index, replacement in ((first_move, Event("MOVE", 5, frame=base.lines[1])), + (first_move, Event("MOVE", 5, frame=frozenset((0, 1, 2)))), + (first_move + 2, Event("ADD", 1, 5, 2)), + (2, Event("ADD", 0, 5, 1)), + (1, Event("INIT", 5, frame=base.lines[0]))): + controls.append(replace(base, events=events[:index] + (replacement,) + events[index + 1:])) + for program in controls: + reject(program) + for permutation, modulus in (((), 0), (tuple(range(105)), 0), ((0,), 7)): + try: + build(permutation, modulus) + except ValueError: + continue + raise ValueError("invalid builder domain unexpectedly accepted") + return len(controls) + 3 + + +def check_changed_contract() -> dict: + base = Program((frozenset((0, 1)), frozenset((0, 2))), (1, 0), (1, 1), ()) + plane = frozenset((0, 1, 2, 3)) + events = (Event("MOVE", 0, frame=plane), Event("MOVE", 1, frame=plane), + Event("ADD", 0, 1), Event("ADD", 1, 0, -1), + Event("ADD", 0, 1), Event("SCALE", 1, scalar=-1), + Event("MOVE", 0, frame=base.lines[0]), + Event("MOVE", 1, frame=base.lines[1])) + program = replace(base, events=events) + reject(program) + answer = replay(program, frozen=False) + require(answer["moves"] == 0, "changed-contract escape failed") + return {"public_moves": 4, "owned_moves": answer["moves"]} + + +def main() -> None: + require(len(sys.argv) == 1, "this checker takes no arguments") + report = {"claim_type": "scoped written proof with exact finite corroboration", + "lattice": check_lattice_edges(), "attainers": check_permutations(), + "rejected_controls": check_controls(), + "changed_contract": check_changed_contract()} + here = Path(__file__).resolve().parent + report["source_sha256"] = {name: sha256((here / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + print(json.dumps(report, sort_keys=True)) + print("PASS_FIXED_LINE_CROSSING_FLOOR") + + +if __name__ == "__main__": + main()